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

Theorem rabbi 3463
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 2805 . 2 ({𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)} ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
2 df-rab 3434 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
3 df-rab 3434 . . 3 {𝑥𝐴𝜒} = {𝑥 ∣ (𝑥𝐴𝜒)}
42, 3eqeq12i 2751 . 2 ({𝑥𝐴𝜓} = {𝑥𝐴𝜒} ↔ {𝑥 ∣ (𝑥𝐴𝜓)} = {𝑥 ∣ (𝑥𝐴𝜒)})
5 df-ral 3063 . . 3 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥(𝑥𝐴 → (𝜓𝜒)))
6 pm5.32 575 . . . 4 ((𝑥𝐴 → (𝜓𝜒)) ↔ ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
76albii 1822 . . 3 (∀𝑥(𝑥𝐴 → (𝜓𝜒)) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
85, 7bitri 275 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ ∀𝑥((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
91, 4, 83bitr4ri 304 1 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wcel 2107  {cab 2710  wral 3062  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-rab 3434
This theorem is referenced by:  rabbidaOLD  3471  kqfeq  23228  isr0  23241  rabeq12f  37025  eq0rabdioph  41514  eqrabdioph  41515  lerabdioph  41543  eluzrabdioph  41544  ltrabdioph  41546  nerabdioph  41547  dvdsrabdioph  41548  undisjrab  43065  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  fourierdlem89  44911  fourierdlem91  44913  fourierdlem100  44922  fourierdlem108  44930  fourierdlem112  44934  ovn0  45282  issmfdmpt  45464  line2x  47440  line2y  47441
  Copyright terms: Public domain W3C validator