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

Proof

Step	Hyp	Ref	Expression
1		dvelimexcasei.1	$$⊢\neg \forall xx=y\to Ⅎx\phi$$
2		dvelimexcasei.2	$$⊢\neg \forall xx=y\to Ⅎz\chi$$
3		dvelimexcasei.3	$$⊢\neg \forall xx=y\to \left(z=x\to \left(\phi \to \chi \right)\right)$$
4		dvelimexcasei.4	$$⊢\forall xx=y\to \left(\psi \to \chi \right)$$
5		dvelimexcasei.5	$$⊢\exists z\phi$$
6		dvelimexcasei.6	$$⊢\exists x\psi$$
7		nftru	$$⊢Ⅎx\top$$
8		nfvd	$$⊢\neg \forall xx=y\to Ⅎz\top$$
9	1	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to Ⅎx\phi$$
10	2	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to Ⅎz\chi$$
11	3	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to \left(z=x\to \left(\phi \to \chi \right)\right)$$
12	4	adantl	$$⊢\left(\top \wedge \forall xx=y\right)\to \left(\psi \to \chi \right)$$
13	5	a1i	$$⊢\top \to \exists z\phi$$
14	6	a1i	$$⊢\top \to \exists x\psi$$
15	7 8 9 10 11 12 13 14	dvelimexcased	$$⊢\top \to \exists x\chi$$
16	15	mptru	$$⊢\exists x\chi$$