![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-mo | Structured version Visualization version GIF version |
Description: Define the at-most-one
quantifier. The expression ∃*𝑥𝜑 is read
"there exists at most one 𝑥 such that 𝜑". This is also
called
the "uniqueness quantifier" but that expression is also used
for the
unique existential quantifier df-eu 2562, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460, whose definition we show as mo3 2557. For other possible definitions see moeu 2576 and mo4 2559. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2576, while this definition was then proved as dfmo 2589). (Revised by BJ, 30-Sep-2022.) |
Ref | Expression |
---|---|
df-mo | ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wmo 2531 | . 2 wff ∃*𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1966 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wi 4 | . . . 4 wff (𝜑 → 𝑥 = 𝑦) |
7 | 6, 2 | wal 1539 | . . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦) |
8 | 7, 4 | wex 1781 | . 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) |
9 | 3, 8 | wb 205 | 1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: nexmo 2534 moim 2537 moimi 2538 nfmo1 2550 nfmod2 2551 nfmodv 2552 mof 2556 mo3 2557 mo4 2559 eu3v 2563 cbvmovw 2595 cbvmow 2596 sbmo 2609 mopick 2620 2mo2 2642 rmoeq1 3413 mo2icl 3706 rmoanim 3884 axrep6 5285 moabex 5452 dffun3 6546 dffun3OLD 6547 dffun6f 6550 grothprim 10811 mobidvALT 35540 wl-cbvmotv 36186 wl-moteq 36187 wl-moae 36189 wl-mo2df 36239 wl-mo2t 36244 wl-mo3t 36245 sn-axrep5v 40848 sn-axprlem3 40849 dffrege115 42500 mof0 47152 |
Copyright terms: Public domain | W3C validator |