Definition df-mo 2541

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

Notation of [BellMachover] p. 460, whose definition we show as mo3 2565. For other possible definitions see moeu 2584 and mo4 2567. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2584, while this definition was then proved as dfmo 2597). (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 2539	. 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 1782	. 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
9	3, 8	wb 205	1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

This definition is referenced by:  nexmo  2542  moim  2545  moimi  2546  nfmo1  2558  nfmod2  2559  nfmodv  2560  mof  2564  mo3  2565  mo4  2567  eu3v  2571  cbvmovw  2603  cbvmow  2604  sbmo  2617  mopick  2628  2mo2  2650  mo2icl  3650  rmoanim  3828  axrep6  5217  moabex  5375  dffun3  6450  dffun3OLD  6451  dffun6f  6454  grothprim  10599  mobidvALT  35050  wl-cbvmotv  35681  wl-moteq  35682  wl-moae  35684  wl-mo2df  35734  wl-mo2t  35739  wl-mo3t  35740  sn-axrep5v  40192  sn-axprlem3  40193  dffrege115  41593  mof0  46176