Definition df-eu 2573

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1787) and uniqueness (df-mo 2543). 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 2543, 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 2614, eu2 2613, eu3v 2574, and eu6 2578. 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 2659). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2578, while this definition was then proved as dfeu 2599). (Revised by BJ, 30-Sep-2022.)

Assertion

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

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	weu 2572	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1786	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2541	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 396	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 207	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2574  euex  2581  eumo  2582  exmoeub  2584  moeuex  2586  eubi  2588  nfeu1  2593  nfeud2  2594  nfeudw  2595  cbveuvw  2609  cbveuw  2610  cbveuALT  2612  eu2  2613  eu4  2619  2euswapv  2634  2euexv  2635  2exeuv  2636  2euex  2645  2euswap  2649  2exeu  2650  2eu4  2659  reu5  3347  eueq  3656  reuss2  4261  n0moeu  4294  reusv2lem1  5334  funcnv3  6562  fnres  6619  mptfnf  6627  fnopabg  6629  brprcneu  6824  brprcneuALT  6825  dff3  7048  finnisoeu  10033  dfac2b  10051  recmulnq  10885  uptx  23615  hausflf2  23988  nosupno  27692  nosupfv  27695  noinfno  27707  noinffv  27710  adjeu  31985  bnj151  35066  bnj600  35108  cbveudavw  36480  bj-eu3f  37195  bj-axreprepsep  37429  wl-euae  37889  ralrnmo  38729  onsucf1olem  43716  eu0  43965  fzisoeu  45749  ellimciota  46060  euabsneu  47492  iota0ndef  47503  aiota0ndef  47561  reutruALT  49296  mo0sn  49307  thincn0eu  49922  eufunc  50013  arweutermc  50021