Definition df-mo 2535

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

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

This definition is referenced by:  nexmo  2536  moim  2539  moimi  2540  nfmo1  2552  nfmod2  2553  nfmodv  2554  mof  2558  mo3  2559  mo4  2561  eu3v  2565  cbvmovw  2597  cbvmow  2598  sbmo  2611  mopick  2622  2mo2  2644  rmoeq1  3415  mo2icl  3710  rmoanim  3888  axrep6  5292  moabex  5459  dffun3  6555  dffun3OLD  6556  dffun6f  6559  grothprim  10826  mobidvALT  35725  wl-cbvmotv  36371  wl-moteq  36372  wl-moae  36374  wl-mo2df  36424  wl-mo2t  36429  wl-mo3t  36430  sn-axrep5v  41030  sn-axprlem3  41031  dffrege115  42715  mof0  47458