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

Theorem rabbiia 3097
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 637 . . 3  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32abbii 2596 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2818 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2818 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2501 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   {cab 2447   {crab 2813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-rab 2818
This theorem is referenced by:  dfepfr  4859  epfrc  4860  fndmdifcom  5979  fniniseg2  5997  fnniniseg2OLD  5998  fninfp  6081  fndifnfp  6083  bm2.5ii  6614  nlimon  6659  dfom2  6675  dfoi  7927  cantnffvalOLD  8073  oef1oOLD  8133  rankval2  8227  kmlem3  8523  alephsuc3  8946  ioopos  11592  hashbclem  12456  gcdcom  14008  gcdass  14033  prmreclem4  14287  acsfn0  14906  acsfn1  14907  acsfn2  14909  dprdvalOLD  16822  dfrhm2  17145  lbsextg  17586  mplvalOLD  17851  fctop2  19267  ordtrest2  19466  qtopres  19929  tsmsfbas  20356  shftmbl  21679  logtayl  22764  ftalem3  23071  ppiub  23202  rpvmasum  23434  usgrafilem1  24075  clwlknclwlkdifs  24624  numclwwlkovf2num  24750  ubthlem1  25450  fpwrelmapffslem  27215  xpinpreima  27512  xpinpreima2  27513  ordtrest2NEW  27529  aean  27844  eulerpartgbij  27939  orvcval2  28025  subfacp1lem6  28257  dvtanlem  29630  itg2addnclem2  29633  scottexf  30169  scott0f  30170  3anrabdioph  30309  3orrabdioph  30310  rexrabdioph  30320  2rexfrabdioph  30322  3rexfrabdioph  30323  4rexfrabdioph  30324  6rexfrabdioph  30325  7rexfrabdioph  30326  elnn0rabdioph  30329  elnnrabdioph  30333  rabren3dioph  30342  rmydioph  30551  rmxdioph  30553  expdiophlem2  30559  expdioph  30560  fourierdlem90  31454  fourierdlem96  31460  fourierdlem97  31461  fourierdlem98  31462  fourierdlem99  31463  fourierdlem100  31464  fourierdlem109  31473  fourierdlem110  31474  fourierdlem112  31476  fourierdlem113  31477  usgfislem1  31840  glbconxN  34051
  Copyright terms: Public domain W3C validator