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

Theorem opabbidv 4480
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 1751 . 2  |-  F/ x ph
2 nfv 1751 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4479 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   {copab 4474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-opab 4476
This theorem is referenced by:  opabbii  4481  csbopab  4744  csbopabgALT  4745  csbmpt12  4746  xpeq1  4859  xpeq2  4860  opabbi2dv  4995  csbcnvgALT  5030  resopab2  5164  mptcnv  5249  cores  5349  xpco  5387  dffn5  5917  f1oiso2  6249  f1ocnvd  6523  ofreq  6539  bropopvvv  6878  fnwelem  6913  sprmpt2d  6969  mpt2curryd  7015  wemapwe  8192  xpcogend  13006  shftfval  13101  2shfti  13111  prdsval  15305  pwsle  15342  sectffval  15599  sectfval  15600  isfunc  15713  isfull  15759  isfth  15763  ipoval  16344  eqgfval  16809  dvdsrval  17801  dvdsrpropd  17852  ltbval  18623  opsrval  18626  lmfval  20172  xkocnv  20753  tgphaus  21055  isphtpc  21911  bcthlem1  22178  bcth  22183  ulmval  23197  lgsquadlem3  24144  iscgrg  24417  legval  24486  ishlg  24504  perpln1  24609  perpln2  24610  isperp  24611  ishpg  24654  iscgra  24704  isinag  24729  wlks  25089  wlkcompim  25096  wlkelwrd  25100  wlkon  25103  trls  25108  trlon  25112  pths  25138  spths  25139  pthon  25147  spthon  25154  clwlk  25323  clwlkcompim  25334  iseupa  25535  ajfval  26292  f1o3d  28066  f1od2  28149  inftmrel  28332  isinftm  28333  metidval  28529  faeval  28905  eulerpartlemgvv  29032  eulerpart  29038  afsval  29273  fnopabeqd  31750  lcvfbr  32295  cmtfvalN  32485  cvrfval  32543  dicffval  34451  dicfval  34452  dicval  34453  dnwech  35616  aomclem8  35629  dfafn5a  38065
  Copyright terms: Public domain W3C validator