Theorem bj-cbveximd

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

	Ref	Expression
Hypotheses	bj-cbveximd.nf0	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bj-cbveximd.nf1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
	bj-cbveximd.nfch	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑦 𝜒 ) )
	bj-cbveximd.nfth	⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜃 ) )
	bj-cbveximd.denote	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜓 )
	bj-cbveximd.maj	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) )
Assertion	bj-cbveximd	⊢ ( 𝜑 → ( ∃ 𝑥 𝜒 → ∃ 𝑦 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbveximd.nf0	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bj-cbveximd.nf1	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3		bj-cbveximd.nfch	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑦 𝜒 ) )
4		bj-cbveximd.nfth	⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜃 ) )
5		bj-cbveximd.denote	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜓 )
6		bj-cbveximd.maj	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → 𝜃 ) )
7		excomim	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜃 → ∃ 𝑦 ∃ 𝑥 𝜃 )
8	2 4	eximdh	⊢ ( 𝜑 → ( ∃ 𝑦 ∃ 𝑥 𝜃 → ∃ 𝑦 𝜃 ) )
9	7 8	syl5	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 𝜃 → ∃ 𝑦 𝜃 ) )
10	1 2 3 9 5 6	bj-cbveximdlem	⊢ ( 𝜑 → ( ∃ 𝑥 𝜒 → ∃ 𝑦 𝜃 ) )