Theorem bj-cleljusti

Description: One direction of cleljust , requiring only ax-1 -- ax-5 and ax8v1 . (Contributed by BJ, 31-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-cleljusti	$$⊢\exists z\left(z=x\wedge z\in y\right)\to x\in y$$

Proof

Step	Hyp	Ref	Expression
1		ax8v1	$$⊢z=x\to \left(z\in y\to x\in y\right)$$
2	1	imp	$$⊢\left(z=x\wedge z\in y\right)\to x\in y$$
3	2	exlimiv	$$⊢\exists z\left(z=x\wedge z\in y\right)\to x\in y$$