Definition df-mo 2534

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

Notation of [BellMachover] p. 460, whose definition we show as mo3 2558. For other possible definitions see moeu 2577 and mo4 2560. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2577, while this definition was then proved as dfmo 2590). (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 2532	. 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  2535  moim  2538  moimi  2539  nfmo1  2551  nfmod2  2552  nfmodv  2553  mof  2557  mo3  2558  mo4  2560  eu3v  2564  cbvmovw  2596  cbvmow  2597  sbmo  2608  mopick  2619  2mo2  2641  rmoeq1  3393  mo2icl  3693  rmoanim  3865  axrep6  5251  axrep6OLD  5252  moabex  5427  dffun3  6533  dffun3OLD  6534  dffun6f  6537  grothprim  10805  cbvmodavw  36235  mobidvALT  36842  wl-cbvmotv  37498  wl-moteq  37499  wl-moae  37501  wl-mo2df  37555  wl-mo2t  37560  wl-mo3t  37561  sn-axrep5v  42196  sn-axprlem3  42197  dffrege115  43939  mof0  48758