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 1963	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wi 4	. . . 4 wff (𝜑 → 𝑥 = 𝑦)
7	6, 2	wal 1539	. . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦)
8	7, 4	wex 1780	. 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
9	3, 8	wb 206	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  2609  mopick  2620  2mo2  2642  rmoeq1  3377  mo2icl  3668  rmoanim  3840  axrep6  5224  axrep6OLD  5225  moabex  5397  dffun3  6493  dffun6f  6496  grothprim  10725  cbvmodavw  36294  mobidvALT  36901  wl-cbvmotv  37557  wl-moteq  37558  wl-moae  37560  wl-mo2df  37614  wl-mo2t  37619  wl-mo3t  37620  sn-axrep5v  42319  sn-axprlem3  42320  dffrege115  44081  mof0  48948