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	|- F/_ x A
Assertion	issetf	|- ( A e. _V <-> E. x x = A )

Proof

Step	Hyp	Ref	Expression
1		issetf.1	|- F/_ x A
2		issetft	|- ( F/_ x A -> ( A e. _V <-> E. x x = A ) )
3	1 2	ax-mp	|- ( A e. _V <-> E. x x = A )