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

Theorem rabbiia 2938
Description: Equivalent wff's yield equal restricted class abstractions (inference rule). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rabbiia.1  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rabbiia  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }

Proof of Theorem rabbiia
StepHypRef Expression
1 rabbiia.1 . . . 4  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
21pm5.32i 619 . . 3  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32abbii 2547 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2706 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2706 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2465 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   {cab 2421   {crab 2701
This theorem is referenced by:  dfepfr  4559  epfrc  4560  bm2.5ii  4778  nlimon  4823  dfom2  4839  fndmdifcom  5827  fniniseg2  5845  fnniniseg2  5846  dfoi  7472  oef1o  7647  rankval2  7736  kmlem3  8024  alephsuc3  8447  ioopos  10979  hashbclem  11693  gcdcom  13012  gcdass  13037  prmreclem4  13279  acsfn0  13877  acsfn1  13878  acsfn2  13880  dfrhm2  15813  lbsextg  16226  ltbwe  16525  fctop2  17061  ordtrest2  17260  qtopres  17722  tsmsfbas  18149  shftmbl  19425  logtayl  20543  ftalem3  20849  ppiub  20980  rpvmasum  21212  usgrafilem1  21417  ubthlem1  22364  xpinpreima  24296  xpinpreima2  24297  aean  24587  orvcval2  24708  subfacp1lem6  24863  itg2addnclem2  26247  fninfp  26726  fndifnfp  26728  3anrabdioph  26832  3orrabdioph  26833  rexrabdioph  26845  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  elnn0rabdioph  26854  elnnrabdioph  26858  rabren3dioph  26867  rmydioph  27076  rmxdioph  27078  expdiophlem2  27084  expdioph  27085  glbconxN  30112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-rab 2706
  Copyright terms: Public domain W3C validator