Theorem bj-spime

Description: A lemma for existential generalization. In applications, x = y will be substituted for ps and ax6ev will prove Hypothesis bj-spime.denote. (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypotheses	bj-spime.nf0	|- ( ph -> A. x ph )
	bj-spime.nf	|- ( ph -> ( ch -> A. x ch ) )
	bj-spime.denote	|- ( ph -> E. x ps )
	bj-spime.maj	|- ( ( ph /\ ps ) -> ( ch -> th ) )
Assertion	bj-spime	|- ( ph -> ( ch -> E. x th ) )

Proof

Step	Hyp	Ref	Expression
1		bj-spime.nf0	|- ( ph -> A. x ph )
2		bj-spime.nf	|- ( ph -> ( ch -> A. x ch ) )
3		bj-spime.denote	|- ( ph -> E. x ps )
4		bj-spime.maj	|- ( ( ph /\ ps ) -> ( ch -> th ) )
5	4	ex	|- ( ph -> ( ps -> ( ch -> th ) ) )
6	1 5	eximdh	|- ( ph -> ( E. x ps -> E. x ( ch -> th ) ) )
7	3 6	mpd	|- ( ph -> E. x ( ch -> th ) )
8		bj-spimenfa	|- ( ( ch -> A. x ch ) -> ( E. x ( ch -> th ) -> ( ch -> E. x th ) ) )
9	2 7 8	sylc	|- ( ph -> ( ch -> E. x th ) )