Definition df-mo 2576

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

Notation of [BellMachover] p. 460, whose definition we show as mo3 2604. For other possible definitions see moeu 2628 and mo4 2607. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2628, while this definition was then proved as dfmo 2641). (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 2574	. 2 wff ∃*𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1941	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wi 4	. . . 4 wff (𝜑 → 𝑥 = 𝑦)
7	6, 2	wal 1520	. . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦)
8	7, 4	wex 1761	. 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
9	3, 8	wb 207	1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

This definition is referenced by:  nexmo  2577  moim  2580  moimi  2581  mobiOLD  2585  mobidOLD  2590  nfmo1  2597  nfmod2  2598  nfmodv  2599  mof  2603  mo3  2604  mo3OLD  2605  mo4  2607  eu3v  2613  eu6OLDOLD  2620  sbmo  2666  mopick  2680  2mo2  2702  mo2icl  3641  rmoanim  3806  axrep6  5088  moabex  5243  dffun3  6236  dffun6f  6239  grothprim  10102  mobidvALT  33751  wl-cbvmotv  34284  wl-moteq  34285  wl-moae  34287  wl-mo2df  34337  wl-mo2t  34342  wl-mo3t  34343  wl-dfrmosb  34384  wl-dfrmov  34385  wl-dfrmof  34386  sn-axrep5v  38638  sn-axprlem3  38639  dffrege115  39809