Theorem eusv4

Description: Two ways to express single-valuedness of a class expression B ( y ) . (Contributed by NM, 27-Oct-2010)

	Ref	Expression
Hypothesis	eusv4.1	$$⊢B\in \mathrm{V}$$
Assertion	eusv4	$$⊢\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B$$

Proof

Step	Hyp	Ref	Expression
1		eusv4.1	$$⊢B\in \mathrm{V}$$
2		reusv2lem3	$$⊢\forall y\in AB\in \mathrm{V}\to \left(\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B\right)$$
3	1	a1i	$$⊢y\in A\to B\in \mathrm{V}$$
4	2 3	mprg	$$⊢\exists !x\exists y\in Ax=B\leftrightarrow \exists !x\forall y\in Ax=B$$