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 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
dvelimhw.2 ⊢ ( 𝜓 → ∀ 𝑧 𝜓 )
dvelimhw.3 ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
dvelimhw.4 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
Assertion dvelimhw ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dvelimhw.1 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2 dvelimhw.2 ⊢ ( 𝜓 → ∀ 𝑧 𝜓 )
3 dvelimhw.3 ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4 dvelimhw.4 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
5 nfv ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
6 equcom ⊢ ( 𝑧 = 𝑦 ↔ 𝑦 = 𝑧 )
7 nfna1 ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
8 7 4 nf5d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 = 𝑧 )
9 6 8 nfxfrd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 )
10 1 nf5i ⊢ Ⅎ 𝑥 𝜑
11 10 a1i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )
12 9 11 nfimd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜑 ) )
13 5 12 nfald ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) )
14 2 3 equsalhw ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ 𝜓 )
15 14 nfbii ⊢ ( Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ Ⅎ 𝑥 𝜓 )
16 13 15 sylib ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜓 )
17 16 nf5rd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )