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	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bj-cbvalimd0.nf1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
	bj-cbvalimd0.nfch	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑦 𝜒 ) )
	bj-cbvalimd0.nfth	⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜃 ) )
	bj-cbvalimd0.denote	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
	bj-cbvalimd0.maj	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) )
Assertion	bj-cbvalimd0	⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbvalimd0.nf0	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bj-cbvalimd0.nf1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3		bj-cbvalimd0.nfch	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑦 𝜒 ) )
4		bj-cbvalimd0.nfth	⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜃 ) )
5		bj-cbvalimd0.denote	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
6		bj-cbvalimd0.maj	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) )
7	1 3	hbald	⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 ∀ 𝑥 𝜒 ) )
8	1 4 5 6	bj-spim	⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → 𝜃 ) )
9	2 7 8	bj-alrimd	⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑦 𝜃 ) )