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  3711  rmoanim  3889  axrep6  5293  moabex  5460  dffun3  6558  dffun3OLD  6559  dffun6f  6562  grothprim  10829  mobidvALT  35736  wl-cbvmotv  36382  wl-moteq  36383  wl-moae  36385  wl-mo2df  36435  wl-mo2t  36440  wl-mo3t  36441  sn-axrep5v  41033  sn-axprlem3  41034  dffrege115  42729  mof0  47504