Definition df-mo 2540

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

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

This definition is referenced by:  nexmo  2541  moim  2544  moimi  2545  nfmo1  2557  nfmod2  2558  nfmodv  2559  mof  2563  mo3  2564  mo4  2566  eu3v  2570  cbvmovw  2602  cbvmow  2603  sbmo  2616  mopick  2627  2mo2  2649  mo2icl  3644  rmoanim  3823  axrep6  5212  moabex  5368  dffun3  6429  dffun6f  6432  grothprim  10521  mobidvALT  34968  wl-cbvmotv  35599  wl-moteq  35600  wl-moae  35602  wl-mo2df  35652  wl-mo2t  35657  wl-mo3t  35658  sn-axrep5v  40113  sn-axprlem3  40114  dffrege115  41475  mof0  46053