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

Theorem rabbiia 2791
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 2408 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2565 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2565 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2326 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   {cab 2282   {crab 2560
This theorem is referenced by:  dfepfr  4394  epfrc  4395  bm2.5ii  4613  nlimon  4658  dfom2  4674  fndmdifcom  5646  fniniseg2  5664  fnniniseg2  5665  dfoi  7242  oef1o  7417  rankval2  7506  kmlem3  7794  alephsuc3  8218  ioopos  10742  hashbclem  11406  gcdcom  12715  gcdass  12740  prmreclem4  12982  acsfn0  13578  acsfn1  13579  acsfn2  13581  dfrhm2  15514  lbsextg  15931  ltbwe  16230  fctop2  16758  ordtrest2  16950  qtopres  17405  tsmsfbas  17826  shftmbl  18912  logtayl  20023  ftalem3  20328  ppiub  20459  rpvmasum  20691  ubthlem1  21465  xpinpreima  23305  xpinpreima2  23306  orvcval2  23674  subfacp1lem6  23731  itg2addnclem2  25004  fninfp  26857  fndifnfp  26859  3anrabdioph  26965  3orrabdioph  26966  rexrabdioph  26978  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  elnn0rabdioph  26987  elnnrabdioph  26991  rabren3dioph  27001  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  glbconxN  30189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-rab 2565
  Copyright terms: Public domain W3C validator