Metamath Proof Explorer

Theorem nd1

Description: A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion nd1 ⊢ ∀ x x = y → ¬ ∀ x y ∈ z

Proof

Step Hyp Ref Expression
1 elirrv ⊢ ¬ z ∈ z
2 stdpc4 ⊢ ∀ y y ∈ z → z y y ∈ z
3 1 nfnth ⊢ Ⅎ y z ∈ z
4 elequ1 ⊢ y = z → y ∈ z ↔ z ∈ z
5 3 4 sbie ⊢ z y y ∈ z ↔ z ∈ z
6 2 5 sylib ⊢ ∀ y y ∈ z → z ∈ z
7 1 6 mto ⊢ ¬ ∀ y y ∈ z
8 axc11 ⊢ ∀ x x = y → ∀ x y ∈ z → ∀ y y ∈ z
9 7 8 mtoi ⊢ ∀ x x = y → ¬ ∀ x y ∈ z