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

Theorem opabbii 4083
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 2283 . 2  |-  z  =  z
2 opabbii.1 . . . 4  |-  ( ph  <->  ps )
32a1i 10 . . 3  |-  ( z  =  z  ->  ( ph 
<->  ps ) )
43opabbidv 4082 . 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 1623   {copab 4076
This theorem is referenced by:  mptv  4112  fconstmpt  4732  xpundi  4741  xpundir  4742  inxp  4818  cnvco  4865  resopab  4996  opabresid  5003  cnvi  5085  cnvun  5086  cnvxp  5097  cnvcnv3  5123  coundi  5174  coundir  5175  mptun  5374  fvopab6  5621  cbvoprab1  5918  cbvoprab12  5920  dmoprabss  5929  mpt2mptx  5938  resoprab  5940  ov6g  5985  1st2val  6145  2nd2val  6146  dfoprab3s  6175  dfoprab3  6176  dfoprab4  6177  fsplit  6223  mapsncnv  6814  xpcomco  6952  marypha2lem2  7189  oemapso  7384  leweon  7639  r0weon  7640  compsscnv  7997  fpwwe  8268  ltrelxr  8886  ltxrlt  8893  ltxr  10457  shftidt2  11576  prdsle  13361  prdsless  13362  prdsleval  13376  gaorb  14761  efgcpbllema  15063  frgpuplem  15081  ltbval  16213  ltbwe  16214  opsrle  16217  opsrtoslem1  16225  opsrtoslem2  16226  dvdsrz  16440  pjfval2  16609  lmfval  16962  lmbr  16988  cnmptid  17355  lgsquadlem3  20595  dfadj2  22465  dmadjss  22467  cnvadj  22472  axcontlem2  24593  dmoprabss6  25035  domncnt  25282  ranncnt  25283  cmppar2  25972  cmppar  25973  isside0  26164  bosser  26167  fneer  26288  opropabco  26389  fgraphopab  27529  fgraphxp  27530  cmtfvalN  29400  cmtvalN  29401  cvrfval  29458  cvrval  29459  dicval2  31369
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