Theorem cbvmodavw

Description: Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbvmodavw.1	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	cbvmodavw	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow {\exists }^{*}y\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvmodavw.1	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		equequ1	$$⊢x=y\to \left(x=z\leftrightarrow y=z\right)$$
3	2	adantl	$$⊢\left(\phi \wedge x=y\right)\to \left(x=z\leftrightarrow y=z\right)$$
4	1 3	imbi12d	$$⊢\left(\phi \wedge x=y\right)\to \left(\left(\psi \to x=z\right)\leftrightarrow \left(\chi \to y=z\right)\right)$$
5	4	cbvaldvaw	$$⊢\phi \to \left(\forall x\left(\psi \to x=z\right)\leftrightarrow \forall y\left(\chi \to y=z\right)\right)$$
6	5	exbidv	$$⊢\phi \to \left(\exists z\forall x\left(\psi \to x=z\right)\leftrightarrow \exists z\forall y\left(\chi \to y=z\right)\right)$$
7		dfmo	$$⊢{\exists }^{*}x\psi \leftrightarrow \exists z\forall x\left(\psi \to x=z\right)$$
8		dfmo	$$⊢{\exists }^{*}y\chi \leftrightarrow \exists z\forall y\left(\chi \to y=z\right)$$
9	6 7 8	3bitr4g	$$⊢\phi \to \left({\exists }^{*}x\psi \leftrightarrow {\exists }^{*}y\chi \right)$$