Theorem cleljustALT2

Description: Alternate proof of cleljust . Compared with cleljustALT , it uses nfv followed by equsexv instead of ax-5 followed by equsexhv , so it uses the idiom F/ x ph instead of ph -> A. x ph to express non-freeness. This style is generally preferred for later theorems. (Contributed by NM, 28-Jan-2004) (Revised by Mario Carneiro, 21-Dec-2016) (Revised by BJ, 29-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cleljustALT2	$$⊢x\in y\leftrightarrow \exists z\left(z=x\wedge z\in y\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎzx\in y$$
2		elequ1	$$⊢z=x\to \left(z\in y\leftrightarrow x\in y\right)$$
3	1 2	equsexv	$$⊢\exists z\left(z=x\wedge z\in y\right)\leftrightarrow x\in y$$
4	3	bicomi	$$⊢x\in y\leftrightarrow \exists z\left(z=x\wedge z\in y\right)$$