Definition df-mo 2533

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 2562, therefore we avoid that ambiguous name.

Notation of [BellMachover] p. 460, whose definition we show as mo3 2557. For other possible definitions see moeu 2576 and mo4 2559. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2576, while this definition was then proved as dfmo 2589). (Revised by BJ, 30-Sep-2022.)

Assertion

Ref	Expression
df-mo	⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wmo 2531	. 2 wff ∃*𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1962	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wi 4	. . . 4 wff (𝜑 → 𝑥 = 𝑦)
7	6, 2	wal 1538	. . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦)
8	7, 4	wex 1779	. 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
9	3, 8	wb 206	1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

This definition is referenced by:  nexmo  2534  moim  2537  moimi  2538  nfmo1  2550  nfmod2  2551  nfmodv  2552  mof  2556  mo3  2557  mo4  2559  eu3v  2563  cbvmovw  2595  cbvmow  2596  sbmo  2607  mopick  2618  2mo2  2640  rmoeq1  3387  mo2icl  3685  rmoanim  3857  axrep6  5243  axrep6OLD  5244  moabex  5419  dffun3  6525  dffun3OLD  6526  dffun6f  6529  grothprim  10787  cbvmodavw  36238  mobidvALT  36845  wl-cbvmotv  37501  wl-moteq  37502  wl-moae  37504  wl-mo2df  37558  wl-mo2t  37563  wl-mo3t  37564  sn-axrep5v  42204  sn-axprlem3  42205  dffrege115  43967  mof0  48826