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	$$⊢\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		cbvexeqsetf	$$⊢\underset{\_}{Ⅎ}xA\to \left(\exists xx=A\leftrightarrow \exists yy=A\right)$$
3	1 2	bitr4id	$$⊢\underset{\_}{Ⅎ}xA\to \left(A\in \mathrm{V}\leftrightarrow \exists xx=A\right)$$