Theorem bj-cbvalimdlem

Description: A lemma for alpha-renaming of variables bound by a universal quantifier. Hypothesis bj-cbvalimdlem.nfch can be proved either from DV conditions as in bj-cbvalimdv or from a nonfreeness condition and alcom as in bj-cbvalimd . Hypothesis bj-cbvalimdlem.denote is weaker than the corresponding hypothesis of bj-cbvalimd0 , and this proof is therefore a bit longer, not using bj-spim but bj-eximcom . (Contributed by BJ, 12-Mar-2023) Proof should not use 19.35 . (Proof modification is discouraged.)

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

Proof

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