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

Proof

Step	Hyp	Ref	Expression
1		bj-cbveximd.nf0	$$⊢\phi \to \forall x\phi$$
2		bj-cbveximd.nf1	$$⊢\phi \to \forall y\phi$$
3		bj-cbveximd.nfch	$$⊢\phi \to \left(\chi \to \forall y\chi \right)$$
4		bj-cbveximd.nfth	$$⊢\phi \to \left(\exists x\theta \to \theta \right)$$
5		bj-cbveximd.denote	$$⊢\phi \to \forall x\exists y\psi$$
6		bj-cbveximd.maj	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \to \theta \right)$$
7		excomim	$$⊢\exists x\exists y\theta \to \exists y\exists x\theta$$
8	2 4	eximdh	$$⊢\phi \to \left(\exists y\exists x\theta \to \exists y\theta \right)$$
9	7 8	syl5	$$⊢\phi \to \left(\exists x\exists y\theta \to \exists y\theta \right)$$
10	1 2 3 9 5 6	bj-cbveximdlem	$$⊢\phi \to \left(\exists x\chi \to \exists y\theta \right)$$