![]() |
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 2539, eu2 2538, eu3v 2526, and eu5 2524 (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 2585). (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 2498 | . 2 wff ∃!𝑥𝜑 |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 2, 4 | weq 1931 | . . . . 5 wff 𝑥 = 𝑦 |
6 | 1, 5 | wb 196 | . . . 4 wff (𝜑 ↔ 𝑥 = 𝑦) |
7 | 6, 2 | wal 1521 | . . 3 wff ∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
8 | 7, 4 | wex 1744 | . 2 wff ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
9 | 3, 8 | wb 196 | 1 wff (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: euequ1 2504 mo2v 2505 euf 2506 nfeu1 2508 nfeud2 2510 eubid 2516 euex 2522 sb8eu 2532 exists1 2590 reu6 3428 euabsn2 4292 euotd 5004 iotauni 5901 iota1 5903 iotanul 5904 iotaex 5906 iota4 5907 fv3 6244 eufnfv 6531 seqomlem2 7591 aceq1 8978 dfac5 8989 bnj89 30915 wl-eudf 33484 wl-euequ1f 33486 wl-sb8eut 33489 iotain 38935 iotaexeu 38936 iotasbc 38937 iotavalsb 38951 sbiota1 38952 |
Copyright terms: Public domain | W3C validator |