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 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )