Theorem issetft

Description: Closed theorem form of isset that does not require x and A to be distinct. Extracted from the proof of vtoclgft . (Contributed by Wolf Lammen, 9-Apr-2025)

	Ref	Expression
Assertion	issetft	|- ( F/_ x A -> ( A e. _V <-> E. x x = A ) )

Proof

Step	Hyp	Ref	Expression
1		isset	|- ( A e. _V <-> E. y y = A )
2		nfv	|- F/ y F/_ x A
3		nfnfc1	|- F/ x F/_ x A
4		nfcvd	|- ( F/_ x A -> F/_ x y )
5		id	|- ( F/_ x A -> F/_ x A )
6	4 5	nfeqd	|- ( F/_ x A -> F/ x y = A )
7	6	nfnd	|- ( F/_ x A -> F/ x -. y = A )
8		nfvd	|- ( F/_ x A -> F/ y -. x = A )
9		eqeq1	|- ( y = x -> ( y = A <-> x = A ) )
10	9	notbid	|- ( y = x -> ( -. y = A <-> -. x = A ) )
11	10	a1i	|- ( F/_ x A -> ( y = x -> ( -. y = A <-> -. x = A ) ) )
12	2 3 7 8 11	cbv2w	|- ( F/_ x A -> ( A. y -. y = A <-> A. x -. x = A ) )
13		alnex	|- ( A. y -. y = A <-> -. E. y y = A )
14		alnex	|- ( A. x -. x = A <-> -. E. x x = A )
15	12 13 14	3bitr3g	|- ( F/_ x A -> ( -. E. y y = A <-> -. E. x x = A ) )
16	15	con4bid	|- ( F/_ x A -> ( E. y y = A <-> E. x x = A ) )
17	1 16	bitrid	|- ( F/_ x A -> ( A e. _V <-> E. x x = A ) )