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

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

Proof of Theorem rabbi
StepHypRef Expression
1 abbib 2809 . 2 ({𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)} ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
2 df-rab 3434 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
3 df-rab 3434 . . 3 {𝑥𝐴𝜒} = {𝑥 ∣ (𝑥𝐴𝜒)}
42, 3eqeq12i 2753 . 2 ({𝑥𝐴𝜓} = {𝑥𝐴𝜒} ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
5 df-ral 3060 . . 3 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥(𝑥𝐴 → (𝜓𝜒)))
6 pm5.32 573 . . . 4 ((𝑥𝐴 → (𝜓𝜒)) ↔ ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
76albii 1816 . . 3 (∀𝑥(𝑥𝐴 → (𝜓𝜒)) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
85, 7bitri 275 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
91, 4, 83bitr4ri 304 1 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535   = wceq 1537  wcel 2106  {cab 2712  wral 3059  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-ral 3060  df-rab 3434
This theorem is referenced by:  rabbidaOLD  3475  kqfeq  23748  isr0  23761  rabeq12f  38144  eq0rabdioph  42764  eqrabdioph  42765  lerabdioph  42793  eluzrabdioph  42794  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  undisjrab  44302  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  fourierdlem89  46151  fourierdlem91  46153  fourierdlem100  46162  fourierdlem108  46170  fourierdlem112  46174  ovn0  46522  issmfdmpt  46704  line2x  48604  line2y  48605
  Copyright terms: Public domain W3C validator