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 2568, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460, whose definition we show as mo3 2563. For other possible definitions see moeu 2582 and mo4 2565. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2582, while this definition was then proved as dfmo 2595). (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 2537 | . 2 wff ∃*𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1971 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wi 4 | . . . 4 wff (𝜑 → 𝑥 = 𝑦) |
7 | 6, 2 | wal 1541 | . . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦) |
8 | 7, 4 | wex 1787 | . 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) |
9 | 3, 8 | wb 209 | 1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: nexmo 2540 moim 2543 moimi 2544 nfmo1 2556 nfmod2 2557 nfmodv 2558 mof 2562 mo3 2563 mo4 2565 eu3v 2569 cbvmovw 2601 cbvmow 2602 sbmo 2615 mopick 2626 2mo2 2648 mo2icl 3627 rmoanim 3806 axrep6 5186 moabex 5343 dffun3 6391 dffun6f 6394 grothprim 10448 mobidvALT 34778 wl-cbvmotv 35409 wl-moteq 35410 wl-moae 35412 wl-mo2df 35462 wl-mo2t 35467 wl-mo3t 35468 sn-axrep5v 39907 sn-axprlem3 39908 dffrege115 41263 mof0 45838 |
Copyright terms: Public domain | W3C validator |