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 2650, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460, whose definition we show as mo3 2644. For other possible definitions see moeu 2664 and mo4 2646. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2664, while this definition was then proved as dfmo 2678). (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 2616 | . 2 wff ∃*𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1955 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wi 4 | . . . 4 wff (𝜑 → 𝑥 = 𝑦) |
7 | 6, 2 | wal 1526 | . . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦) |
8 | 7, 4 | wex 1771 | . 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) |
9 | 3, 8 | wb 207 | 1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: nexmo 2619 moim 2622 moimi 2623 nfmo1 2637 nfmod2 2638 nfmodv 2639 mof 2643 mo3 2644 mo4 2646 eu3v 2651 sbmo 2694 mopick 2706 2mo2 2728 mo2icl 3704 rmoanim 3877 axrep6 5189 moabex 5343 dffun3 6360 dffun6f 6363 grothprim 10245 mobidvALT 34079 wl-cbvmotv 34636 wl-moteq 34637 wl-moae 34639 wl-mo2df 34688 wl-mo2t 34693 wl-mo3t 34694 wl-dfrmosb 34735 wl-dfrmov 34736 wl-dfrmof 34737 sn-axrep5v 38988 sn-axprlem3 38989 dffrege115 40204 |
Copyright terms: Public domain | W3C validator |