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 | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | wph | ⊢ 𝜑 | |
| 2 | 1 0 | wmo | ⊢ ∃* 𝑥 𝜑 |
| 3 | vy | ⊢ 𝑦 | |
| 4 | 0 | cv | ⊢ 𝑥 |
| 5 | 3 | cv | ⊢ 𝑦 |
| 6 | 4 5 | wceq | ⊢ 𝑥 = 𝑦 |
| 7 | 1 6 | wi | ⊢ ( 𝜑 → 𝑥 = 𝑦 ) |
| 8 | 7 0 | wal | ⊢ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) |
| 9 | 8 3 | wex | ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) |
| 10 | 2 9 | wb | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |