Theorem cleljustALT 2396

Description: Alternate proof of cleljust 2152. 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.)

Assertion

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

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

Proof of Theorem cleljustALT

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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-10 2176  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814

This theorem is referenced by: (None)