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

Theorem rabbiia 2778
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 618 . . 3  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32abbii 2395 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2552 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2552 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2313 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   {cab 2269   {crab 2547
This theorem is referenced by:  dfepfr  4378  epfrc  4379  bm2.5ii  4597  nlimon  4642  dfom2  4658  fndmdifcom  5630  fniniseg2  5648  fnniniseg2  5649  dfoi  7226  oef1o  7401  rankval2  7490  kmlem3  7778  alephsuc3  8202  ioopos  10726  hashbclem  11390  gcdcom  12699  gcdass  12724  prmreclem4  12966  acsfn0  13562  acsfn1  13563  acsfn2  13565  dfrhm2  15498  lbsextg  15915  ltbwe  16214  fctop2  16742  ordtrest2  16934  qtopres  17389  tsmsfbas  17810  shftmbl  18896  logtayl  20007  ftalem3  20312  ppiub  20443  rpvmasum  20675  ubthlem1  21449  xpinpreima  23290  xpinpreima2  23291  orvcval2  23659  subfacp1lem6  23716  fninfp  26754  fndifnfp  26756  3anrabdioph  26862  3orrabdioph  26863  rexrabdioph  26875  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  elnn0rabdioph  26884  elnnrabdioph  26888  rabren3dioph  26898  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  expdioph  27116  glbconxN  29567
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-rab 2552
  Copyright terms: Public domain W3C validator