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 2473
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 2509, eu2 2508, eu3v 2497, and eu5 2495 (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 2555). (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 2469 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1871 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 196 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1478 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1701 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 196 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2475  mo2v  2476  euf  2477  nfeu1  2479  nfeud2  2481  eubid  2487  euex  2493  sb8eu  2502  exists1  2560  reu6  3382  euabsn2  4237  euotd  4945  iotauni  5832  iota1  5834  iotanul  5835  iotaex  5837  iota4  5838  fv3  6173  eufnfv  6456  seqomlem2  7506  aceq1  8900  dfac5  8911  bnj89  30548  wl-eudf  33025  wl-euequ1f  33027  wl-sb8eut  33030  iotain  38139  iotaexeu  38140  iotasbc  38141  iotavalsb  38155  sbiota1  38156
  Copyright terms: Public domain W3C validator