Definition df-eu 2559

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1775) and uniqueness (df-mo 2530). 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 2530, 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 2602, eu2 2601, eu3v 2560, and eu6 2564. 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 2646). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2564, while this definition was then proved as dfeu 2585). (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 2558	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1774	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2528	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2560  euex  2567  eumo  2568  exmoeub  2570  moeuex  2572  eubi  2574  eubii  2575  nfeu1ALT  2579  nfeud2  2580  nfeudw  2581  cbveuvw  2596  cbveuw  2597  cbveuALT  2600  eu2  2601  eu4  2607  2euswapv  2622  2euexv  2623  2exeuv  2624  2euex  2633  2euswap  2637  2exeu  2638  2eu4  2646  reu5  3375  eueq  3703  reuss2  4316  n0moeu  4357  reusv2lem1  5398  funcnv3  6623  fnres  6682  mptfnf  6690  fnopabg  6692  brprcneu  6887  brprcneuALT  6888  dff3  7110  finnisoeu  10137  dfac2b  10154  recmulnq  10988  uptx  23542  hausflf2  23915  nosupno  27649  nosupfv  27652  noinfno  27664  noinffv  27667  adjeu  31712  bnj151  34508  bnj600  34550  bj-eu3f  36318  wl-euae  36984  onsucf1olem  42699  eu0  42950  fzisoeu  44682  ellimciota  45002  euabsneu  46410  iota0ndef  46421  aiota0ndef  46477  reutruALT  47877  mo0sn  47886  thincn0eu  48038