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

Theorem opabbii 4275
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 2438 . 2  |-  z  =  z
2 opabbii.1 . . . 4  |-  ( ph  <->  ps )
32a1i 11 . . 3  |-  ( z  =  z  ->  ( ph 
<->  ps ) )
43opabbidv 4274 . 2  |-  ( z  =  z  ->  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps } )
51, 4ax-mp 5 1  |-  { <. x ,  y >.  |  ph }  =  { <. x ,  y >.  |  ps }
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653   {copab 4268
This theorem is referenced by:  mptv  4304  fconstmpt  4924  xpundi  4933  xpundir  4934  inxp  5010  cnvco  5059  resopab  5190  opabresid  5197  cnvi  5279  cnvun  5280  cnvxp  5293  cnvcnv3  5323  coundi  5374  coundir  5375  mptun  5578  fvopab6  5829  cbvoprab1  6147  cbvoprab12  6149  dmoprabss  6158  mpt2mptx  6167  resoprab  6169  ov6g  6214  1st2val  6375  2nd2val  6376  dfoprab3s  6405  dfoprab3  6406  dfoprab4  6407  fsplit  6454  mapsncnv  7063  xpcomco  7201  marypha2lem2  7444  oemapso  7641  leweon  7898  r0weon  7899  compsscnv  8256  fpwwe  8526  ltrelxr  9144  ltxrlt  9151  ltxr  10720  shftidt2  11901  prdsle  13689  prdsless  13690  prdsleval  13704  gaorb  15089  efgcpbllema  15391  frgpuplem  15409  ltbval  16537  ltbwe  16538  opsrle  16541  opsrtoslem1  16549  opsrtoslem2  16550  dvdsrz  16772  pjfval2  16941  lmfval  17301  lmbr  17327  cnmptid  17698  lgsquadlem3  21145  wlks  21531  trls  21541  dfconngra1  21663  dfadj2  23393  dmadjss  23395  cnvadj  23400  dfid4  25188  axcontlem2  25909  fneer  26382  opropabco  26439  fgraphopab  27520  fgraphxp  27521  cmtfvalN  30082  cmtvalN  30083  cvrfval  30140  cvrval  30141  dicval2  32051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-opab 4270
  Copyright terms: Public domain W3C validator