Definition df-mo 2538

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

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

This definition is referenced by:  nexmo  2539  moim  2542  moimi  2543  nfmo1  2555  nfmod2  2556  nfmodv  2557  mof  2561  mo3  2562  mo4  2564  eu3v  2568  cbvmovw  2600  cbvmow  2601  sbmo  2612  mopick  2623  2mo2  2645  rmoeq1  3400  mo2icl  3704  rmoanim  3876  axrep6  5270  axrep6OLD  5271  moabex  5446  dffun3  6556  dffun3OLD  6557  dffun6f  6560  grothprim  10857  cbvmodavw  36188  mobidvALT  36795  wl-cbvmotv  37451  wl-moteq  37452  wl-moae  37454  wl-mo2df  37508  wl-mo2t  37513  wl-mo3t  37514  sn-axrep5v  42192  sn-axprlem3  42193  dffrege115  43932  mof0  48689