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

Metamath Proof Explorer

Theorem dvelimhw

Description: Proof of dvelimh without using ax-13 but with additional distinct variable conditions. (Contributed by NM, 1-Oct-2002) (Revised by Andrew Salmon, 21-Jul-2011) (Revised by NM, 1-Aug-2017) (Proof shortened by Wolf Lammen, 23-Dec-2018)

Ref Expression
Hypotheses dvelimhw.1 ⊢ φ → ∀ x φ
dvelimhw.2 ⊢ ψ → ∀ z ψ
dvelimhw.3 ⊢ z = y → φ ↔ ψ
dvelimhw.4 ⊢ ¬ ∀ x x = y → y = z → ∀ x y = z
Assertion dvelimhw ⊢ ¬ ∀ x x = y → ψ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 dvelimhw.1 ⊢ φ → ∀ x φ
2 dvelimhw.2 ⊢ ψ → ∀ z ψ
3 dvelimhw.3 ⊢ z = y → φ ↔ ψ
4 dvelimhw.4 ⊢ ¬ ∀ x x = y → y = z → ∀ x y = z
5 nfv ⊢ Ⅎ z ¬ ∀ x x = y
6 equcom ⊢ z = y ↔ y = z
7 nfna1 ⊢ Ⅎ x ¬ ∀ x x = y
8 7 4 nf5d ⊢ ¬ ∀ x x = y → Ⅎ x y = z
9 6 8 nfxfrd ⊢ ¬ ∀ x x = y → Ⅎ x z = y
10 1 nf5i ⊢ Ⅎ x φ
11 10 a1i ⊢ ¬ ∀ x x = y → Ⅎ x φ
12 9 11 nfimd ⊢ ¬ ∀ x x = y → Ⅎ x z = y → φ
13 5 12 nfald ⊢ ¬ ∀ x x = y → Ⅎ x ∀ z z = y → φ
14 2 3 equsalhw ⊢ ∀ z z = y → φ ↔ ψ
15 14 nfbii ⊢ Ⅎ x ∀ z z = y → φ ↔ Ⅎ x ψ
16 13 15 sylib ⊢ ¬ ∀ x x = y → Ⅎ x ψ
17 16 nf5rd ⊢ ¬ ∀ x x = y → ψ → ∀ x ψ