Definition df-eu 2600

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 2570). 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 2570, 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 2641, eu2 2640, eu3v 2601, and eu6 2605. 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 2685). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2605, while this definition was then proved as dfeu 2626). (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 2599	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1812	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2568	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 401	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is used by:  eu3v  2601  euex  2608  eumo  2609  exmoeub  2611  moeuex  2613  eubi  2615  nfeu1  2620  nfeud2  2621  nfeudw  2622  cbveuvw  2636  cbveuw  2637  cbveuALT  2639  eu2  2640  eu4  2646  2euswapv  2661  2euexv  2662  2exeuv  2663  2euex  2672  2euswap  2676  2exeu  2677  2eu4  2685  reu5  3374  eueq  3674  reuss2  4282  n0moeu  4317  reusv2lem1  5374  funcnv3  6613  fnres  6669  mptfnf  6677  fnopabg  6679  brprcneu  6878  brprcneuALT  6879  dff3  7102  finnisoeu  10116  dfac2b  10133  recmulnq  10967  uptx  23812  hausflf2  24185  nosupno  27897  nosupfv  27900  noinfno  27912  noinffv  27915  adjeu  32271  bnj151  35289  bnj600  35331  cbveudavw  36796  bj-eu3f  37509  bj-axreprepsep  37745  wl-euae  38205  ralrnmo  39043  onsucf1olem  44030  eu0  44279  fzisoeu  46052  ellimciota  46363  euabsneu  47798  iota0ndef  47809  aiota0ndef  47867  reutruALT  49616  mo0sn  49627  thincn0eu  50242  eufunc  50333  arweutermc  50341  alsanmo  50621