Theorem cleljustALT

Description: Alternate proof of cleljust . It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how disjoint variable conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004) (Revised by BJ, 29-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cleljustALT	⊢ ( 𝑥 ∈ 𝑦 ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-5	⊢ ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 )
2		elequ1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
3	1 2	equsexhv	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝑦 )
4	3	bicomi	⊢ ( 𝑥 ∈ 𝑦 ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦 ) )