Theorem bj-cbveximdv

Description: A lemma for alpha-renaming of variables bound by an existential quantifier. (Contributed by BJ, 4-Apr-2026) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-cbveximdv.nf0	|- ( ph -> A. x ph )
	bj-cbveximdv.nf1	|- ( ph -> A. y ph )
	bj-cbveximdv.nfth	|- ( ph -> ( ch -> A. y ch ) )
	bj-cbveximdv.denote	|- ( ph -> A. x E. y ps )
	bj-cbveximdv.maj	|- ( ( ph /\ ps ) -> ( ch -> th ) )
Assertion	bj-cbveximdv	|- ( ph -> ( E. x ch -> E. y th ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbveximdv.nf0	|- ( ph -> A. x ph )
2		bj-cbveximdv.nf1	|- ( ph -> A. y ph )
3		bj-cbveximdv.nfth	|- ( ph -> ( ch -> A. y ch ) )
4		bj-cbveximdv.denote	|- ( ph -> A. x E. y ps )
5		bj-cbveximdv.maj	|- ( ( ph /\ ps ) -> ( ch -> th ) )
6		ax5e	|- ( E. x E. y th -> E. y th )
7	6	a1i	|- ( ph -> ( E. x E. y th -> E. y th ) )
8	1 2 3 7 4 5	bj-cbveximdlem	|- ( ph -> ( E. x ch -> E. y th ) )