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 <-> A. x ( x e. A <-> x e. B ) )

Proof

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