Theorem eusv2

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

	Ref	Expression
Hypothesis	eusv2.1	$$⊢A\in \mathrm{V}$$
Assertion	eusv2	$$⊢\exists !y\exists xy=A\leftrightarrow \exists !y\forall xy=A$$

Proof

Step	Hyp	Ref	Expression
1		eusv2.1	$$⊢A\in \mathrm{V}$$
2	1	eusv2nf	$$⊢\exists !y\exists xy=A\leftrightarrow \underset{\_}{Ⅎ}xA$$
3		eusvnfb	$$⊢\exists !y\forall xy=A\leftrightarrow \left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)$$
4	1 3	mpbiran2	$$⊢\exists !y\forall xy=A\leftrightarrow \underset{\_}{Ⅎ}xA$$
5	2 4	bitr4i	$$⊢\exists !y\exists xy=A\leftrightarrow \exists !y\forall xy=A$$