Definition df-eu 2594

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1812) and uniqueness (df-mo 2564). 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 2564, 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 2635, eu2 2634, eu3v 2595, and eu6 2599. 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 2679). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2599, while this definition was then proved as dfeu 2620). (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 2593	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1811	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2562	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 401	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is used by:  eu3v  2595  euex  2602  eumo  2603  exmoeub  2605  moeuex  2607  eubi  2609  nfeu1  2614  nfeud2  2615  nfeudw  2616  cbveuvw  2630  cbveuw  2631  cbveuALT  2633  eu2  2634  eu4  2640  2euswapv  2655  2euexv  2656  2exeuv  2657  2euex  2666  2euswap  2670  2exeu  2671  2eu4  2679  reu5  3367  eueq  3665  reuss2  4271  n0moeu  4306  reusv2lem1  5359  funcnv3  6610  fnres  6666  mptfnf  6674  fnopabg  6676  brprcneu  6875  brprcneuALT  6876  dff3  7100  finnisoeu  10195  dfac2b  10212  recmulnq  11052  uptx  23949  hausflf2  24322  nosupno  28065  nosupfv  28068  noinfno  28080  noinffv  28083  adjeu  32496  bnj151  35553  bnj600  35595  cbveudavw  37132  bj-eu3f  37845  bj-axreprepsep  38083  wl-euae  38542  ralrnmo  39386  onsucf1olem  44365  eu0  44614  fzisoeu  46409  ellimciota  46719  euabsneu  48191  iota0ndef  48202  aiota0ndef  48260  reutruALT  50008  mo0sn  50020  thincn0eu  50659  eufunc  50750  arweutermc  50758  alsanmo  51074