Theorem wl-issetft

Description: A closed form of issetf . The proof here is a modification of a subproof in vtoclgft , where it could be used to shorten the proof. (Contributed by Wolf Lammen, 25-Jan-2025)

	Ref	Expression
Assertion	wl-issetft	$$⊢\underset{\_}{Ⅎ}xA\to \left(A\in \mathrm{V}\leftrightarrow \exists xx=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists yy=A$$
2		nfv	$$⊢Ⅎy\underset{\_}{Ⅎ}xA$$
3		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xA$$
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		nfvd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎy\neg x=A$$
9		eqeq1	$$⊢y=x\to \left(y=A\leftrightarrow x=A\right)$$
10	9	notbid	$$⊢y=x\to \left(\neg y=A\leftrightarrow \neg x=A\right)$$
11	10	a1i	$$⊢\underset{\_}{Ⅎ}xA\to \left(y=x\to \left(\neg y=A\leftrightarrow \neg x=A\right)\right)$$
12	2 3 7 8 11	cbv2w	$$⊢\underset{\_}{Ⅎ}xA\to \left(\forall y\neg y=A\leftrightarrow \forall x\neg x=A\right)$$
13		alnex	$$⊢\forall y\neg y=A\leftrightarrow \neg \exists yy=A$$
14		alnex	$$⊢\forall x\neg x=A\leftrightarrow \neg \exists xx=A$$
15	12 13 14	3bitr3g	$$⊢\underset{\_}{Ⅎ}xA\to \left(\neg \exists yy=A\leftrightarrow \neg \exists xx=A\right)$$
16	15	con4bid	$$⊢\underset{\_}{Ⅎ}xA\to \left(\exists yy=A\leftrightarrow \exists xx=A\right)$$
17	1 16	bitrid	$$⊢\underset{\_}{Ⅎ}xA\to \left(A\in \mathrm{V}\leftrightarrow \exists xx=A\right)$$