Theorem bj-cbvexiw

Description: Change bound variable. This is to cbvexvw what cbvaliw is to cbvalvw . TODO: move after cbvalivw . (Contributed by BJ, 17-Mar-2020)

	Ref	Expression
Hypotheses	bj-cbvexiw.1	$$⊢\exists x\exists y\psi \to \exists y\psi$$
	bj-cbvexiw.2	$$⊢\phi \to \forall y\phi$$
	bj-cbvexiw.3	$$⊢y=x\to \left(\phi \to \psi \right)$$
Assertion	bj-cbvexiw	$$⊢\exists x\phi \to \exists y\psi$$

Proof

Step	Hyp	Ref	Expression
1		bj-cbvexiw.1	$$⊢\exists x\exists y\psi \to \exists y\psi$$
2		bj-cbvexiw.2	$$⊢\phi \to \forall y\phi$$
3		bj-cbvexiw.3	$$⊢y=x\to \left(\phi \to \psi \right)$$
4	2 3	spimew	$$⊢\phi \to \exists y\psi$$
5	1 4	bj-sylge	$$⊢\exists x\phi \to \exists y\psi$$