Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mo Structured version   Visualization version   GIF version

Definition df-mo 2598
 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 2629, therefore we avoid that ambiguous name. Notation of [BellMachover] p. 460, whose definition we show as mo3 2623. For other possible definitions see moeu 2643 and mo4 2625. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2643, while this definition was then proved as dfmo 2657). (Revised by BJ, 30-Sep-2022.)
Assertion
Ref Expression
df-mo (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-mo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wmo 2596 . 2 wff ∃*𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1964 . . . . 5 wff 𝑥 = 𝑦
61, 5wi 4 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1536 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1781 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 209 1 wff (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
 Colors of variables: wff setvar class This definition is referenced by:  nexmo  2599  moim  2602  moimi  2603  nfmo1  2616  nfmod2  2617  nfmodv  2618  mof  2622  mo3  2623  mo4  2625  eu3v  2630  cbvmow  2663  sbmo  2675  mopick  2687  2mo2  2709  mo2icl  3655  rmoanim  3825  axrep6  5165  moabex  5320  dffun3  6343  dffun6f  6346  grothprim  10263  mobidvALT  34447  wl-cbvmotv  35069  wl-moteq  35070  wl-moae  35072  wl-mo2df  35122  wl-mo2t  35127  wl-mo3t  35128  wl-dfrmosb  35169  wl-dfrmov  35170  wl-dfrmof  35171  sn-axrep5v  39551  sn-axprlem3  39552  dffrege115  40850
 Copyright terms: Public domain W3C validator