Definition df-eu 2595

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1799) and uniqueness (df-mo 2565). 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 2565, 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 2636, eu2 2635, eu3v 2596, and eu6 2600. 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 2680). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2600, while this definition was then proved as dfeu 2621). (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 2594	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1798	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2563	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 399	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 208	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2596  euex  2603  eumo  2604  exmoeub  2606  moeuex  2608  eubi  2610  nfeu1  2615  nfeud2  2616  nfeudw  2617  cbveuvw  2631  cbveuw  2632  cbveuALT  2634  eu2  2635  eu4  2641  2euswapv  2656  2euexv  2657  2exeuv  2658  2euex  2667  2euswap  2671  2exeu  2672  2eu4  2680  reu5  3368  eueq  3670  reuss2  4278  n0moeu  4311  reusv2lem1  5354  funcnv3  6585  fnres  6642  mptfnf  6650  fnopabg  6652  brprcneu  6851  brprcneuALT  6852  dff3  7075  finnisoeu  10064  dfac2b  10082  recmulnq  10917  uptx  23663  hausflf2  24036  nosupno  27742  nosupfv  27745  noinfno  27757  noinffv  27760  adjeu  32036  bnj151  35134  bnj600  35176  cbveudavw  36564  bj-eu3f  37279  bj-axreprepsep  37513  wl-euae  37973  ralrnmo  38813  onsucf1olem  43800  eu0  44049  fzisoeu  45832  ellimciota  46143  euabsneu  47575  iota0ndef  47586  aiota0ndef  47644  reutruALT  49379  mo0sn  49390  thincn0eu  50005  eufunc  50096  arweutermc  50104