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 2498, eu2 2497, eu3v 2486, and eu5 2484 (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 2544). (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 2458 | . 2 wff ∃!𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1861 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wb 195 | . . . 4 wff (𝜑 ↔ 𝑥 = 𝑦) |
7 | 6, 2 | wal 1473 | . . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
8 | 7, 4 | wex 1695 | . 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
9 | 3, 8 | wb 195 | 1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: euequ1 2464 mo2v 2465 euf 2466 nfeu1 2468 nfeud2 2470 eubid 2476 euex 2482 sb8eu 2491 exists1 2549 reu6 3362 euabsn2 4204 euotd 4900 iotauni 5780 iota1 5782 iotanul 5783 iotaex 5785 iota4 5786 fv3 6116 eufnfv 6395 seqomlem2 7433 aceq1 8823 dfac5 8834 bnj89 30041 wl-eudf 32533 wl-euequ1f 32535 wl-sb8eut 32538 iotain 37640 iotaexeu 37641 iotasbc 37642 iotavalsb 37656 sbiota1 37657 |
Copyright terms: Public domain | W3C validator |