Definition df-eu 2568

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1780) and uniqueness (df-mo 2539). 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 2539, 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 2609, eu2 2608, eu3v 2569, and eu6 2573. 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 2654). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2573, while this definition was then proved as dfeu 2594). (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 2567	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1779	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2537	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 206	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2569  euex  2576  eumo  2577  exmoeub  2579  moeuex  2581  eubi  2583  eubii  2584  nfeu1ALT  2588  nfeud2  2589  nfeudw  2590  cbveuvw  2604  cbveuw  2605  cbveuALT  2607  eu2  2608  eu4  2614  2euswapv  2629  2euexv  2630  2exeuv  2631  2euex  2640  2euswap  2644  2exeu  2645  2eu4  2654  reu5  3381  eueq  3713  reuss2  4325  n0moeu  4358  reusv2lem1  5396  funcnv3  6634  fnres  6693  mptfnf  6701  fnopabg  6703  brprcneu  6894  brprcneuALT  6895  dff3  7118  finnisoeu  10149  dfac2b  10167  recmulnq  11000  uptx  23623  hausflf2  23996  nosupno  27738  nosupfv  27741  noinfno  27753  noinffv  27756  adjeu  31898  bnj151  34869  bnj600  34911  cbveudavw  36230  bj-eu3f  36820  wl-euae  37496  onsucf1olem  43261  eu0  43511  fzisoeu  45285  ellimciota  45602  euabsneu  47013  iota0ndef  47024  aiota0ndef  47082  reutruALT  48698  mo0sn  48708  thincn0eu  49053