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

Theorem opabbidv 4274
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 1630 . 2  |-  F/ x ph
2 nfv 1630 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4273 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   {copab 4268
This theorem is referenced by:  opabbii  4275  csbopabg  4286  xpeq1  4895  xpeq2  4896  opabbi2dv  5025  resopab2  5193  cores  5376  xpco  5417  dffn5  5775  f1oiso2  6075  f1ocnvd  6296  ofreq  6311  bropopvvv  6429  fnwelem  6464  sprmpt2  6479  wemapwe  7657  shftfval  11890  2shfti  11900  fsumrev  12567  fsumshft  12568  prdsval  13683  pwsle  13719  sectffval  13981  sectfval  13982  isfunc  14066  isfull  14112  isfth  14116  ipoval  14585  eqgfval  14993  dvdsrval  15755  dvdsrpropd  15806  ltbval  16537  opsrval  16540  lmfval  17301  pt1hmeo  17843  xkocnv  17851  tgphaus  18151  isphtpc  19024  bcthlem1  19282  bcth  19287  ulmval  20301  lgsquadlem3  21145  wlks  21531  wlkon  21535  trls  21541  trlon  21545  pths  21571  spths  21572  pthon  21580  spthon  21587  iseupa  21692  ajfval  22315  csbcnvg  24042  f1o3d  24046  mptcnv  24050  inftmrel  24255  isinftm  24256  metidval  24290  faeval  24602  fprodshft  25305  fprodrev  25306  fnopabeqd  26435  dnwech  27137  aomclem8  27150  dfafn5a  28014  wlkelwrd  28333  wlkcompim  28340  lcvfbr  29892  cmtfvalN  30082  cvrfval  30140  dicffval  32046  dicfval  32047  dicval  32048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-opab 4270
  Copyright terms: Public domain W3C validator