Theorem eusv2nf

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypothesis	eusv2.1	$$⊢A\in \mathrm{V}$$
Assertion	eusv2nf	$$⊢\exists !y\exists xy=A\leftrightarrow \underset{\_}{Ⅎ}xA$$

Proof

Step	Hyp	Ref	Expression
1		eusv2.1	$$⊢A\in \mathrm{V}$$
2		nfeu1	$$⊢Ⅎy\exists !y\exists xy=A$$
3		nfe1	$$⊢Ⅎx\exists xy=A$$
4	3	nfeuw	$$⊢Ⅎx\exists !y\exists xy=A$$
5	1	isseti	$$⊢\exists yy=A$$
6		19.8a	$$⊢y=A\to \exists xy=A$$
7	6	ancri	$$⊢y=A\to \left(\exists xy=A\wedge y=A\right)$$
8	5 7	eximii	$$⊢\exists y\left(\exists xy=A\wedge y=A\right)$$
9		eupick	$$⊢\left(\exists !y\exists xy=A\wedge \exists y\left(\exists xy=A\wedge y=A\right)\right)\to \left(\exists xy=A\to y=A\right)$$
10	8 9	mpan2	$$⊢\exists !y\exists xy=A\to \left(\exists xy=A\to y=A\right)$$
11	4 10	alrimi	$$⊢\exists !y\exists xy=A\to \forall x\left(\exists xy=A\to y=A\right)$$
12		nf6	$$⊢Ⅎxy=A\leftrightarrow \forall x\left(\exists xy=A\to y=A\right)$$
13	11 12	sylibr	$$⊢\exists !y\exists xy=A\to Ⅎxy=A$$
14	2 13	alrimi	$$⊢\exists !y\exists xy=A\to \forall yℲxy=A$$
15		dfnfc2	$$⊢\forall xA\in \mathrm{V}\to \left(\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy=A\right)$$
16	15 1	mpg	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy=A$$
17	14 16	sylibr	$$⊢\exists !y\exists xy=A\to \underset{\_}{Ⅎ}xA$$
18		eusvnfb	$$⊢\exists !y\forall xy=A\leftrightarrow \left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)$$
19	1 18	mpbiran2	$$⊢\exists !y\forall xy=A\leftrightarrow \underset{\_}{Ⅎ}xA$$
20		eusv2i	$$⊢\exists !y\forall xy=A\to \exists !y\exists xy=A$$
21	19 20	sylbir	$$⊢\underset{\_}{Ⅎ}xA\to \exists !y\exists xy=A$$
22	17 21	impbii	$$⊢\exists !y\exists xy=A\leftrightarrow \underset{\_}{Ⅎ}xA$$