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

Proof

Step	Hyp	Ref	Expression
1		dvelimexcasei.1	|- ( -. A. x x = y -> F/ x ph )
2		dvelimexcasei.2	|- ( -. A. x x = y -> F/ z ch )
3		dvelimexcasei.3	|- ( -. A. x x = y -> ( z = x -> ( ph -> ch ) ) )
4		dvelimexcasei.4	|- ( A. x x = y -> ( ps -> ch ) )
5		dvelimexcasei.5	|- E. z ph
6		dvelimexcasei.6	|- E. x ps
7		nftru	|- F/ x T.
8		nfvd	|- ( -. A. x x = y -> F/ z T. )
9	1	adantl	|- ( ( T. /\ -. A. x x = y ) -> F/ x ph )
10	2	adantl	|- ( ( T. /\ -. A. x x = y ) -> F/ z ch )
11	3	adantl	|- ( ( T. /\ -. A. x x = y ) -> ( z = x -> ( ph -> ch ) ) )
12	4	adantl	|- ( ( T. /\ A. x x = y ) -> ( ps -> ch ) )
13	5	a1i	|- ( T. -> E. z ph )
14	6	a1i	|- ( T. -> E. x ps )
15	7 8 9 10 11 12 13 14	dvelimexcased	|- ( T. -> E. x ch )
16	15	mptru	|- E. x ch