# Metamath Proof Explorer

## Theorem rmo2

Description: Alternate definition of restricted "at most one." Note that E* x e. A ph is not equivalent to E. y e. A A. x e. A ( ph -> x = y ) (in analogy to reu6 ); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i . (Contributed by NM, 17-Jun-2017)

Ref Expression
Hypothesis rmo2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 rmo2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 df-rmo ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
3 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
4 3 1 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
5 4 mof ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}={y}\right)$
6 impexp ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}={y}\right)↔\left({x}\in {A}\to \left({\phi }\to {x}={y}\right)\right)$
7 6 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {x}={y}\right)\right)$
8 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left({\phi }\to {x}={y}\right)\right)$
9 7 8 bitr4i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}={y}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
10 9 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {\phi }\right)\to {x}={y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
11 2 5 10 3bitri ${⊢}{\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)$