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

Theorem opabbii 4232
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
Hypothesis
Ref Expression
opabbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
opabbii  |-  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps }

Proof of Theorem opabbii
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 eqid 2404 . 2  |-  z  =  z
2 opabbii.1 . . . 4  |-  ( ph  <->  ps )
32a1i 11 . . 3  |-  ( z  =  z  ->  ( ph 
<->  ps ) )
43opabbidv 4231 . 2  |-  ( z  =  z  ->  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps } )
51, 4ax-mp 8 1  |-  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649   {copab 4225
This theorem is referenced by:  mptv  4261  fconstmpt  4880  xpundi  4889  xpundir  4890  inxp  4966  cnvco  5015  resopab  5146  opabresid  5153  cnvi  5235  cnvun  5236  cnvxp  5249  cnvcnv3  5279  coundi  5330  coundir  5331  mptun  5534  fvopab6  5785  cbvoprab1  6103  cbvoprab12  6105  dmoprabss  6114  mpt2mptx  6123  resoprab  6125  ov6g  6170  1st2val  6331  2nd2val  6332  dfoprab3s  6361  dfoprab3  6362  dfoprab4  6363  fsplit  6410  mapsncnv  7019  xpcomco  7157  marypha2lem2  7399  oemapso  7594  leweon  7849  r0weon  7850  compsscnv  8207  fpwwe  8477  ltrelxr  9095  ltxrlt  9102  ltxr  10671  shftidt2  11851  prdsle  13639  prdsless  13640  prdsleval  13654  gaorb  15039  efgcpbllema  15341  frgpuplem  15359  ltbval  16487  ltbwe  16488  opsrle  16491  opsrtoslem1  16499  opsrtoslem2  16500  dvdsrz  16722  pjfval2  16891  lmfval  17250  lmbr  17276  cnmptid  17646  lgsquadlem3  21093  wlks  21479  trls  21489  dfconngra1  21611  dfadj2  23341  dmadjss  23343  cnvadj  23348  dfid4  25136  axcontlem2  25808  fneer  26258  opropabco  26315  fgraphopab  27397  fgraphxp  27398  cmtfvalN  29693  cmtvalN  29694  cvrfval  29751  cvrval  29752  dicval2  31662
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