Theorem cbvreu

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvreuw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvrmo.1	$$⊢Ⅎy\phi$$
2		cbvrmo.2	$$⊢Ⅎx\psi$$
3		cbvrmo.3	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
4		nfv	$$⊢Ⅎz\left(x\in A\wedge \phi \right)$$
5	4	sb8eu	$$⊢\exists !x\left(x\in A\wedge \phi \right)\leftrightarrow \exists !z\left[z/x\right]\left(x\in A\wedge \phi \right)$$
6		sban	$$⊢\left[z/x\right]\left(x\in A\wedge \phi \right)\leftrightarrow \left(\left[z/x\right]x\in A\wedge \left[z/x\right]\phi \right)$$
7	6	eubii	$$⊢\exists !z\left[z/x\right]\left(x\in A\wedge \phi \right)\leftrightarrow \exists !z\left(\left[z/x\right]x\in A\wedge \left[z/x\right]\phi \right)$$
8		clelsb1	$$⊢\left[z/x\right]x\in A\leftrightarrow z\in A$$
9	8	anbi1i	$$⊢\left(\left[z/x\right]x\in A\wedge \left[z/x\right]\phi \right)\leftrightarrow \left(z\in A\wedge \left[z/x\right]\phi \right)$$
10	9	eubii	$$⊢\exists !z\left(\left[z/x\right]x\in A\wedge \left[z/x\right]\phi \right)\leftrightarrow \exists !z\left(z\in A\wedge \left[z/x\right]\phi \right)$$
11		nfv	$$⊢Ⅎyz\in A$$
12	1	nfsb	$$⊢Ⅎy\left[z/x\right]\phi$$
13	11 12	nfan	$$⊢Ⅎy\left(z\in A\wedge \left[z/x\right]\phi \right)$$
14		nfv	$$⊢Ⅎz\left(y\in A\wedge \psi \right)$$
15		eleq1w	$$⊢z=y\to \left(z\in A\leftrightarrow y\in A\right)$$
16		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
17	2 3	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
18	16 17	bitrdi	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
19	15 18	anbi12d	$$⊢z=y\to \left(\left(z\in A\wedge \left[z/x\right]\phi \right)\leftrightarrow \left(y\in A\wedge \psi \right)\right)$$
20	13 14 19	cbveu	$$⊢\exists !z\left(z\in A\wedge \left[z/x\right]\phi \right)\leftrightarrow \exists !y\left(y\in A\wedge \psi \right)$$
21	10 20	bitri	$$⊢\exists !z\left(\left[z/x\right]x\in A\wedge \left[z/x\right]\phi \right)\leftrightarrow \exists !y\left(y\in A\wedge \psi \right)$$
22	5 7 21	3bitri	$$⊢\exists !x\left(x\in A\wedge \phi \right)\leftrightarrow \exists !y\left(y\in A\wedge \psi \right)$$
23		df-reu	$$⊢\exists !x\in A\phi \leftrightarrow \exists !x\left(x\in A\wedge \phi \right)$$
24		df-reu	$$⊢\exists !y\in A\psi \leftrightarrow \exists !y\left(y\in A\wedge \psi \right)$$
25	22 23 24	3bitr4i	$$⊢\exists !x\in A\phi \leftrightarrow \exists !y\in A\psi$$