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

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

Proof of Theorem rabbi
StepHypRef Expression
1 abbi 2724 . 2 (∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)) ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
2 df-ral 2901 . . 3 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥(𝑥𝐴 → (𝜓𝜒)))
3 pm5.32 666 . . . 4 ((𝑥𝐴 → (𝜓𝜒)) ↔ ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
43albii 1737 . . 3 (∀𝑥(𝑥𝐴 → (𝜓𝜒)) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
52, 4bitri 263 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
6 df-rab 2905 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
7 df-rab 2905 . . 3 {𝑥𝐴𝜒} = {𝑥 ∣ (𝑥𝐴𝜒)}
86, 7eqeq12i 2624 . 2 ({𝑥𝐴𝜓} = {𝑥𝐴𝜒} ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
91, 5, 83bitr4i 291 1 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  {crab 2900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-rab 2905 This theorem is referenced by:  rabbidva  3163  kqfeq  21337  isr0  21350  bj-rabbida  32106  rabeq12f  33135  eq0rabdioph  36358  eqrabdioph  36359  lerabdioph  36387  eluzrabdioph  36388  ltrabdioph  36390  nerabdioph  36391  dvdsrabdioph  36392  undisjrab  37527  rabbida  38302  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  fourierdlem89  39088  fourierdlem91  39090  fourierdlem100  39099  fourierdlem108  39107  fourierdlem112  39111  ovn0  39456  issmfdmpt  39635
 Copyright terms: Public domain W3C validator