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

Theorem opabbidv 4502
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 1712 . 2  |-  F/ x ph
2 nfv 1712 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4501 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   {copab 4496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-opab 4498
This theorem is referenced by:  opabbii  4503  csbopab  4768  csbopabgALT  4769  csbmpt12  4770  xpeq1  5002  xpeq2  5003  opabbi2dv  5141  csbcnvgALT  5176  resopab2  5310  mptcnv  5393  cores  5493  xpco  5530  dffn5  5893  f1oiso2  6223  f1ocnvd  6497  ofreq  6516  bropopvvv  6853  fnwelem  6888  sprmpt2d  6944  mpt2curryd  6990  wemapwe  8130  wemapweOLD  8131  xpcogend  12892  shftfval  12985  2shfti  12995  prdsval  14944  pwsle  14981  sectffval  15238  sectfval  15239  isfunc  15352  isfull  15398  isfth  15402  ipoval  15983  eqgfval  16448  dvdsrval  17489  dvdsrpropd  17540  ltbval  18331  opsrval  18334  lmfval  19900  xkocnv  20481  tgphaus  20781  isphtpc  21660  bcthlem1  21929  bcth  21934  ulmval  22941  lgsquadlem3  23829  iscgrg  24105  legval  24172  ishlg  24187  perpln1  24288  perpln2  24289  isperp  24290  ishpg  24329  iscgra  24370  wlks  24721  wlkcompim  24728  wlkelwrd  24732  wlkon  24735  trls  24740  trlon  24744  pths  24770  spths  24771  pthon  24779  spthon  24786  clwlk  24955  clwlkcompim  24966  iseupa  25167  ajfval  25922  f1o3d  27690  f1od2  27778  inftmrel  27958  isinftm  27959  metidval  28104  faeval  28455  eulerpartlemgvv  28579  eulerpart  28585  afsval  28815  fnopabeqd  30450  dnwech  31233  aomclem8  31246  dfafn5a  32484  lcvfbr  35142  cmtfvalN  35332  cvrfval  35390  dicffval  37298  dicfval  37299  dicval  37300
  Copyright terms: Public domain W3C validator