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 | |- ( E* x ph <-> E. y A. x ( ph -> x = y ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | wph | |- ph |
|
| 2 | 1 0 | wmo | |- E* x ph |
| 3 | vy | |- y |
|
| 4 | 0 | cv | |- x |
| 5 | 3 | cv | |- y |
| 6 | 4 5 | wceq | |- x = y |
| 7 | 1 6 | wi | |- ( ph -> x = y ) |
| 8 | 7 0 | wal | |- A. x ( ph -> x = y ) |
| 9 | 8 3 | wex | |- E. y A. x ( ph -> x = y ) |
| 10 | 2 9 | wb | |- ( E* x ph <-> E. y A. x ( ph -> x = y ) ) |