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

Theorem rabbiia 3477
Description: Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rabbiia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rabbiia {𝑥𝐴𝜑} = {𝑥𝐴𝜓}

Proof of Theorem rabbiia
StepHypRef Expression
1 rabbiia.1 . . . 4 (𝑥𝐴 → (𝜑𝜓))
21pm5.32i 575 . . 3 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32abbii 2890 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3151 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
5 df-rab 3151 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
63, 4, 53eqtr4i 2858 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wcel 2107  {cab 2803  {crab 3146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2804  df-cleq 2818  df-rab 3151
This theorem is referenced by:  rabbii  3478  fninfp  6931  fndifnfp  6933  nlimon  7557  dfom2  7573  rankval2  9239  ioopos  12806  prmreclem4  16247  acsfn1  16924  acsfn2  16926  logtayl  25158  ftalem3  25568  ppiub  25696  isuvtx  27093  vtxdginducedm1  27241  finsumvtxdg2size  27248  rgrusgrprc  27287  clwwlknclwwlkdif  27673  numclwwlkqhash  28070  ubthlem1  28563  xpinpreima  31037  xpinpreima2  31038  eulerpartgbij  31518  topdifinfeq  34502  rabimbieq  35383  rmydioph  39478  rmxdioph  39480  expdiophlem2  39486  expdioph  39487  alephiso3  39785  fsovrfovd  40222  k0004val0  40371  nzss  40516  hashnzfz  40519  fourierdlem90  42349  fourierdlem96  42355  fourierdlem97  42356  fourierdlem98  42357  fourierdlem99  42358  fourierdlem100  42359  fourierdlem109  42368  fourierdlem110  42369  fourierdlem112  42371  fourierdlem113  42372  sssmf  42883  dfodd6  43636  dfeven4  43637  dfeven2  43648  dfodd3  43649  dfeven3  43657  dfodd4  43658  dfodd5  43659
  Copyright terms: Public domain W3C validator