Theorem bj-cbvalimdv

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

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

Proof

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