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

Theorem rabbiia 3059
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 2585 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2804 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2804 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2490 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    e. wcel 1758   {cab 2436   {crab 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-rab 2804
This theorem is referenced by:  dfepfr  4805  epfrc  4806  fndmdifcom  5909  fniniseg2  5927  fnniniseg2OLD  5928  fninfp  6006  fndifnfp  6008  bm2.5ii  6519  nlimon  6564  dfom2  6580  dfoi  7828  cantnffvalOLD  7974  oef1oOLD  8034  rankval2  8128  kmlem3  8424  alephsuc3  8847  ioopos  11475  hashbclem  12309  gcdcom  13808  gcdass  13833  prmreclem4  14084  acsfn0  14702  acsfn1  14703  acsfn2  14705  dprdvalOLD  16594  dfrhm2  16916  lbsextg  17351  mplvalOLD  17611  fctop2  18727  ordtrest2  18926  qtopres  19389  tsmsfbas  19816  shftmbl  21138  logtayl  22223  ftalem3  22530  ppiub  22661  rpvmasum  22893  usgrafilem1  23461  ubthlem1  24408  fpwrelmapffslem  26168  xpinpreima  26472  xpinpreima2  26473  ordtrest2NEW  26489  aean  26796  eulerpartgbij  26891  orvcval2  26977  subfacp1lem6  27209  dvtanlem  28581  itg2addnclem2  28584  scottexf  29120  scott0f  29121  3anrabdioph  29261  3orrabdioph  29262  rexrabdioph  29272  2rexfrabdioph  29274  3rexfrabdioph  29275  4rexfrabdioph  29276  6rexfrabdioph  29277  7rexfrabdioph  29278  elnn0rabdioph  29281  elnnrabdioph  29285  rabren3dioph  29294  rmydioph  29503  rmxdioph  29505  expdiophlem2  29511  expdioph  29512  clwlknclwlkdifs  30718  numclwwlkovf2num  30818  dmatsubcl  31033  glbconxN  33330
  Copyright terms: Public domain W3C validator