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 2461
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 2497, eu2 2496, eu3v 2485, and eu5 2483 (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 2543). (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 2457 . 2 wff ∃!𝑥𝜑
4 vy . . . . . 6 setvar 𝑦
52, 4weq 1860 . . . . 5 wff 𝑥 = 𝑦
61, 5wb 194 . . . 4 wff (𝜑𝑥 = 𝑦)
76, 2wal 1472 . . 3 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1694 . 2 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
93, 8wb 194 1 wff (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  euequ1  2463  mo2v  2464  euf  2465  nfeu1  2467  nfeud2  2469  eubid  2475  euex  2481  sb8eu  2490  exists1  2548  reu6  3361  euabsn2  4203  euotd  4890  iotauni  5765  iota1  5767  iotanul  5768  iotaex  5770  iota4  5771  fv3  6100  eufnfv  6372  seqomlem2  7410  aceq1  8800  dfac5  8811  bnj89  29834  wl-eudf  32316  wl-euequ1f  32318  wl-sb8eut  32321  iotain  37423  iotaexeu  37424  iotasbc  37425  iotavalsb  37439  sbiota1  37440
  Copyright terms: Public domain W3C validator