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 * x A φ * x x A φ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 cA class A
2 wph wff φ
3 2 0 1 wrmo wff * x A φ
4 0 cv setvar x
5 4 1 wcel wff x A
6 5 2 wa wff x A φ
7 6 0 wmo wff * x x A φ
8 3 7 wb wff * x A φ * x x A φ