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 2629
Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1782) and uniqueness (df-mo 2598). The expression ∃!𝑥𝜑 is read "there exists exactly one 𝑥 such that 𝜑 " or "there exists a unique 𝑥 such that 𝜑". This is also called the "uniqueness quantifier" but that expression is also used for the at-most-one quantifier df-mo 2598, therefore we avoid that ambiguous name.

Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2671, eu2 2670, eu3v 2630, and eu6 2634. As for double unique existence, beware that the expression ∃!𝑥∃!𝑦𝜑 means "there exists a unique 𝑥 such that there exists a unique 𝑦 such that 𝜑 " which is a weaker property than "there exists exactly one 𝑥 and one 𝑦 such that 𝜑 " (see 2eu4 2716). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2634, while this definition was then proved as dfeu 2656). (Revised by BJ, 30-Sep-2022.)

Assertion
Ref Expression
df-eu (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2weu 2628 . 2 wff ∃!𝑥𝜑
41, 2wex 1781 . . 3 wff 𝑥𝜑
51, 2wmo 2596 . . 3 wff ∃*𝑥𝜑
64, 5wa 399 . 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
73, 6wb 209 1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  eu3v  2630  euex  2637  eumo  2638  exmoeub  2640  moeuex  2642  eubi  2644  eubii  2645  nfeu1ALT  2650  nfeud2  2651  nfeudw  2652  cbveuw  2666  cbveuALT  2669  eu2  2670  eu4  2676  euimOLD  2679  2euswapv  2692  2euexv  2693  2exeuv  2694  2euex  2703  2euswap  2707  2exeu  2708  2eu4  2716  reu5  3375  eueq  3647  reuss2  4235  n0moeu  4270  reusv2lem1  5264  funcnv3  6394  fnres  6446  mptfnf  6455  fnopabg  6457  brprcneu  6637  dff3  6843  finnisoeu  9524  dfac2b  9541  recmulnq  10375  uptx  22230  hausflf2  22603  adjeu  29672  bnj151  32259  bnj600  32301  nosupno  33316  nosupfv  33319  bj-eu3f  34280  wl-euae  34922  wl-dfreusb  35022  wl-dfreuv  35023  wl-dfreuf  35024  eu0  40226  fzisoeu  41930  ellimciota  42254  euabsneu  43618  iota0ndef  43629  aiota0ndef  43650
  Copyright terms: Public domain W3C validator