Theorem eusv1

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

	Ref	Expression
Assertion	eusv1	$$⊢\exists !y\forall xy=A\leftrightarrow \exists y\forall xy=A$$

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall xy=A\to y=A$$
2		sp	$$⊢\forall xz=A\to z=A$$
3		eqtr3	$$⊢\left(y=A\wedge z=A\right)\to y=z$$
4	1 2 3	syl2an	$$⊢\left(\forall xy=A\wedge \forall xz=A\right)\to y=z$$
5	4	gen2	$$⊢\forall y\forall z\left(\left(\forall xy=A\wedge \forall xz=A\right)\to y=z\right)$$
6		eqeq1	$$⊢y=z\to \left(y=A\leftrightarrow z=A\right)$$
7	6	albidv	$$⊢y=z\to \left(\forall xy=A\leftrightarrow \forall xz=A\right)$$
8	7	eu4	$$⊢\exists !y\forall xy=A\leftrightarrow \left(\exists y\forall xy=A\wedge \forall y\forall z\left(\left(\forall xy=A\wedge \forall xz=A\right)\to y=z\right)\right)$$
9	5 8	mpbiran2	$$⊢\exists !y\forall xy=A\leftrightarrow \exists y\forall xy=A$$