Theorem cleljustALT 2370

Description: Alternate proof of cleljust 2117. 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 1909	. . 3 ⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)
2		elequ1 2115	. . 3 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
3	1, 2	equsexhv 2296	. 2 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) ↔ 𝑥 ∈ 𝑦)
4	3	bicomi 224	1 ⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-10 2141  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782

This theorem is referenced by: (None)