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

Theorem opabbidv 4161
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 1619 . 2  |-  F/ x ph
2 nfv 1619 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4160 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642   {copab 4155
This theorem is referenced by:  opabbii  4162  csbopabg  4173  xpeq1  4782  xpeq2  4783  opabbi2dv  4912  resopab2  5078  cores  5255  dffn5  5648  f1oiso2  5933  f1ocnvd  6150  ofreq  6165  fnwelem  6314  wemapwe  7487  shftfval  11655  2shfti  11665  fsumrev  12332  fsumshft  12333  prdsval  13448  pwsle  13484  sectffval  13746  sectfval  13747  isfunc  13831  isfull  13877  isfth  13881  ipoval  14350  eqgfval  14758  dvdsrval  15520  dvdsrpropd  15571  ltbval  16306  opsrval  16309  lmfval  17062  pt1hmeo  17597  xkocnv  17605  tgphaus  17895  isphtpc  18590  bcthlem1  18844  bcth  18849  ulmval  19857  lgsquadlem3  20701  ajfval  21495  csbcnvg  23234  f1o3d  23242  mptcnv  23246  xpco  23525  faeval  23861  iseupa  24285  fprodshft  24601  fprodrev  24602  fnopabeqd  25709  dnwech  26468  aomclem8  26482  dfafn5a  27348  bropopvvv  27432  sprmpt2  27445  wlks  27661  wlkon  27665  trls  27671  trlon  27675  pths  27691  spths  27692  pthon  27700  lcvfbr  29262  cmtfvalN  29452  cvrfval  29510  dicffval  31416  dicfval  31417  dicval  31418
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-opab 4157
  Copyright terms: Public domain W3C validator