Theorem eusv2i

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

	Ref	Expression
Assertion	eusv2i	$$⊢\exists !y\forall xy=A\to \exists !y\exists xy=A$$

Proof

Step	Hyp	Ref	Expression
1		nfeu1	$$⊢Ⅎy\exists !y\forall xy=A$$
2		nfcvd	$$⊢\exists !y\forall xy=A\to \underset{\_}{Ⅎ}xy$$
3		eusvnf	$$⊢\exists !y\forall xy=A\to \underset{\_}{Ⅎ}xA$$
4	2 3	nfeqd	$$⊢\exists !y\forall xy=A\to Ⅎxy=A$$
5	4	nfrd	$$⊢\exists !y\forall xy=A\to \left(\exists xy=A\to \forall xy=A\right)$$
6		19.2	$$⊢\forall xy=A\to \exists xy=A$$
7	5 6	impbid1	$$⊢\exists !y\forall xy=A\to \left(\exists xy=A\leftrightarrow \forall xy=A\right)$$
8	1 7	eubid	$$⊢\exists !y\forall xy=A\to \left(\exists !y\exists xy=A\leftrightarrow \exists !y\forall xy=A\right)$$
9	8	ibir	$$⊢\exists !y\forall xy=A\to \exists !y\exists xy=A$$