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

Theorem opabbii 4162
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 2358 . 2  |-  z  =  z
2 opabbii.1 . . . 4  |-  ( ph  <->  ps )
32a1i 10 . . 3  |-  ( z  =  z  ->  ( ph 
<->  ps ) )
43opabbidv 4161 . 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 176    = wceq 1642   {copab 4155
This theorem is referenced by:  mptv  4191  fconstmpt  4811  xpundi  4820  xpundir  4821  inxp  4897  cnvco  4944  resopab  5075  opabresid  5082  cnvi  5164  cnvun  5165  cnvxp  5176  cnvcnv3  5202  coundi  5253  coundir  5254  mptun  5453  fvopab6  5701  cbvoprab1  6002  cbvoprab12  6004  dmoprabss  6013  mpt2mptx  6022  resoprab  6024  ov6g  6069  1st2val  6229  2nd2val  6230  dfoprab3s  6259  dfoprab3  6260  dfoprab4  6261  fsplit  6307  mapsncnv  6899  xpcomco  7037  marypha2lem2  7276  oemapso  7471  leweon  7726  r0weon  7727  compsscnv  8084  fpwwe  8355  ltrelxr  8973  ltxrlt  8980  ltxr  10546  shftidt2  11666  prdsle  13454  prdsless  13455  prdsleval  13469  gaorb  14854  efgcpbllema  15156  frgpuplem  15174  ltbval  16306  ltbwe  16307  opsrle  16310  opsrtoslem1  16318  opsrtoslem2  16319  dvdsrz  16540  pjfval2  16709  lmfval  17062  lmbr  17088  cnmptid  17455  lgsquadlem3  20701  dfadj2  22573  dmadjss  22575  cnvadj  22580  dfid4  24484  axcontlem2  25152  fneer  25612  opropabco  25713  fgraphopab  26852  fgraphxp  26853  wlks  27661  trls  27671  dfconngra1  27778  cmtfvalN  29452  cmtvalN  29453  cvrfval  29510  cvrval  29511  dicval2  31421
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