dvelimalcased

Description: Eliminate a disjoint variable condition from a universally quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025)

	Ref	Expression
Hypotheses	dvelimalcased.1	⊢ Ⅎ 𝑥 𝜑
	dvelimalcased.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜑 )
	dvelimalcased.3	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
	dvelimalcased.4	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑧 𝜃 )
	dvelimalcased.5	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑥 → ( 𝜓 → 𝜃 ) ) )
	dvelimalcased.6	⊢ ( ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜒 → 𝜃 ) )
	dvelimalcased.7	⊢ ( 𝜑 → ∀ 𝑧 𝜓 )
	dvelimalcased.8	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )
Assertion	dvelimalcased	⊢ ( 𝜑 → ∀ 𝑥 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		dvelimalcased.1	⊢ Ⅎ 𝑥 𝜑
2		dvelimalcased.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜑 )
3		dvelimalcased.3	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
4		dvelimalcased.4	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑧 𝜃 )
5		dvelimalcased.5	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑥 → ( 𝜓 → 𝜃 ) ) )
6		dvelimalcased.6	⊢ ( ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜒 → 𝜃 ) )
7		dvelimalcased.7	⊢ ( 𝜑 → ∀ 𝑧 𝜓 )
8		dvelimalcased.8	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )
9		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑦
10	1 9	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 )
11	10 6	alimd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) )
12	11	ex	⊢ ( 𝜑 → ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) ) )
13	8 12	mpid	⊢ ( 𝜑 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 𝜃 ) )
14		nfv	⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
15	14 2	nfan1c	⊢ Ⅎ 𝑧 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
16		nfna1	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
18	15 17 3 4 5	cbv1v	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑧 𝜓 → ∀ 𝑥 𝜃 ) )
19	18	ex	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑧 𝜓 → ∀ 𝑥 𝜃 ) ) )
20	7 19	mpid	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 𝜃 ) )
21	13 20	pm2.61d	⊢ ( 𝜑 → ∀ 𝑥 𝜃 )

Metamath Proof Explorer

Theorem dvelimalcased

Proof