# Metamath Proof Explorer

## Definition df-rmo

Description: Define restricted "at most one".

Note: This notation is most often used to express that ph holds for at most one element of a given class A . For this reading F/_ x A is required, though, for example, asserted when x and A are disjoint.

Should instead A depend on x , you rather assert at most one x fulfilling ph happens to be contained in the corresponding A ( x ) . This interpretation is rarely needed (see also df-ral ). (Contributed by NM, 16-Jun-2017)

Ref Expression
Assertion df-rmo ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 cA ${class}{A}$
2 wph ${wff}{\phi }$
3 2 0 1 wrmo ${wff}{\exists }^{*}{x}\in {A}{\phi }$
4 0 cv ${setvar}{x}$
5 4 1 wcel ${wff}{x}\in {A}$
6 5 2 wa ${wff}\left({x}\in {A}\wedge {\phi }\right)$
7 6 0 wmo ${wff}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
8 3 7 wb ${wff}\left({\exists }^{*}{x}\in {A}{\phi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\right)$