Definition df-eu 2596

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 2566). 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 2566, 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 2637, eu2 2636, eu3v 2597, and eu6 2601. 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 2681). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2601, while this definition was then proved as dfeu 2622). (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 2595	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1812	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2564	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 401	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is used by:  eu3v  2597  euex  2604  eumo  2605  exmoeub  2607  moeuex  2609  eubi  2611  nfeu1  2616  nfeud2  2617  nfeudw  2618  cbveuvw  2632  cbveuw  2633  cbveuALT  2635  eu2  2636  eu4  2642  2euswapv  2657  2euexv  2658  2exeuv  2659  2euex  2668  2euswap  2672  2exeu  2673  2eu4  2681  reu5  3369  eueq  3669  reuss2  4275  n0moeu  4310  reusv2lem1  5367  funcnv3  6607  fnres  6663  mptfnf  6671  fnopabg  6673  brprcneu  6872  brprcneuALT  6873  dff3  7097  finnisoeu  10120  dfac2b  10137  recmulnq  10977  uptx  23857  hausflf2  24230  nosupno  27947  nosupfv  27950  noinfno  27962  noinffv  27965  adjeu  32378  bnj151  35394  bnj600  35436  cbveudavw  36879  bj-eu3f  37592  bj-axreprepsep  37828  wl-euae  38288  ralrnmo  39117  onsucf1olem  44119  eu0  44368  fzisoeu  46141  ellimciota  46452  euabsneu  47924  iota0ndef  47935  aiota0ndef  47993  reutruALT  49741  mo0sn  49752  thincn0eu  50365  eufunc  50456  arweutermc  50464  alsanmo  50747