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 2654, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460, whose definition we show as mo3 2648. For other possible definitions see moeu 2668 and mo4 2650. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2668, while this definition was then proved as dfmo 2682). (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 2620 | . 2 wff ∃*𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1964 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wi 4 | . . . 4 wff (𝜑 → 𝑥 = 𝑦) |
7 | 6, 2 | wal 1535 | . . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦) |
8 | 7, 4 | wex 1780 | . 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) |
9 | 3, 8 | wb 208 | 1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: nexmo 2623 moim 2626 moimi 2627 nfmo1 2641 nfmod2 2642 nfmodv 2643 mof 2647 mo3 2648 mo4 2650 eu3v 2655 sbmo 2698 mopick 2710 2mo2 2732 mo2icl 3705 rmoanim 3878 axrep6 5197 moabex 5351 dffun3 6366 dffun6f 6369 grothprim 10256 mobidvALT 34181 wl-cbvmotv 34768 wl-moteq 34769 wl-moae 34771 wl-mo2df 34821 wl-mo2t 34826 wl-mo3t 34827 wl-dfrmosb 34868 wl-dfrmov 34869 wl-dfrmof 34870 sn-axrep5v 39157 sn-axprlem3 39158 dffrege115 40373 |
Copyright terms: Public domain | W3C validator |