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

Theorem rabbiia 3098
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 2591 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2816 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2816 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2496 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395    e. wcel 1819   {cab 2442   {crab 2811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-rab 2816
This theorem is referenced by:  dfepfr  4873  epfrc  4874  fndmdifcom  5993  fniniseg2  6011  fnniniseg2OLD  6012  fninfp  6099  fndifnfp  6101  bm2.5ii  6640  nlimon  6685  dfom2  6701  dfoi  7954  cantnffvalOLD  8099  oef1oOLD  8159  rankval2  8253  kmlem3  8549  alephsuc3  8972  ioopos  11626  hashbclem  12504  gcdcom  14169  gcdass  14194  prmreclem4  14448  acsfn0  15076  acsfn1  15077  acsfn2  15079  dprdvalOLD  17162  dfrhm2  17492  lbsextg  17934  mplvalOLD  18211  fctop2  19632  ordtrest2  19831  qtopres  20324  tsmsfbas  20751  shftmbl  22074  logtayl  23166  ftalem3  23473  ppiub  23604  rpvmasum  23836  usgrafilem1  24537  clwlknclwlkdifs  25086  numclwwlkovf2num  25211  ubthlem1  25912  fpwrelmapffslem  27705  xpinpreima  28041  xpinpreima2  28042  ordtrest2NEW  28058  aean  28377  eulerpartgbij  28486  orvcval2  28572  subfacp1lem6  28804  dvtanlem  30226  itg2addnclem2  30229  scottexf  30738  scott0f  30739  3anrabdioph  30878  3orrabdioph  30879  rexrabdioph  30889  2rexfrabdioph  30891  3rexfrabdioph  30892  4rexfrabdioph  30893  6rexfrabdioph  30894  7rexfrabdioph  30895  elnn0rabdioph  30898  elnnrabdioph  30902  rabren3dioph  30911  rmydioph  31118  rmxdioph  31120  expdiophlem2  31126  expdioph  31127  lcmcom  31361  lcmass  31380  nzss  31384  hashnzfz  31387  uzmptshftfval  31413  binomcxplemdvsum  31422  binomcxp  31424  dvnprod  31907  fourierdlem90  32140  fourierdlem96  32146  fourierdlem97  32147  fourierdlem98  32148  fourierdlem99  32149  fourierdlem100  32150  fourierdlem109  32159  fourierdlem110  32160  fourierdlem112  32162  fourierdlem113  32163  usgfislem1  32664  usgfisALTlem1  32668  glbconxN  35203
  Copyright terms: Public domain W3C validator