Definition df-eu 2599

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1803) and uniqueness (df-mo 2569). 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 2569, 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 2640, eu2 2639, eu3v 2600, and eu6 2604. 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 2684). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2604, while this definition was then proved as dfeu 2625). (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 2598	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1802	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2567	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 400	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2600  euex  2607  eumo  2608  exmoeub  2610  moeuex  2612  eubi  2614  nfeu1  2619  nfeud2  2620  nfeudw  2621  cbveuvw  2635  cbveuw  2636  cbveuALT  2638  eu2  2639  eu4  2645  2euswapv  2660  2euexv  2661  2exeuv  2662  2euex  2671  2euswap  2675  2exeu  2676  2eu4  2684  reu5  3372  eueq  3674  reuss2  4281  n0moeu  4315  reusv2lem1  5360  funcnv3  6595  fnres  6652  mptfnf  6660  fnopabg  6662  brprcneu  6861  brprcneuALT  6862  dff3  7085  finnisoeu  10085  dfac2b  10102  recmulnq  10937  uptx  23743  hausflf2  24116  nosupno  27825  nosupfv  27828  noinfno  27840  noinffv  27843  adjeu  32150  bnj151  35182  bnj600  35224  cbveudavw  36624  bj-eu3f  37338  bj-axreprepsep  37572  wl-euae  38032  ralrnmo  38872  onsucf1olem  43859  eu0  44108  fzisoeu  45877  ellimciota  46188  euabsneu  47620  iota0ndef  47631  aiota0ndef  47689  reutruALT  49434  mo0sn  49445  thincn0eu  50060  eufunc  50151  arweutermc  50159