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

Theorem rabbiia 3333
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 570 . . 3 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32abbii 2882 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑥 ∣ (𝑥𝐴𝜓)}
4 df-rab 3064 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
5 df-rab 3064 . 2 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
63, 4, 53eqtr4i 2797 1 {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  {cab 2751  {crab 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-rab 3064
This theorem is referenced by:  rabbii  3334  elneldisjOLD  4129  elnelunOLD  4130  fninfp  6635  fndifnfp  6637  nlimon  7251  dfom2  7267  rankval2  8898  ioopos  12455  prmreclem4  15905  acsfn1  16590  acsfn2  16592  logtayl  24700  ftalem3  25095  ppiub  25223  isuvtx  26581  vtxdginducedm1  26733  finsumvtxdg2size  26740  rgrusgrprc  26779  clwwlknclwwlkdif  27207  clwwlknclwwlkdifsOLD  27209  numclwwlkqhash  27682  ubthlem1  28185  xpinpreima  30402  xpinpreima2  30403  eulerpartgbij  30884  topdifinfeq  33634  rabimbieq  34454  rmydioph  38261  rmxdioph  38263  expdiophlem2  38269  expdioph  38270  fsovrfovd  38980  k0004val0  39129  nzss  39193  hashnzfz  39196  fourierdlem90  41053  fourierdlem96  41059  fourierdlem97  41060  fourierdlem98  41061  fourierdlem99  41062  fourierdlem100  41063  fourierdlem109  41072  fourierdlem110  41073  fourierdlem112  41075  fourierdlem113  41076  sssmf  41590  dfodd6  42229  dfeven4  42230  dfeven2  42241  dfodd3  42242  dfeven3  42249  dfodd4  42250  dfodd5  42251
  Copyright terms: Public domain W3C validator