Theorem bj-cbvalimd0

Description: A lemma for alpha-renaming of variables bound by a universal quantifier. In applications, x = y will be substituted for ps and ax6ev will prove Hypothesis bj-cbvalimd0.denote. When ax6ev is not available but only its universal closure is, then bj-cbvalimd or bj-cbvalimdv should be used (see bj-cbvalimdlem , bj-cbval ). (Contributed by BJ, 4-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		bj-cbvalimd0.nf0	|- ( ph -> A. x ph )
2		bj-cbvalimd0.nf1	|- ( ph -> A. y ph )
3		bj-cbvalimd0.nfch	|- ( ph -> ( ch -> A. y ch ) )
4		bj-cbvalimd0.nfth	|- ( ph -> ( E. x th -> th ) )
5		bj-cbvalimd0.denote	|- ( ph -> E. x ps )
6		bj-cbvalimd0.maj	|- ( ( ph /\ ps ) -> ( ch -> th ) )
7	1 3	hbald	|- ( ph -> ( A. x ch -> A. y A. x ch ) )
8	1 4 5 6	bj-spim	|- ( ph -> ( A. x ch -> th ) )
9	2 7 8	bj-alrimd	|- ( ph -> ( A. x ch -> A. y th ) )