Definition df-mo 2567

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

Notation of [BellMachover] p. 460, whose definition we show as mo3 2592. For other possible definitions see moeu 2611 and mo4 2594.

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

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

Prefer dfmo 2568 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 2611, while this definition was then proved as dfmo 2568). (Revised by BJ, 30-Sep-2022.)

Hypothesis

Ref	Expression
mojust.1	⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))

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 2565	. 2 wff ∃*𝑥𝜑
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	weq 1997	. . . . 5 wff 𝑥 = 𝑦
6	1, 5	wi 4	. . . 4 wff (𝜑 → 𝑥 = 𝑦)
7	6, 2	wal 1568	. . 3 wff ∀𝑥(𝜑 → 𝑥 = 𝑦)
8	7, 4	wex 1812	. 2 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
9	3, 8	wb 209	1 wff (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

This definition is used by:  dfmo  2568