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

Theorem rabbi 3295
Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3388. (Contributed by NM, 25-Nov-2013.)
Assertion
Ref Expression
rabbi (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})

Proof of Theorem rabbi
StepHypRef Expression
1 abbi 2810 . 2 (∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)) ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
2 df-ral 3066 . . 3 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥(𝑥𝐴 → (𝜓𝜒)))
3 pm5.32 577 . . . 4 ((𝑥𝐴 → (𝜓𝜒)) ↔ ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
43albii 1827 . . 3 (∀𝑥(𝑥𝐴 → (𝜓𝜒)) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
52, 4bitri 278 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
6 df-rab 3070 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
7 df-rab 3070 . . 3 {𝑥𝐴𝜒} = {𝑥 ∣ (𝑥𝐴𝜒)}
86, 7eqeq12i 2755 . 2 ({𝑥𝐴𝜓} = {𝑥𝐴𝜒} ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
91, 5, 83bitr4i 306 1 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1541   = wceq 1543  wcel 2110  {cab 2714  wral 3061  {crab 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-ral 3066  df-rab 3070
This theorem is referenced by:  rabbida  3384  rabbidvaOLD  3389  kqfeq  22621  isr0  22634  rabeq12f  36052  eq0rabdioph  40301  eqrabdioph  40302  lerabdioph  40330  eluzrabdioph  40331  ltrabdioph  40333  nerabdioph  40334  dvdsrabdioph  40335  undisjrab  41597  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  fourierdlem89  43411  fourierdlem91  43413  fourierdlem100  43422  fourierdlem108  43430  fourierdlem112  43434  ovn0  43779  issmfdmpt  43956  line2x  45773  line2y  45774
  Copyright terms: Public domain W3C validator