Theorem bj-elissetALT

Description: Alternate proof of elisset . This is essentially the same proof as seen by inlining bj-denotes and bj-denoteslem . Use elissetv instead when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-elissetALT	$$⊢A\in V\to \exists xx=A$$

Proof

Step	Hyp	Ref	Expression
1		elissetv	$$⊢A\in V\to \exists yy=A$$
2		bj-denotes	$$⊢\exists yy=A\leftrightarrow \exists xx=A$$
3	1 2	sylib	$$⊢A\in V\to \exists xx=A$$