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

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

Proof of Theorem rabbi
StepHypRef Expression
1 abbib 2811 . 2 ({𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)} ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
2 df-rab 3437 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
3 df-rab 3437 . . 3 {𝑥𝐴𝜒} = {𝑥 ∣ (𝑥𝐴𝜒)}
42, 3eqeq12i 2755 . 2 ({𝑥𝐴𝜓} = {𝑥𝐴𝜒} ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
5 df-ral 3062 . . 3 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥(𝑥𝐴 → (𝜓𝜒)))
6 pm5.32 573 . . . 4 ((𝑥𝐴 → (𝜓𝜒)) ↔ ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
76albii 1819 . . 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 1538   = wceq 1540  wcel 2108  {cab 2714  wral 3061  {crab 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-ral 3062  df-rab 3437
This theorem is referenced by:  rabbidaOLD  3477  kqfeq  23732  isr0  23745  rabeq12f  38164  eq0rabdioph  42787  eqrabdioph  42788  lerabdioph  42816  eluzrabdioph  42817  ltrabdioph  42819  nerabdioph  42820  dvdsrabdioph  42821  undisjrab  44325  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem89  46210  fourierdlem91  46212  fourierdlem100  46221  fourierdlem108  46229  fourierdlem112  46233  ovn0  46581  issmfdmpt  46763  line2x  48675  line2y  48676
  Copyright terms: Public domain W3C validator