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

Theorem rabbiia 3048
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 635 . . 3  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32abbii 2536 . 2  |-  { x  |  ( x  e.  A  /\  ph ) }  =  { x  |  ( x  e.  A  /\  ps ) }
4 df-rab 2763 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
5 df-rab 2763 . 2  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
63, 4, 53eqtr4i 2441 1  |-  { x  e.  A  |  ph }  =  { x  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1405    e. wcel 1842   {cab 2387   {crab 2758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-rab 2763
This theorem is referenced by:  dfepfr  4808  epfrc  4809  fndmdifcom  5970  fniniseg2  5988  fnniniseg2OLD  5989  fninfp  6078  fndifnfp  6080  bm2.5ii  6624  nlimon  6669  dfom2  6685  dfoi  7970  cantnffvalOLD  8114  oef1oOLD  8174  rankval2  8268  kmlem3  8564  alephsuc3  8987  ioopos  11655  hashbclem  12550  gcdcom  14367  gcdass  14392  prmreclem4  14646  acsfn0  15274  acsfn1  15275  acsfn2  15277  dprdvalOLD  17356  dfrhm2  17686  lbsextg  18128  mplvalOLD  18405  fctop2  19798  ordtrest2  19998  qtopres  20491  tsmsfbas  20918  shftmbl  22241  logtayl  23335  ftalem3  23729  ppiub  23860  rpvmasum  24092  usgrafilem1  24828  clwlknclwlkdifs  25377  numclwwlkovf2num  25502  ubthlem1  26200  fpwrelmapffslem  28002  xpinpreima  28341  xpinpreima2  28342  ordtrest2NEW  28358  unelldsys  28606  rossros  28628  aean  28693  eulerpartgbij  28817  orvcval2  28903  subfacp1lem6  29482  topdifinfeq  31267  dvtanlemOLD  31437  itg2addnclem2  31440  scottexf  31858  scott0f  31859  glbconxN  32395  3anrabdioph  35077  3orrabdioph  35078  rexrabdioph  35089  2rexfrabdioph  35091  3rexfrabdioph  35092  4rexfrabdioph  35093  6rexfrabdioph  35094  7rexfrabdioph  35095  elnn0rabdioph  35098  elnnrabdioph  35102  rabren3dioph  35110  rmydioph  35318  rmxdioph  35320  expdiophlem2  35326  expdioph  35327  lcmcom  36047  lcmass  36066  nzss  36070  hashnzfz  36073  uzmptshftfval  36099  binomcxplemdvsum  36108  binomcxp  36110  dvnprod  37114  fourierdlem90  37347  fourierdlem96  37353  fourierdlem97  37354  fourierdlem98  37355  fourierdlem99  37356  fourierdlem100  37357  fourierdlem109  37366  fourierdlem110  37367  fourierdlem112  37369  fourierdlem113  37370  dfodd6  37720  dfeven4  37721  dfeven2  37732  dfodd3  37733  dfeven3  37740  dfodd4  37741  dfodd5  37742  usgfislem1  38073  usgfisALTlem1  38077
  Copyright terms: Public domain W3C validator