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	|- F/ x ph
	dvelimexcased.2	|- ( -. A. x x = y -> F/ z ph )
	dvelimexcased.3	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
	dvelimexcased.4	|- ( ( ph /\ -. A. x x = y ) -> F/ z th )
	dvelimexcased.5	|- ( ( ph /\ -. A. x x = y ) -> ( z = x -> ( ps -> th ) ) )
	dvelimexcased.6	|- ( ( ph /\ A. x x = y ) -> ( ch -> th ) )
	dvelimexcased.7	|- ( ph -> E. z ps )
	dvelimexcased.8	|- ( ph -> E. x ch )
Assertion	dvelimexcased	|- ( ph -> E. x th )

Proof

Step	Hyp	Ref	Expression
1		dvelimexcased.1	|- F/ x ph
2		dvelimexcased.2	|- ( -. A. x x = y -> F/ z ph )
3		dvelimexcased.3	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
4		dvelimexcased.4	|- ( ( ph /\ -. A. x x = y ) -> F/ z th )
5		dvelimexcased.5	|- ( ( ph /\ -. A. x x = y ) -> ( z = x -> ( ps -> th ) ) )
6		dvelimexcased.6	|- ( ( ph /\ A. x x = y ) -> ( ch -> th ) )
7		dvelimexcased.7	|- ( ph -> E. z ps )
8		dvelimexcased.8	|- ( ph -> E. x ch )
9		nfa1	|- F/ x A. x x = y
10	1 9	nfan	|- F/ x ( ph /\ A. x x = y )
11	10 6	eximd	|- ( ( ph /\ A. x x = y ) -> ( E. x ch -> E. x th ) )
12	11	ex	|- ( ph -> ( A. x x = y -> ( E. x ch -> E. x th ) ) )
13	8 12	mpid	|- ( ph -> ( A. x x = y -> E. x th ) )
14		nfv	|- F/ z -. A. x x = y
15	14 2	nfan1c	|- F/ z ( ph /\ -. A. x x = y )
16		nfna1	|- F/ x -. A. x x = y
17	1 16	nfan	|- F/ x ( ph /\ -. A. x x = y )
18	15 17 3 4 5	cbvex1v	|- ( ( ph /\ -. A. x x = y ) -> ( E. z ps -> E. x th ) )
19	18	ex	|- ( ph -> ( -. A. x x = y -> ( E. z ps -> E. x th ) ) )
20	7 19	mpid	|- ( ph -> ( -. A. x x = y -> E. x th ) )
21	13 20	pm2.61d	|- ( ph -> E. x th )