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

Theorem opabbidv 4496
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 1692 . 2  |-  F/ x ph
2 nfv 1692 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4495 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1381   {copab 4490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-opab 4492
This theorem is referenced by:  opabbii  4497  csbopab  4765  csbopabgALT  4766  csbmpt12  4767  xpeq1  4999  xpeq2  5000  opabbi2dv  5138  csbcnvgALT  5173  resopab2  5308  mptcnv  5394  cores  5496  xpco  5533  dffn5  5899  f1oiso2  6229  f1ocnvd  6505  ofreq  6524  bropopvvv  6861  fnwelem  6896  sprmpt2d  6950  mpt2curryd  6996  wemapwe  8137  wemapweOLD  8138  shftfval  12877  2shfti  12887  prdsval  14724  pwsle  14761  sectffval  15017  sectfval  15018  isfunc  15102  isfull  15148  isfth  15152  ipoval  15653  eqgfval  16118  dvdsrval  17162  dvdsrpropd  17213  ltbval  18004  opsrval  18007  lmfval  19599  xkocnv  20181  tgphaus  20481  isphtpc  21360  bcthlem1  21629  bcth  21634  ulmval  22640  lgsquadlem3  23496  iscgrg  23769  legval  23836  ishlg  23851  perpln1  23952  perpln2  23953  isperp  23954  ishpg  23993  iscgra  24034  wlks  24384  wlkcompim  24391  wlkelwrd  24395  wlkon  24398  trls  24403  trlon  24407  pths  24433  spths  24434  pthon  24442  spthon  24449  clwlk  24618  clwlkcompim  24629  iseupa  24830  ajfval  25589  f1o3d  27336  f1od2  27412  inftmrel  27590  isinftm  27591  metidval  27735  faeval  28084  eulerpartlemgvv  28181  eulerpart  28187  afsval  28417  fnopabeqd  30178  dnwech  30962  aomclem8  30975  dfafn5a  32079  lcvfbr  34447  cmtfvalN  34637  cvrfval  34695  dicffval  36603  dicfval  36604  dicval  36605  xpcogend  37428
  Copyright terms: Public domain W3C validator