Theorem bj-cbveximdlem

Description: A lemma for alpha-renaming of variables bound by an existential quantifier. Hypothesis bj-cbveximdlem.nfth can be proved either from DV conditions as in bj-cbveximdv or from a nonfreeness condition and excom as in bj-cbveximd . Hypothesis bj-cbveximdlem.denote is weaker than the corresponding hypothesis of ~bj-cbveximd0 , and this proof is therefore a bit longer, not using bj-spime but bj-eximcom . (Contributed by BJ, 12-Mar-2023) Proof should not use 19.35 . (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bj-cbveximdlem.nf0	|- ( ph -> A. x ph )
2		bj-cbveximdlem.nf1	|- ( ph -> A. y ph )
3		bj-cbveximdlem.nfch	|- ( ph -> ( ch -> A. y ch ) )
4		bj-cbveximdlem.nfth	|- ( ph -> ( E. x E. y th -> E. y th ) )
5		bj-cbveximdlem.denote	|- ( ph -> A. x E. y ps )
6		bj-cbveximdlem.maj	|- ( ( ph /\ ps ) -> ( ch -> th ) )
7	6	ex	|- ( ph -> ( ps -> ( ch -> th ) ) )
8	2 7	eximdh	|- ( ph -> ( E. y ps -> E. y ( ch -> th ) ) )
9	1 8	alimdh	|- ( ph -> ( A. x E. y ps -> A. x E. y ( ch -> th ) ) )
10	5 9	mpd	|- ( ph -> A. x E. y ( ch -> th ) )
11		bj-eximcom	|- ( E. y ( ch -> th ) -> ( A. y ch -> E. y th ) )
12	10 4 11	bj-exlimd	|- ( ph -> ( E. x A. y ch -> E. y th ) )
13	1 12 3	bj-exlimd	|- ( ph -> ( E. x ch -> E. y th ) )