New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  rabbi GIF version

Theorem rabbi 2789
 Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 2850. (Contributed by NM, 25-Nov-2013.)
Assertion
Ref Expression
rabbi (x A (ψχ) ↔ {x A ψ} = {x A χ})

Proof of Theorem rabbi
StepHypRef Expression
1 abbi 2463 . 2 (x((x A ψ) ↔ (x A χ)) ↔ {x (x A ψ)} = {x (x A χ)})
2 df-ral 2619 . . 3 (x A (ψχ) ↔ x(x A → (ψχ)))
3 pm5.32 617 . . . 4 ((x A → (ψχ)) ↔ ((x A ψ) ↔ (x A χ)))
43albii 1566 . . 3 (x(x A → (ψχ)) ↔ x((x A ψ) ↔ (x A χ)))
52, 4bitri 240 . 2 (x A (ψχ) ↔ x((x A ψ) ↔ (x A χ)))
6 df-rab 2623 . . 3 {x A ψ} = {x (x A ψ)}
7 df-rab 2623 . . 3 {x A χ} = {x (x A χ)}
86, 7eqeq12i 2366 . 2 ({x A ψ} = {x A χ} ↔ {x (x A ψ)} = {x (x A χ)})
91, 5, 83bitr4i 268 1 (x A (ψχ) ↔ {x A ψ} = {x A χ})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  {crab 2618 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-ral 2619  df-rab 2623 This theorem is referenced by:  rabbidva  2850  fnpm  6008
 Copyright terms: Public domain W3C validator