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

Definition df-mo 2618
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.)

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 2616 . 2 wff ∃*𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1955 . . . . 5 wff 𝑥 = 𝑦
61, 5wi 4 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1526 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1771 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 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