![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-eu | Structured version Visualization version GIF version |
Description: Define existential uniqueness, i.e. "there exists exactly one 𝑥 such that 𝜑." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2640, eu2 2639, eu3v 2627, and eu5 2625 (which in some cases we show with a hypothesis 𝜑 → ∀𝑦𝜑 in place of a distinct variable condition on 𝑦 and 𝜑). Double uniqueness is tricky: ∃!𝑥∃!𝑦𝜑 does not mean "exactly one 𝑥 and one 𝑦 " (see 2eu4 2686). (Contributed by NM, 12-Aug-1993.) |
Ref | Expression |
---|---|
df-eu | ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | weu 2599 | . 2 wff ∃!𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 2032 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wb 196 | . . . 4 wff (𝜑 ↔ 𝑥 = 𝑦) |
7 | 6, 2 | wal 1622 | . . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
8 | 7, 4 | wex 1845 | . 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
9 | 3, 8 | wb 196 | 1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: euequ1 2605 mo2v 2606 euf 2607 nfeu1 2609 nfeud2 2611 eubid 2617 euex 2623 sb8eu 2633 exists1 2691 reu6 3528 euabsn2 4396 euotd 5115 iotauni 6016 iota1 6018 iotanul 6019 iotaex 6021 iota4 6022 fv3 6359 eufnfv 6646 seqomlem2 7707 aceq1 9122 dfac5 9133 bnj89 31088 wl-eudf 33659 wl-euequ1f 33661 wl-sb8eut 33664 iotain 39112 iotaexeu 39113 iotasbc 39114 iotavalsb 39128 sbiota1 39129 |
Copyright terms: Public domain | W3C validator |