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 .

Note that the definiens does not express "at-most-one" in the empty domain. Since the hypothesis relies on ax-6 , this case is excluded anyway. Nevertheless, it was suggested to begin with the definition of uniqueness ( eu6 ) and then define the at-most-one quantifier via moeu . Both eu6 and moeu remain valid in the empty domain.

The hypothesis asserts that the definition is independent of the particular choice of the dummy variable y . Without this hypothesis, mojust would be derivable from propositional axioms alone: one could apply the definiens for E* x ph twice, using different dummy variables y and z , and then invoke bitr3i to establish their equivalence. This would jeopardize the independence of axioms, as demonstrated in an analoguous situation involving df-ss to prove ax-8 (see in-ax8 ).

Prefer dfmo unless you can prove the hypothesis from fewer axioms in special cases. (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
Hypothesis	mojust.1	|- ( E. y A. x ( ph -> x = y ) <-> E. z A. x ( ph -> x = z ) )
Assertion	df-mo	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		wph	|- ph
2	1 0	wmo	|- E* x ph
3		vy	|- y
4	0	cv	|- x
5	3	cv	|- y
6	4 5	wceq	|- x = y
7	1 6	wi	|- ( ph -> x = y )
8	7 0	wal	|- A. x ( ph -> x = y )
9	8 3	wex	|- E. y A. x ( ph -> x = y )
10	2 9	wb	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )