MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eu Structured version   Visualization version   GIF version

Definition df-eu 2634
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 2673, eu2 2672, eu3v 2660, and eu5 2658 (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 2720). (Contributed by NM, 12-Aug-1993.)
Assertion
Ref Expression
df-eu (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2weu 2630 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 2054 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 197 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1635 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1859 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 197 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  eubidv  2636  euequi  2638  mo2v  2639  euf  2640  nfeu1  2642  nfeud2  2644  eubid  2650  euex  2656  sb8eu  2666  exists1  2725  reu6  3593  euabsn2  4451  euotd  5168  iotauni  6072  iota1  6074  iotanul  6075  iotaex  6077  iota4  6078  fv3  6422  eufnfv  6712  seqomlem2  7778  aceq1  9219  dfac5  9230  bnj89  31108  wl-eudf  33663  wl-euequif  33665  wl-sb8eut  33668  iotain  39111  iotaexeu  39112  iotasbc  39113  iotavalsb  39127  sbiota1  39128  eusnsn  41644
  Copyright terms: Public domain W3C validator