Theorem issetf

Description: A version of isset that does not require x and A to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011) (Revised by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypothesis	issetf.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	issetf	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$

Proof

Step	Hyp	Ref	Expression
1		issetf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists yy=A$$
3	1	nfeq2	$$⊢Ⅎxy=A$$
4		nfv	$$⊢Ⅎyx=A$$
5		eqeq1	$$⊢y=x\to \left(y=A\leftrightarrow x=A\right)$$
6	3 4 5	cbvexv1	$$⊢\exists yy=A\leftrightarrow \exists xx=A$$
7	2 6	bitri	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$