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	$$⊢\phi \to \forall x\phi$$
	bj-cbvalimd0.nf1	$$⊢\phi \to \forall y\phi$$
	bj-cbvalimd0.nfch	$$⊢\phi \to \left(\chi \to \forall y\chi \right)$$
	bj-cbvalimd0.nfth	$$⊢\phi \to \left(\exists x\theta \to \theta \right)$$
	bj-cbvalimd0.denote	$$⊢\phi \to \exists x\psi$$
	bj-cbvalimd0.maj	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \to \theta \right)$$
Assertion	bj-cbvalimd0	$$⊢\phi \to \left(\forall x\chi \to \forall y\theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-cbvalimd0.nf0	$$⊢\phi \to \forall x\phi$$
2		bj-cbvalimd0.nf1	$$⊢\phi \to \forall y\phi$$
3		bj-cbvalimd0.nfch	$$⊢\phi \to \left(\chi \to \forall y\chi \right)$$
4		bj-cbvalimd0.nfth	$$⊢\phi \to \left(\exists x\theta \to \theta \right)$$
5		bj-cbvalimd0.denote	$$⊢\phi \to \exists x\psi$$
6		bj-cbvalimd0.maj	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \to \theta \right)$$
7	1 3	hbald	$$⊢\phi \to \left(\forall x\chi \to \forall y\forall x\chi \right)$$
8	1 4 5 6	bj-spim	$$⊢\phi \to \left(\forall x\chi \to \theta \right)$$
9	2 7 8	bj-alrimd	$$⊢\phi \to \left(\forall x\chi \to \forall y\theta \right)$$