Theorem rmo2i

Description: Condition implying restricted "at most one". (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Hypothesis	rmo2.1	$$⊢Ⅎy\phi$$
Assertion	rmo2i	$$⊢\exists y\in A\forall x\in A\left(\phi \to x=y\right)\to {\exists }^{*}x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		rmo2.1	$$⊢Ⅎy\phi$$
2		rexex	$$⊢\exists y\in A\forall x\in A\left(\phi \to x=y\right)\to \exists y\forall x\in A\left(\phi \to x=y\right)$$
3	1	rmo2	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow \exists y\forall x\in A\left(\phi \to x=y\right)$$
4	2 3	sylibr	$$⊢\exists y\in A\forall x\in A\left(\phi \to x=y\right)\to {\exists }^{*}x\in A\phi$$