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 2462
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.)
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 2458 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1861 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 195 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1473 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1695 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 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