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 2603
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 2640, eu2 2639, eu3v 2627, and eu5 2625 (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 2686). (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 2599 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 2032 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 196 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1622 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1845 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 196 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2605  mo2v  2606  euf  2607  nfeu1  2609  nfeud2  2611  eubid  2617  euex  2623  sb8eu  2633  exists1  2691  reu6  3528  euabsn2  4396  euotd  5115  iotauni  6016  iota1  6018  iotanul  6019  iotaex  6021  iota4  6022  fv3  6359  eufnfv  6646  seqomlem2  7707  aceq1  9122  dfac5  9133  bnj89  31088  wl-eudf  33659  wl-euequ1f  33661  wl-sb8eut  33664  iotain  39112  iotaexeu  39113  iotasbc  39114  iotavalsb  39128  sbiota1  39129
  Copyright terms: Public domain W3C validator