Theorem dvelimexcasei

Description: Eliminate a disjoint variable condition from an existentially quantified statement using cases. Inference form of dvelimexcased . See axnulg for an example of its use. (Contributed by BTernaryTau, 31-Jul-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dvelimexcasei.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )
2		dvelimexcasei.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜒 )
3		dvelimexcasei.3	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ( 𝜑 → 𝜒 ) ) )
4		dvelimexcasei.4	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) )
5		dvelimexcasei.5	⊢ ∃ 𝑧 𝜑
6		dvelimexcasei.6	⊢ ∃ 𝑥 𝜓
7		nftru	⊢ Ⅎ 𝑥 ⊤
8		nfvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 ⊤ )
9	1	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜑 )
10	2	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑧 𝜒 )
11	3	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑥 → ( 𝜑 → 𝜒 ) ) )
12	4	adantl	⊢ ( ( ⊤ ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜓 → 𝜒 ) )
13	5	a1i	⊢ ( ⊤ → ∃ 𝑧 𝜑 )
14	6	a1i	⊢ ( ⊤ → ∃ 𝑥 𝜓 )
15	7 8 9 10 11 12 13 14	dvelimexcased	⊢ ( ⊤ → ∃ 𝑥 𝜒 )
16	15	mptru	⊢ ∃ 𝑥 𝜒