Theorem cbvex1v

Description: Rule used to change bound variables, using implicit substitution. (Contributed by BTernaryTau, 31-Jul-2025)

	Ref	Expression
Hypotheses	cbvex1v.1	$$⊢Ⅎx\phi$$
	cbvex1v.2	$$⊢Ⅎy\phi$$
	cbvex1v.3	$$⊢\phi \to Ⅎy\psi$$
	cbvex1v.4	$$⊢\phi \to Ⅎx\chi$$
	cbvex1v.5	$$⊢\phi \to \left(x=y\to \left(\psi \to \chi \right)\right)$$
Assertion	cbvex1v	$$⊢\phi \to \left(\exists x\psi \to \exists y\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvex1v.1	$$⊢Ⅎx\phi$$
2		cbvex1v.2	$$⊢Ⅎy\phi$$
3		cbvex1v.3	$$⊢\phi \to Ⅎy\psi$$
4		cbvex1v.4	$$⊢\phi \to Ⅎx\chi$$
5		cbvex1v.5	$$⊢\phi \to \left(x=y\to \left(\psi \to \chi \right)\right)$$
6	4	nfnd	$$⊢\phi \to Ⅎx\neg \chi$$
7	3	nfnd	$$⊢\phi \to Ⅎy\neg \psi$$
8		equcomi	$$⊢y=x\to x=y$$
9		con3	$$⊢\left(\psi \to \chi \right)\to \left(\neg \chi \to \neg \psi \right)$$
10	8 5 9	syl56	$$⊢\phi \to \left(y=x\to \left(\neg \chi \to \neg \psi \right)\right)$$
11	2 1 6 7 10	cbv1v	$$⊢\phi \to \left(\forall y\neg \chi \to \forall x\neg \psi \right)$$
12	11	con3d	$$⊢\phi \to \left(\neg \forall x\neg \psi \to \neg \forall y\neg \chi \right)$$
13		df-ex	$$⊢\exists x\psi \leftrightarrow \neg \forall x\neg \psi$$
14		df-ex	$$⊢\exists y\chi \leftrightarrow \neg \forall y\neg \chi$$
15	12 13 14	3imtr4g	$$⊢\phi \to \left(\exists x\psi \to \exists y\chi \right)$$