Theorem wl-dfcleq

Description: The defining characterization of class equality. It is proved, over Tarski's FOL, from the axiom of (set) extensionality ( ax-ext ) and the definition of class equality ( df-cleq ). Its forward implication is called "class extensionality". Remark: the proof uses axextb to prove also the hypothesis of df-cleq that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen , equid }. (Contributed by NM, 15-Sep-1993) (Revised by BJ, 24-Jun-2019) Base on wl-dfcleq.just . (Revised by Wolf Lammen, 7-Apr-2026)

	Ref	Expression
Assertion	wl-dfcleq	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
2		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
3	1 2	bibi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) )
4	3	cbvalvw	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
5		eqid	⊢ 𝐴 = 𝐴
6		eqtr	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐶 )
7	6	eqcomd	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐶 = 𝐴 )
8	7	ex	⊢ ( 𝐴 = 𝐵 → ( 𝐵 = 𝐶 → 𝐶 = 𝐴 ) )
9		eqeq2	⊢ ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ↔ 𝑥 = 𝐵 ) )
10	9	biimpd	⊢ ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 → 𝑥 = 𝐵 ) )
11	10	anim1d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
12	11	eximdv	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
13		dfclel	⊢ ( 𝐴 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
14		dfclel	⊢ ( 𝐵 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
15	12 13 14	3imtr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 → 𝐵 ∈ 𝐶 ) )
16		wl-dfcleq.basic	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
17		biimp	⊢ ( ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) )
18	17	alimi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) )
19	1	biimpd	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
20	19	eqcoms	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
21		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
22	21	biimpd	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 → 𝑥 ∈ 𝐵 ) )
23	20 22	imim12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
24	23	spimvw	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
25	18 24	syl	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
26	16 25	sylbi	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
27	26	anim2d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) )
28	27	eximdv	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) )
29		dfclel	⊢ ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) )
30		dfclel	⊢ ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) )
31	28 29 30	3imtr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )
32	4 5 8 15 31	wl-dfcleq.just	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )