Theorem elissetv

Description: An element of a class exists. Version of elisset with a disjoint variable condition on V , x , avoiding df-clab . Prefer its use over elisset when sufficient (for instance in usages where x is a dummy variable). (Contributed by BJ, 14-Sep-2019)

	Ref	Expression
Assertion	elissetv	|- ( A e. V -> E. x x = A )

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( A e. V <-> E. x ( x = A /\ x e. V ) )
2		exsimpl	|- ( E. x ( x = A /\ x e. V ) -> E. x x = A )
3	1 2	sylbi	|- ( A e. V -> E. x x = A )