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

Theorem rabbiia 3068
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 641 . . 3  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32abbii 2551 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2780 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2780 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2461 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   {cab 2407   {crab 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-rab 2780
This theorem is referenced by:  elneldisj  3787  elnelun  3788  dfepfr  4838  epfrc  4839  fndmdifcom  6002  fniniseg2  6020  fninfp  6106  fndifnfp  6108  bm2.5ii  6647  nlimon  6692  dfom2  6708  dfoi  8035  rankval2  8297  kmlem3  8589  alephsuc3  9012  ioopos  11718  hashbclem  12619  gcdcom  14483  gcdass  14512  lcmcom  14556  lcmass  14578  prmreclem4  14862  prmordvdslcmsOLDOLD  15020  acsfn0  15565  acsfn1  15566  acsfn2  15568  dfrhm2  17944  lbsextg  18384  fctop2  20018  ordtrest2  20218  qtopres  20711  tsmsfbas  21140  shftmbl  22490  logtayl  23603  ftalem3  23997  ppiub  24130  rpvmasum  24362  usgrafilem1  25137  clwlknclwlkdifs  25686  numclwwlkovf2num  25811  ubthlem1  26510  fpwrelmapffslem  28323  xpinpreima  28720  xpinpreima2  28721  ordtrest2NEW  28737  unelldsys  28988  rossros  29010  aean  29075  eulerpartgbij  29213  orvcval2  29299  subfacp1lem6  29916  topdifinfeq  31717  dvtanlemOLD  31955  itg2addnclem2  31958  scottexf  32375  scott0f  32376  glbconxN  32912  3anrabdioph  35594  3orrabdioph  35595  rexrabdioph  35606  2rexfrabdioph  35608  3rexfrabdioph  35609  4rexfrabdioph  35610  6rexfrabdioph  35611  7rexfrabdioph  35612  elnn0rabdioph  35615  elnnrabdioph  35619  rabren3dioph  35627  rmydioph  35839  rmxdioph  35841  expdiophlem2  35847  expdioph  35848  relintab  36159  nzss  36636  hashnzfz  36639  uzmptshftfval  36665  binomcxplemdvsum  36674  binomcxp  36676  dvnprod  37764  fourierdlem90  38000  fourierdlem96  38006  fourierdlem97  38007  fourierdlem98  38008  fourierdlem99  38009  fourierdlem100  38010  fourierdlem109  38019  fourierdlem110  38020  fourierdlem112  38022  fourierdlem113  38023  ovnsubadd  38298  hoidmv1lelem3  38319  hoidmvlelem3  38323  dfodd6  38637  dfeven4  38638  dfeven2  38649  dfodd3  38650  dfeven3  38657  dfodd4  38658  dfodd5  38659  usgfislem1  39375  usgfisALTlem1  39379
  Copyright terms: Public domain W3C validator