Metamath Proof Explorer


Definition df-mo

Description: Define the at-most-one quantifier. The expression E* x ph is read "there exists at most one x such that ph ". This is also called the "uniqueness quantifier" but that expression is also used for the unique existential quantifier df-eu , therefore we avoid that ambiguous name.

Notation of BellMachover p. 460, whose definition we show as mo3 . For other possible definitions see moeu and mo4 . (Contributed by Wolf Lammen, 27-May-2019) Make this the definition (which used to be moeu , while this definition was then proved as dfmo ). (Revised by BJ, 30-Sep-2022)

Ref Expression
Assertion df-mo *xφyxφx=y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvarx
1 wph wffφ
2 1 0 wmo wff*xφ
3 vy setvary
4 0 cv setvarx
5 3 cv setvary
6 4 5 wceq wffx=y
7 1 6 wi wffφx=y
8 7 0 wal wffxφx=y
9 8 3 wex wffyxφx=y
10 2 9 wb wff*xφyxφx=y