Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence ( df-ex ) and uniqueness ( df-mo ). The expression E! x ph is read "there exists exactly one x such that ph " or "there exists a unique x such that ph ". This is also called the "uniqueness quantifier" but that expression is also used for the at-most-one quantifier df-mo , therefore we avoid that ambiguous name.
Definition 10.1 of BellMachover p. 97; also Definition *14.02 of WhiteheadRussell p. 175. Other possible definitions are given by eu1 , eu2 , eu3v , and eu6 . As for double unique existence, beware that the expression E! x E! y ph means "there exists a unique x such that there exists a unique y such that ph " which is a weaker property than "there exists exactly one x and one y such that ph " (see 2eu4 ). (Contributed by NM, 12-Aug-1993) Make this the definition (which used to be eu6 , while this definition was then proved as dfeu ). (Revised by BJ, 30-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-eu | ⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | wph | ⊢ 𝜑 | |
| 2 | 1 0 | weu | ⊢ ∃! 𝑥 𝜑 |
| 3 | 1 0 | wex | ⊢ ∃ 𝑥 𝜑 |
| 4 | 1 0 | wmo | ⊢ ∃* 𝑥 𝜑 |
| 5 | 3 4 | wa | ⊢ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) |
| 6 | 2 5 | wb | ⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ) |