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 ⊢ ∀ x x = z → x ∈ y → ∃ x x ∈ y ∧ ∀ z z ∈ x → ¬ z ∈ y

Proof

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