Theorem 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	$$⊢Ⅎx\phi$$
	dvelimexcased.2	$$⊢\neg \forall xx=y\to Ⅎz\phi$$
	dvelimexcased.3	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
	dvelimexcased.4	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎz\theta$$
	dvelimexcased.5	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(z=x\to \left(\psi \to \theta \right)\right)$$
	dvelimexcased.6	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\chi \to \theta \right)$$
	dvelimexcased.7	$$⊢\phi \to \exists z\psi$$
	dvelimexcased.8	$$⊢\phi \to \exists x\chi$$
Assertion	dvelimexcased	$$⊢\phi \to \exists x\theta$$

Proof

Step	Hyp	Ref	Expression
1		dvelimexcased.1	$$⊢Ⅎx\phi$$
2		dvelimexcased.2	$$⊢\neg \forall xx=y\to Ⅎz\phi$$
3		dvelimexcased.3	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
4		dvelimexcased.4	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎz\theta$$
5		dvelimexcased.5	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(z=x\to \left(\psi \to \theta \right)\right)$$
6		dvelimexcased.6	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\chi \to \theta \right)$$
7		dvelimexcased.7	$$⊢\phi \to \exists z\psi$$
8		dvelimexcased.8	$$⊢\phi \to \exists x\chi$$
9		nfa1	$$⊢Ⅎx\forall xx=y$$
10	1 9	nfan	$$⊢Ⅎx\left(\phi \wedge \forall xx=y\right)$$
11	10 6	eximd	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\exists x\chi \to \exists x\theta \right)$$
12	11	ex	$$⊢\phi \to \left(\forall xx=y\to \left(\exists x\chi \to \exists x\theta \right)\right)$$
13	8 12	mpid	$$⊢\phi \to \left(\forall xx=y\to \exists x\theta \right)$$
14		nfv	$$⊢Ⅎz\neg \forall xx=y$$
15	14 2	nfan1c	$$⊢Ⅎz\left(\phi \wedge \neg \forall xx=y\right)$$
16		nfna1	$$⊢Ⅎx\neg \forall xx=y$$
17	1 16	nfan	$$⊢Ⅎx\left(\phi \wedge \neg \forall xx=y\right)$$
18	15 17 3 4 5	cbvex1v	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(\exists z\psi \to \exists x\theta \right)$$
19	18	ex	$$⊢\phi \to \left(\neg \forall xx=y\to \left(\exists z\psi \to \exists x\theta \right)\right)$$
20	7 19	mpid	$$⊢\phi \to \left(\neg \forall xx=y\to \exists x\theta \right)$$
21	13 20	pm2.61d	$$⊢\phi \to \exists x\theta$$