# Metamath Proof Explorer

## Theorem rmo2i

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

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

### Proof

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