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

Theorem opabbidv 4082
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 1605 . 2  |-  F/ x ph
2 nfv 1605 . 2  |-  F/ y
ph
3 opabbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 2, 3opabbid 4081 1  |-  ( ph  ->  { <. x ,  y
>.  |  ps }  =  { <. x ,  y
>.  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   {copab 4076
This theorem is referenced by:  opabbii  4083  csbopabg  4094  xpeq1  4703  xpeq2  4704  opabbi2dv  4833  resopab2  4999  cores  5176  dffn5  5568  f1oiso2  5849  f1ocnvd  6066  ofreq  6081  fnwelem  6230  wemapwe  7400  shftfval  11565  2shfti  11575  fsumrev  12241  fsumshft  12242  prdsval  13355  pwsle  13391  sectffval  13653  sectfval  13654  isfunc  13738  isfull  13784  isfth  13788  ipoval  14257  eqgfval  14665  dvdsrval  15427  dvdsrpropd  15478  ltbval  16213  opsrval  16216  lmfval  16962  pt1hmeo  17497  xkocnv  17505  tgphaus  17799  isphtpc  18492  bcthlem1  18746  bcth  18751  ulmval  19759  lgsquadlem3  20595  ajfval  21387  mptcnv  23027  f1o3d  23037  csbcnvg  23198  iseupa  23881  dfoprab4pop  25037  isside0  26164  fnopabeqd  26385  dnwech  27145  aomclem8  27159  dfafn5a  28022  lcvfbr  29210  cmtfvalN  29400  cvrfval  29458  dicffval  31364  dicfval  31365  dicval  31366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-opab 4078
  Copyright terms: Public domain W3C validator