Theorem rabbi 3445

Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii 3421. (Contributed by NM, 25-Nov-2013.)

Assertion

Ref	Expression
rabbi	⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Proof of Theorem rabbi

Step	Hyp	Ref	Expression
1		abbib 2832	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
2		df-rab 3417	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3		df-rab 3417	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)}
4	2, 3	eqeq12i 2781	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)})
5		df-ral 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)))
6		pm5.32 584	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
7	6	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
8	5, 7	bitri 278	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
9	1, 4, 8	3bitr4ri 307	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2147  {cab 2741  ∀wral 3080  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rab 3417

This theorem is used by:  kqfeq  24098  isr0  24111  rabeq12f  39355  eq0rabdioph  44053  eqrabdioph  44054  lerabdioph  44078  eluzrabdioph  44079  ltrabdioph  44081  nerabdioph  44082  dvdsrabdioph  44083  undisjrab  45551  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  fourierdlem89  47478  fourierdlem91  47480  fourierdlem100  47489  fourierdlem108  47497  fourierdlem112  47501  ovn0  47849  issmfdmpt  48031  line2x  50197  line2y  50198