Theorem rabbi 3430

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

Assertion

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

Proof of Theorem rabbi

Step	Hyp	Ref	Expression
1		abbib 2806	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)} ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
2		df-rab 3401	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3		df-rab 3401	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)}
4	2, 3	eqeq12i 2755	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜒)})
5		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)))
6		pm5.32 573	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
7	6	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜓 ↔ 𝜒)) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
8	5, 7	bitri 275	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
9	1, 4, 8	3bitr4ri 304	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  {crab 3400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rab 3401

This theorem is referenced by:  rabbidaOLD  3438  kqfeq  23672  isr0  23685  rabeq12f  38329  eq0rabdioph  43054  eqrabdioph  43055  lerabdioph  43083  eluzrabdioph  43084  ltrabdioph  43086  nerabdioph  43087  dvdsrabdioph  43088  undisjrab  44583  ioodvbdlimc1lem2  46212  ioodvbdlimc2lem  46214  fourierdlem89  46475  fourierdlem91  46477  fourierdlem100  46486  fourierdlem108  46494  fourierdlem112  46498  ovn0  46846  issmfdmpt  47028  line2x  49036  line2y  49037