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 1960	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wi 4	. . . 4 wff (𝜑 → 𝑥 = 𝑦)
7	6, 2	wal 1535	. . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦)
8	7, 4	wex 1776	. 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  3414  mo2icl  3723  rmoanim  3903  axrep6  5294  axrep6OLD  5295  moabex  5470  dffun3  6577  dffun3OLD  6578  dffun6f  6581  grothprim  10872  cbvmodavw  36233  mobidvALT  36840  wl-cbvmotv  37494  wl-moteq  37495  wl-moae  37497  wl-mo2df  37551  wl-mo2t  37556  wl-mo3t  37557  sn-axrep5v  42234  sn-axprlem3  42235  dffrege115  43968  mof0  48668