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	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
2		eleq1w	$$⊢x=y\to \left(x\in B\leftrightarrow y\in B\right)$$
3	1 2	bibi12d	$$⊢x=y\to \left(\left(x\in A\leftrightarrow x\in B\right)\leftrightarrow \left(y\in A\leftrightarrow y\in B\right)\right)$$
4	3	cbvalvw	$$⊢\forall x\left(x\in A\leftrightarrow x\in B\right)\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
5		eqid	$$⊢A=A$$
6		eqtr	$$⊢\left(A=B\wedge B=C\right)\to A=C$$
7	6	eqcomd	$$⊢\left(A=B\wedge B=C\right)\to C=A$$
8	7	ex	$$⊢A=B\to \left(B=C\to C=A\right)$$
9		eqeq2	$$⊢A=B\to \left(x=A\leftrightarrow x=B\right)$$
10	9	biimpd	$$⊢A=B\to \left(x=A\to x=B\right)$$
11	10	anim1d	$$⊢A=B\to \left(\left(x=A\wedge x\in C\right)\to \left(x=B\wedge x\in C\right)\right)$$
12	11	eximdv	$$⊢A=B\to \left(\exists x\left(x=A\wedge x\in C\right)\to \exists x\left(x=B\wedge x\in C\right)\right)$$
13		dfclel	$$⊢A\in C\leftrightarrow \exists x\left(x=A\wedge x\in C\right)$$
14		dfclel	$$⊢B\in C\leftrightarrow \exists x\left(x=B\wedge x\in C\right)$$
15	12 13 14	3imtr4g	$$⊢A=B\to \left(A\in C\to B\in C\right)$$
16		wl-dfcleq.basic	$$⊢A=B\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
17		biimp	$$⊢\left(y\in A\leftrightarrow y\in B\right)\to \left(y\in A\to y\in B\right)$$
18	17	alimi	$$⊢\forall y\left(y\in A\leftrightarrow y\in B\right)\to \forall y\left(y\in A\to y\in B\right)$$
19	1	biimpd	$$⊢x=y\to \left(x\in A\to y\in A\right)$$
20	19	eqcoms	$$⊢y=x\to \left(x\in A\to y\in A\right)$$
21		eleq1w	$$⊢y=x\to \left(y\in B\leftrightarrow x\in B\right)$$
22	21	biimpd	$$⊢y=x\to \left(y\in B\to x\in B\right)$$
23	20 22	imim12d	$$⊢y=x\to \left(\left(y\in A\to y\in B\right)\to \left(x\in A\to x\in B\right)\right)$$
24	23	spimvw	$$⊢\forall y\left(y\in A\to y\in B\right)\to \left(x\in A\to x\in B\right)$$
25	18 24	syl	$$⊢\forall y\left(y\in A\leftrightarrow y\in B\right)\to \left(x\in A\to x\in B\right)$$
26	16 25	sylbi	$$⊢A=B\to \left(x\in A\to x\in B\right)$$
27	26	anim2d	$$⊢A=B\to \left(\left(x=C\wedge x\in A\right)\to \left(x=C\wedge x\in B\right)\right)$$
28	27	eximdv	$$⊢A=B\to \left(\exists x\left(x=C\wedge x\in A\right)\to \exists x\left(x=C\wedge x\in B\right)\right)$$
29		dfclel	$$⊢C\in A\leftrightarrow \exists x\left(x=C\wedge x\in A\right)$$
30		dfclel	$$⊢C\in B\leftrightarrow \exists x\left(x=C\wedge x\in B\right)$$
31	28 29 30	3imtr4g	$$⊢A=B\to \left(C\in A\to C\in B\right)$$
32	4 5 8 15 31	wl-dfcleq.just	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$