dvelimexcased

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

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

Proof

Step	Hyp	Ref	Expression
1		dvelimexcased.1	⊢ Ⅎ 𝑥 𝜑
2		dvelimexcased.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜑 )
3		dvelimexcased.3	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
4		dvelimexcased.4	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑧 𝜃 )
5		dvelimexcased.5	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑥 → ( 𝜓 → 𝜃 ) ) )
6		dvelimexcased.6	⊢ ( ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜒 → 𝜃 ) )
7		dvelimexcased.7	⊢ ( 𝜑 → ∃ 𝑧 𝜓 )
8		dvelimexcased.8	⊢ ( 𝜑 → ∃ 𝑥 𝜒 )
9		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑦
10	1 9	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 )
11	10 6	eximd	⊢ ( ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜒 → ∃ 𝑥 𝜃 ) )
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	cbvex1v	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑧 𝜓 → ∃ 𝑥 𝜃 ) )
19	18	ex	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 𝜓 → ∃ 𝑥 𝜃 ) ) )
20	7 19	mpid	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝜃 ) )
21	13 20	pm2.61d	⊢ ( 𝜑 → ∃ 𝑥 𝜃 )

Metamath Proof Explorer

Theorem dvelimexcased

Proof