Theorem cleqf

Description: Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions as in dfcleq . See also cleqh . (Contributed by NM, 26-May-1993) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 17-Nov-2019) Avoid ax-13 . (Revised by Wolf Lammen, 10-May-2023) Avoid ax-10 . (Revised by Gino Giotto, 20-Aug-2023)

	Ref	Expression
Hypotheses	cleqf.1	|- F/_ x A
	cleqf.2	|- F/_ x B
Assertion	cleqf	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		cleqf.1	|- F/_ x A
2		cleqf.2	|- F/_ x B
3		dfcleq	|- ( A = B <-> A. y ( y e. A <-> y e. B ) )
4		nfv	|- F/ y ( x e. A <-> x e. B )
5	1	nfcri	|- F/ x y e. A
6	2	nfcri	|- F/ x y e. B
7	5 6	nfbi	|- F/ x ( y e. A <-> y e. B )
8		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
9		eleq1w	|- ( x = y -> ( x e. B <-> y e. B ) )
10	8 9	bibi12d	|- ( x = y -> ( ( x e. A <-> x e. B ) <-> ( y e. A <-> y e. B ) ) )
11	4 7 10	cbvalv1	|- ( A. x ( x e. A <-> x e. B ) <-> A. y ( y e. A <-> y e. B ) )
12	3 11	bitr4i	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )