Theorem dvelimhw

Description: Proof of dvelimh without using ax-13 but with additional distinct variable conditions. (Contributed 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	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) )