Theorem cbvreucsf

Description: A more general version of cbvreuv that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvralcsf.1	$$⊢\underset{\_}{Ⅎ}yA$$
	cbvralcsf.2	$$⊢\underset{\_}{Ⅎ}xB$$
	cbvralcsf.3	$$⊢Ⅎy\phi$$
	cbvralcsf.4	$$⊢Ⅎx\psi$$
	cbvralcsf.5	$$⊢x=y\to A=B$$
	cbvralcsf.6	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvreucsf	$$⊢\exists !x\in A\phi \leftrightarrow \exists !y\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		cbvralcsf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		cbvralcsf.3	$$⊢Ⅎy\phi$$
4		cbvralcsf.4	$$⊢Ⅎx\psi$$
5		cbvralcsf.5	$$⊢x=y\to A=B$$
6		cbvralcsf.6	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
7		nfv	$$⊢Ⅎz\left(x\in A\wedge \phi \right)$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌A$$
9	8	nfcri	$$⊢Ⅎxz\in ⦋z/x⦌A$$
10		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
11	9 10	nfan	$$⊢Ⅎx\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)$$
12		id	$$⊢x=z\to x=z$$
13		csbeq1a	$$⊢x=z\to A=⦋z/x⦌A$$
14	12 13	eleq12d	$$⊢x=z\to \left(x\in A\leftrightarrow z\in ⦋z/x⦌A\right)$$
15		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
16	14 15	anbi12d	$$⊢x=z\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow \left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\right)$$
17	7 11 16	cbveu	$$⊢\exists !x\left(x\in A\wedge \phi \right)\leftrightarrow \exists !z\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}yz$$
19	18 1	nfcsb	$$⊢\underset{\_}{Ⅎ}y⦋z/x⦌A$$
20	19	nfcri	$$⊢Ⅎyz\in ⦋z/x⦌A$$
21	3	nfsb	$$⊢Ⅎy\left[z/x\right]\phi$$
22	20 21	nfan	$$⊢Ⅎy\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)$$
23		nfv	$$⊢Ⅎz\left(y\in B\wedge \psi \right)$$
24		id	$$⊢z=y\to z=y$$
25		csbeq1	$$⊢z=y\to ⦋z/x⦌A=⦋y/x⦌A$$
26		sbsbc	$$⊢\left[y/x\right]v\in A\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A$$
27	26	abbii	$$⊢\left\{v|\left[y/x\right]v\in A\right\}=\left\{v|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A\right\}$$
28	2	nfcri	$$⊢Ⅎxv\in B$$
29	5	eleq2d	$$⊢x=y\to \left(v\in A\leftrightarrow v\in B\right)$$
30	28 29	sbie	$$⊢\left[y/x\right]v\in A\leftrightarrow v\in B$$
31	30	bicomi	$$⊢v\in B\leftrightarrow \left[y/x\right]v\in A$$
32	31	abbi2i	$$⊢B=\left\{v|\left[y/x\right]v\in A\right\}$$
33		df-csb	$$⊢⦋y/x⦌A=\left\{v|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A\right\}$$
34	27 32 33	3eqtr4ri	$$⊢⦋y/x⦌A=B$$
35	25 34	eqtrdi	$$⊢z=y\to ⦋z/x⦌A=B$$
36	24 35	eleq12d	$$⊢z=y\to \left(z\in ⦋z/x⦌A\leftrightarrow y\in B\right)$$
37		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
38	4 6	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
39	37 38	bitrdi	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
40	36 39	anbi12d	$$⊢z=y\to \left(\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\leftrightarrow \left(y\in B\wedge \psi \right)\right)$$
41	22 23 40	cbveu	$$⊢\exists !z\left(z\in ⦋z/x⦌A\wedge \left[z/x\right]\phi \right)\leftrightarrow \exists !y\left(y\in B\wedge \psi \right)$$
42	17 41	bitri	$$⊢\exists !x\left(x\in A\wedge \phi \right)\leftrightarrow \exists !y\left(y\in B\wedge \psi \right)$$
43		df-reu	$$⊢\exists !x\in A\phi \leftrightarrow \exists !x\left(x\in A\wedge \phi \right)$$
44		df-reu	$$⊢\exists !y\in B\psi \leftrightarrow \exists !y\left(y\in B\wedge \psi \right)$$
45	42 43 44	3bitr4i	$$⊢\exists !x\in A\phi \leftrightarrow \exists !y\in B\psi$$