Definition df-eu 2562

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 2533). 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 2533, 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 2603, eu2 2602, eu3v 2563, and eu6 2567. 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 2648). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2567, while this definition was then proved as dfeu 2588). (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 2561	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1779	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2531	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 206	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2563  euex  2570  eumo  2571  exmoeub  2573  moeuex  2575  eubi  2577  eubii  2578  nfeu1ALT  2582  nfeud2  2583  nfeudw  2584  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  eu2  2602  eu4  2608  2euswapv  2623  2euexv  2624  2exeuv  2625  2euex  2634  2euswap  2638  2exeu  2639  2eu4  2648  reu5  3347  eueq  3670  reuss2  4279  n0moeu  4312  reusv2lem1  5340  funcnv3  6556  fnres  6613  mptfnf  6621  fnopabg  6623  brprcneu  6816  brprcneuALT  6817  dff3  7038  finnisoeu  10026  dfac2b  10044  recmulnq  10877  uptx  23528  hausflf2  23901  nosupno  27631  nosupfv  27634  noinfno  27646  noinffv  27649  adjeu  31851  bnj151  34843  bnj600  34885  cbveudavw  36224  bj-eu3f  36814  wl-euae  37490  onsucf1olem  43243  eu0  43493  fzisoeu  45282  ellimciota  45596  euabsneu  47013  iota0ndef  47024  aiota0ndef  47082  reutruALT  48777  mo0sn  48788  thincn0eu  49404  eufunc  49495  arweutermc  49503