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

Theorem opabbidv 4464
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 1674 . 2  |-  F/ x ph
2 nfv 1674 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4463 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370   {copab 4458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-opab 4460
This theorem is referenced by:  opabbii  4465  csbopab  4729  csbopabgALT  4730  csbmpt12  4731  xpeq1  4963  xpeq2  4964  opabbi2dv  5098  csbcnvgALT  5133  resopab2  5264  mptcnv  5348  cores  5450  xpco  5486  dffn5  5847  f1oiso2  6153  f1ocnvd  6420  ofreq  6434  bropopvvv  6764  fnwelem  6798  sprmpt2d  6853  mpt2curryd  6899  wemapwe  8040  wemapweOLD  8041  shftfval  12678  2shfti  12688  fsumrev  13365  prdsval  14513  pwsle  14550  sectffval  14809  sectfval  14810  isfunc  14894  isfull  14940  isfth  14944  ipoval  15444  eqgfval  15849  dvdsrval  16861  dvdsrpropd  16912  ltbval  17678  opsrval  17681  lmfval  18969  pt1hmeo  19512  xkocnv  19520  tgphaus  19820  isphtpc  20699  bcthlem1  20968  bcth  20973  ulmval  21979  lgsquadlem3  22829  iscgrg  23102  legval  23154  perpln1  23247  perpln2  23248  isperp  23249  wlks  23578  wlkon  23582  trls  23588  trlon  23592  pths  23618  spths  23619  pthon  23627  spthon  23634  iseupa  23739  ajfval  24362  f1o3d  26100  f1od2  26176  inftmrel  26343  isinftm  26344  metidval  26463  faeval  26807  eulerpartlemgvv  26904  eulerpart  26910  afsval  27140  fprodshft  27632  fprodrev  27633  fnopabeqd  28762  dnwech  29550  aomclem8  29563  dfafn5a  30215  wlkelwrd  30429  wlkcompim  30436  clwlk  30567  clwlkcompim  30576  lcvfbr  33004  cmtfvalN  33194  cvrfval  33252  dicffval  35158  dicfval  35159  dicval  35160
  Copyright terms: Public domain W3C validator