Theorem wl-dfcleq

Description: The defining characterization of class equality. This version of df-cleq has no restrictions, unlike the forms on which it is based. It is proved in Tarski's FOL from the axiom of extensionality ( ax-ext ), the definition of class equality ( df-cleq ), and the definition of class membership ( df-clel ).

Its forward implication is known as "class extensionality". (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 ) )