Theorem cbvreuwOLD

Description: Obsolete version of cbvreuw as of 10-Dec-2024. (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by GG, 10-Jan-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvreuwOLD.1	$$⊢Ⅎy\phi$$
2		cbvreuwOLD.2	$$⊢Ⅎx\psi$$
3		cbvreuwOLD.3	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
4		nfv	$$⊢Ⅎz\left(x\in A\wedge \phi \right)$$
5	4	sb8euv	$$⊢\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	nfsbv	$$⊢Ⅎ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	sbiev	$$⊢\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	cbveuw	$$⊢\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$$