Theorem cbvreud

Description: Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		cbvreud.1	$$⊢Ⅎx\phi$$
2		cbvreud.2	$$⊢Ⅎy\phi$$
3		cbvreud.3	$$⊢\phi \to Ⅎy\psi$$
4		cbvreud.4	$$⊢\phi \to Ⅎx\chi$$
5		cbvreud.5	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
6		nfvd	$$⊢\phi \to Ⅎyx\in A$$
7	6 3	nfand	$$⊢\phi \to Ⅎy\left(x\in A\wedge \psi \right)$$
8		nfvd	$$⊢\phi \to Ⅎxy\in A$$
9	8 4	nfand	$$⊢\phi \to Ⅎx\left(y\in A\wedge \chi \right)$$
10		eleq1	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
11	10	adantl	$$⊢\left(\phi \wedge x=y\right)\to \left(x\in A\leftrightarrow y\in A\right)$$
12	5	imp	$$⊢\left(\phi \wedge x=y\right)\to \left(\psi \leftrightarrow \chi \right)$$
13	11 12	anbi12d	$$⊢\left(\phi \wedge x=y\right)\to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \left(y\in A\wedge \chi \right)\right)$$
14	13	ex	$$⊢\phi \to \left(x=y\to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \left(y\in A\wedge \chi \right)\right)\right)$$
15	1 2 7 9 14	cbveud	$$⊢\phi \to \left(\exists !x\left(x\in A\wedge \psi \right)\leftrightarrow \exists !y\left(y\in A\wedge \chi \right)\right)$$
16		df-reu	$$⊢\exists !x\in A\psi \leftrightarrow \exists !x\left(x\in A\wedge \psi \right)$$
17		df-reu	$$⊢\exists !y\in A\chi \leftrightarrow \exists !y\left(y\in A\wedge \chi \right)$$
18	15 16 17	3bitr4g	$$⊢\phi \to \left(\exists !x\in A\psi \leftrightarrow \exists !y\in A\chi \right)$$