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 1813) 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 1812	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2563	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 401	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is used 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  3666  reuss2  4272  n0moeu  4307  reusv2lem1  5360  funcnv3  6602  fnres  6658  mptfnf  6666  fnopabg  6668  brprcneu  6867  brprcneuALT  6868  dff3  7092  finnisoeu  10170  dfac2b  10187  recmulnq  11027  uptx  23921  hausflf2  24294  nosupno  28039  nosupfv  28042  noinfno  28054  noinffv  28057  adjeu  32470  bnj151  35487  bnj600  35529  cbveudavw  37007  bj-eu3f  37720  bj-axreprepsep  37956  wl-euae  38414  ralrnmo  39258  onsucf1olem  44227  eu0  44476  fzisoeu  46256  ellimciota  46567  euabsneu  48039  iota0ndef  48050  aiota0ndef  48108  reutruALT  49856  mo0sn  49867  thincn0eu  50480  eufunc  50571  arweutermc  50579  alsanmo  50847