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

Theorem opabbidv 4231
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 1626 . 2  |-  F/ x ph
2 nfv 1626 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4230 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   {copab 4225
This theorem is referenced by:  opabbii  4232  csbopabg  4243  xpeq1  4851  xpeq2  4852  opabbi2dv  4981  resopab2  5149  cores  5332  xpco  5373  dffn5  5731  f1oiso2  6031  f1ocnvd  6252  ofreq  6267  bropopvvv  6385  fnwelem  6420  sprmpt2  6435  wemapwe  7610  shftfval  11840  2shfti  11850  fsumrev  12517  fsumshft  12518  prdsval  13633  pwsle  13669  sectffval  13931  sectfval  13932  isfunc  14016  isfull  14062  isfth  14066  ipoval  14535  eqgfval  14943  dvdsrval  15705  dvdsrpropd  15756  ltbval  16487  opsrval  16490  lmfval  17250  pt1hmeo  17791  xkocnv  17799  tgphaus  18099  isphtpc  18972  bcthlem1  19230  bcth  19235  ulmval  20249  lgsquadlem3  21093  wlks  21479  wlkon  21483  trls  21489  trlon  21493  pths  21519  spths  21520  pthon  21528  spthon  21535  iseupa  21640  ajfval  22263  csbcnvg  23990  f1o3d  23994  mptcnv  23998  inftmrel  24203  isinftm  24204  metidval  24238  faeval  24550  fprodshft  25253  fprodrev  25254  fnopabeqd  26311  dnwech  27013  aomclem8  27027  dfafn5a  27891  lcvfbr  29503  cmtfvalN  29693  cvrfval  29751  dicffval  31657  dicfval  31658  dicval  31659
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-opab 4227
  Copyright terms: Public domain W3C validator