Theorem eusvnf

Description: Even if x is free in A , it is effectively bound when A ( x ) is single-valued. (Contributed by NM, 14-Oct-2010) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Assertion	eusvnf	$$⊢\exists !y\forall xy=A\to \underset{\_}{Ⅎ}xA$$

Proof

Step	Hyp	Ref	Expression
1		euex	$$⊢\exists !y\forall xy=A\to \exists y\forall xy=A$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
3		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌A$$
4	3	nfeq2	$$⊢Ⅎxy=⦋z/x⦌A$$
5		csbeq1a	$$⊢x=z\to A=⦋z/x⦌A$$
6	5	eqeq2d	$$⊢x=z\to \left(y=A\leftrightarrow y=⦋z/x⦌A\right)$$
7	2 4 6	spcgf	$$⊢z\in \mathrm{V}\to \left(\forall xy=A\to y=⦋z/x⦌A\right)$$
8	7	elv	$$⊢\forall xy=A\to y=⦋z/x⦌A$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
10		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋w/x⦌A$$
11	10	nfeq2	$$⊢Ⅎxy=⦋w/x⦌A$$
12		csbeq1a	$$⊢x=w\to A=⦋w/x⦌A$$
13	12	eqeq2d	$$⊢x=w\to \left(y=A\leftrightarrow y=⦋w/x⦌A\right)$$
14	9 11 13	spcgf	$$⊢w\in \mathrm{V}\to \left(\forall xy=A\to y=⦋w/x⦌A\right)$$
15	14	elv	$$⊢\forall xy=A\to y=⦋w/x⦌A$$
16	8 15	eqtr3d	$$⊢\forall xy=A\to ⦋z/x⦌A=⦋w/x⦌A$$
17	16	alrimivv	$$⊢\forall xy=A\to \forall z\forall w⦋z/x⦌A=⦋w/x⦌A$$
18		sbnfc2	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall z\forall w⦋z/x⦌A=⦋w/x⦌A$$
19	17 18	sylibr	$$⊢\forall xy=A\to \underset{\_}{Ⅎ}xA$$
20	19	exlimiv	$$⊢\exists y\forall xy=A\to \underset{\_}{Ⅎ}xA$$
21	1 20	syl	$$⊢\exists !y\forall xy=A\to \underset{\_}{Ⅎ}xA$$