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 2502
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.)
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 2498 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1931 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 196 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1521 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1744 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 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