Theorem reusv2lem1

Description: Lemma for reusv2 . (Contributed by NM, 22-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016)

	Ref	Expression
Assertion	reusv2lem1	$$⊢A\ne \varnothing \to \left(\exists !x\forall y\in Ax=B\leftrightarrow \exists x\forall y\in Ax=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists yy\in A$$
2		nfra1	$$⊢Ⅎy\forall y\in Ax=B$$
3	2	nfmov	$$⊢Ⅎy{\exists }^{*}x\forall y\in Ax=B$$
4		rsp	$$⊢\forall y\in Ax=B\to \left(y\in A\to x=B\right)$$
5	4	com12	$$⊢y\in A\to \left(\forall y\in Ax=B\to x=B\right)$$
6	5	alrimiv	$$⊢y\in A\to \forall x\left(\forall y\in Ax=B\to x=B\right)$$
7		mo2icl	$$⊢\forall x\left(\forall y\in Ax=B\to x=B\right)\to {\exists }^{*}x\forall y\in Ax=B$$
8	6 7	syl	$$⊢y\in A\to {\exists }^{*}x\forall y\in Ax=B$$
9	3 8	exlimi	$$⊢\exists yy\in A\to {\exists }^{*}x\forall y\in Ax=B$$
10	1 9	sylbi	$$⊢A\ne \varnothing \to {\exists }^{*}x\forall y\in Ax=B$$
11		df-eu	$$⊢\exists !x\forall y\in Ax=B\leftrightarrow \left(\exists x\forall y\in Ax=B\wedge {\exists }^{*}x\forall y\in Ax=B\right)$$
12	11	rbaib	$$⊢{\exists }^{*}x\forall y\in Ax=B\to \left(\exists !x\forall y\in Ax=B\leftrightarrow \exists x\forall y\in Ax=B\right)$$
13	10 12	syl	$$⊢A\ne \varnothing \to \left(\exists !x\forall y\in Ax=B\leftrightarrow \exists x\forall y\in Ax=B\right)$$