Theorem cbvexeqsetf

Description: The expression E. x x = A means " A is a set" even if A contains x as a bound variable. This lemma helps minimizing axiom or df-clab usage in some cases. Extracted from the proof of issetft . (Contributed by Wolf Lammen, 30-Jul-2025)

	Ref	Expression
Assertion	cbvexeqsetf	$$⊢\underset{\_}{Ⅎ}xA\to \left(\exists xx=A\leftrightarrow \exists yy=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xA$$
2		nfv	$$⊢Ⅎy\underset{\_}{Ⅎ}xA$$
3		nfvd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎy\neg x=A$$
4		nfcvd	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xy$$
5		id	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xA$$
6	4 5	nfeqd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy=A$$
7	6	nfnd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎx\neg y=A$$
8		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
9	8	notbid	$$⊢x=y\to \left(\neg x=A\leftrightarrow \neg y=A\right)$$
10	9	a1i	$$⊢\underset{\_}{Ⅎ}xA\to \left(x=y\to \left(\neg x=A\leftrightarrow \neg y=A\right)\right)$$
11	1 2 3 7 10	cbv2w	$$⊢\underset{\_}{Ⅎ}xA\to \left(\forall x\neg x=A\leftrightarrow \forall y\neg y=A\right)$$
12		alnex	$$⊢\forall x\neg x=A\leftrightarrow \neg \exists xx=A$$
13		alnex	$$⊢\forall y\neg y=A\leftrightarrow \neg \exists yy=A$$
14	11 12 13	3bitr3g	$$⊢\underset{\_}{Ⅎ}xA\to \left(\neg \exists xx=A\leftrightarrow \neg \exists yy=A\right)$$
15	14	con4bid	$$⊢\underset{\_}{Ⅎ}xA\to \left(\exists xx=A\leftrightarrow \exists yy=A\right)$$