This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 nonfreeness. 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 (z = x \land z \in y)$

Proof

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