Definition df-mo

Description: Define the at-most-one quantifier. The expression E* x ph is read "there exists at most one x such that ph ". This is also called the "uniqueness quantifier" but that expression is also used for the unique existential quantifier df-eu , therefore we avoid that ambiguous name.

Notation of BellMachover p. 460, whose definition we show as mo3 . For other possible definitions see moeu and mo4 . (Contributed by Wolf Lammen, 27-May-2019) Make this the definition (which used to be moeu , while this definition was then proved as dfmo ). (Revised by BJ, 30-Sep-2022)

	Ref	Expression
Assertion	df-mo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wmo	$$wff{\exists }^{*}x\phi$$
3		vy	$$setvary$$
4	0	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	4 5	wceq	$$wffx=y$$
7	1 6	wi	$$wff\left(\phi \to x=y\right)$$
8	7 0	wal	$$wff\forall x\left(\phi \to x=y\right)$$
9	8 3	wex	$$wff\exists y\forall x\left(\phi \to x=y\right)$$
10	2 9	wb	$$wff\left({\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$