Definition df-mo 2622

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

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

This definition is referenced by:  nexmo  2623  moim  2626  moimi  2627  nfmo1  2641  nfmod2  2642  nfmodv  2643  mof  2647  mo3  2648  mo4  2650  eu3v  2655  sbmo  2698  mopick  2710  2mo2  2732  mo2icl  3705  rmoanim  3878  axrep6  5197  moabex  5351  dffun3  6366  dffun6f  6369  grothprim  10256  mobidvALT  34181  wl-cbvmotv  34768  wl-moteq  34769  wl-moae  34771  wl-mo2df  34821  wl-mo2t  34826  wl-mo3t  34827  wl-dfrmosb  34868  wl-dfrmov  34869  wl-dfrmof  34870  sn-axrep5v  39157  sn-axprlem3  39158  dffrege115  40373