Definition df-mo 2539

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

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

This definition is referenced by:  nexmo  2540  moim  2543  moimi  2544  nfmo1  2556  nfmod2  2557  nfmodv  2558  mof  2562  mo3  2563  mo4  2565  eu3v  2569  cbvmovw  2601  cbvmow  2602  sbmo  2615  mopick  2626  2mo2  2648  mo2icl  3627  rmoanim  3806  axrep6  5186  moabex  5343  dffun3  6391  dffun6f  6394  grothprim  10448  mobidvALT  34778  wl-cbvmotv  35409  wl-moteq  35410  wl-moae  35412  wl-mo2df  35462  wl-mo2t  35467  wl-mo3t  35468  sn-axrep5v  39907  sn-axprlem3  39908  dffrege115  41263  mof0  45838