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

Theorem rabbiia 3385
 Description: Equivalent formulas 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 578 . . 3 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32abbii 2824 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3080 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
5 df-rab 3080 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
63, 4, 53eqtr4i 2792 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539   ∈ wcel 2112  {cab 2736  {crab 3075 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-rab 3080 This theorem is referenced by:  rabbii  3386  fninfp  6934  fndifnfp  6936  nlimon  7572  dfom2  7588  rankval2  9294  ioopos  12870  prmreclem4  16325  acsfn1  17005  acsfn2  17007  logtayl  25365  ftalem3  25774  ppiub  25902  isuvtx  27299  vtxdginducedm1  27447  finsumvtxdg2size  27454  rgrusgrprc  27493  clwwlknclwwlkdif  27878  numclwwlkqhash  28274  ubthlem1  28767  xpinpreima  31391  xpinpreima2  31392  eulerpartgbij  31872  topdifinfeq  35083  rabimbieq  35989  rmydioph  40374  rmxdioph  40376  expdiophlem2  40382  expdioph  40383  alephiso3  40677  fsovrfovd  41129  k0004val0  41276  nzss  41440  hashnzfz  41443  fourierdlem90  43250  fourierdlem96  43256  fourierdlem97  43257  fourierdlem98  43258  fourierdlem99  43259  fourierdlem100  43260  fourierdlem109  43269  fourierdlem110  43270  fourierdlem112  43272  fourierdlem113  43273  sssmf  43784  dfodd6  44582  dfeven4  44583  dfeven2  44594  dfodd3  44595  dfeven3  44603  dfodd4  44604  dfodd5  44605
 Copyright terms: Public domain W3C validator