MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opabbidv Structured version   Unicode version

Theorem opabbidv 4503
Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
opabbidv  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)

Proof of Theorem opabbidv
StepHypRef Expression
1 nfv 1678 . 2  |-  F/ x ph
2 nfv 1678 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4502 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374   {copab 4497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-opab 4499
This theorem is referenced by:  opabbii  4504  csbopab  4772  csbopabgALT  4773  csbmpt12  4774  xpeq1  5006  xpeq2  5007  opabbi2dv  5143  csbcnvgALT  5178  resopab2  5313  mptcnv  5399  cores  5501  xpco  5538  dffn5  5904  f1oiso2  6227  f1ocnvd  6499  ofreq  6518  bropopvvv  6853  fnwelem  6888  sprmpt2d  6942  mpt2curryd  6988  wemapwe  8128  wemapweOLD  8129  shftfval  12853  2shfti  12863  fsumrev  13543  prdsval  14699  pwsle  14736  sectffval  14995  sectfval  14996  isfunc  15080  isfull  15126  isfth  15130  ipoval  15630  eqgfval  16037  dvdsrval  17071  dvdsrpropd  17122  ltbval  17900  opsrval  17903  lmfval  19492  pt1hmeo  20035  xkocnv  20043  tgphaus  20343  isphtpc  21222  bcthlem1  21491  bcth  21496  ulmval  22502  lgsquadlem3  23352  iscgrg  23625  legval  23691  perpln1  23788  perpln2  23789  isperp  23790  wlks  24181  wlkcompim  24188  wlkelwrd  24192  wlkon  24195  trls  24200  trlon  24204  pths  24230  spths  24231  pthon  24239  spthon  24246  clwlk  24415  clwlkcompim  24426  iseupa  24627  ajfval  25386  f1o3d  27130  f1od2  27205  inftmrel  27372  isinftm  27373  metidval  27491  faeval  27844  eulerpartlemgvv  27941  eulerpart  27947  afsval  28177  fprodshft  28669  fprodrev  28670  fnopabeqd  29800  dnwech  30587  aomclem8  30600  dfafn5a  31667  lcvfbr  33692  cmtfvalN  33882  cvrfval  33940  dicffval  35846  dicfval  35847  dicval  35848  xpcogend  36658
  Copyright terms: Public domain W3C validator