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	$$⊢\underset{\_}{Ⅎ}xA$$
	cleqf.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	cleqf	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cleqf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		cleqf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		dfcleq	$$⊢A=B\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
4		nfv	$$⊢Ⅎy\left(x\in A\leftrightarrow x\in B\right)$$
5	1	nfcri	$$⊢Ⅎxy\in A$$
6	2	nfcri	$$⊢Ⅎxy\in B$$
7	5 6	nfbi	$$⊢Ⅎx\left(y\in A\leftrightarrow y\in B\right)$$
8		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
9		eleq1w	$$⊢x=y\to \left(x\in B\leftrightarrow y\in B\right)$$
10	8 9	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)$$
11	4 7 10	cbvalv1	$$⊢\forall x\left(x\in A\leftrightarrow x\in B\right)\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
12	3 11	bitr4i	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$