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

Theorem rabbiia 2889
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 2499 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2658 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2658 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2417 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   {cab 2373   {crab 2653
This theorem is referenced by:  dfepfr  4508  epfrc  4509  bm2.5ii  4726  nlimon  4771  dfom2  4787  fndmdifcom  5774  fniniseg2  5792  fnniniseg2  5793  dfoi  7413  oef1o  7588  rankval2  7677  kmlem3  7965  alephsuc3  8388  ioopos  10919  hashbclem  11628  gcdcom  12947  gcdass  12972  prmreclem4  13214  acsfn0  13812  acsfn1  13813  acsfn2  13815  dfrhm2  15748  lbsextg  16161  ltbwe  16460  fctop2  16992  ordtrest2  17190  qtopres  17651  tsmsfbas  18078  shftmbl  19300  logtayl  20418  ftalem3  20724  ppiub  20855  rpvmasum  21087  usgrafilem1  21291  ubthlem1  22220  xpinpreima  24108  xpinpreima2  24109  aean  24389  orvcval2  24495  subfacp1lem6  24650  itg2addnclem2  25958  fninfp  26426  fndifnfp  26428  3anrabdioph  26532  3orrabdioph  26533  rexrabdioph  26545  2rexfrabdioph  26547  3rexfrabdioph  26548  4rexfrabdioph  26549  6rexfrabdioph  26550  7rexfrabdioph  26551  elnn0rabdioph  26554  elnnrabdioph  26558  rabren3dioph  26567  rmydioph  26776  rmxdioph  26778  expdiophlem2  26784  expdioph  26785  glbconxN  29492
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-rab 2658
  Copyright terms: Public domain W3C validator