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

Metamath Proof Explorer

Theorem axregndlem1

Description: Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axregndlem1 ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 19.8a ⊢ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 𝑥 ∈ 𝑦 )
2 nfae ⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑧
3 nfae ⊢ Ⅎ 𝑧 ∀ 𝑥 𝑥 = 𝑧
4 elirrv ⊢ ¬ 𝑥 ∈ 𝑥
5 elequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
6 4 5 mtbii ⊢ ( 𝑥 = 𝑧 → ¬ 𝑧 ∈ 𝑥 )
7 6 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ 𝑧 ∈ 𝑥 )
8 7 pm2.21d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) )
9 3 8 alrimi ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) )
10 9 anim2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
11 10 expcom ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
12 2 11 eximd ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
13 1 12 syl5 ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )