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  3356  eueq  3679  reuss2  4289  n0moeu  4322  reusv2lem1  5353  funcnv3  6586  fnres  6645  mptfnf  6653  fnopabg  6655  brprcneu  6848  brprcneuALT  6849  dff3  7072  finnisoeu  10066  dfac2b  10084  recmulnq  10917  uptx  23512  hausflf2  23885  nosupno  27615  nosupfv  27618  noinfno  27630  noinffv  27633  adjeu  31818  bnj151  34867  bnj600  34909  cbveudavw  36239  bj-eu3f  36829  wl-euae  37505  onsucf1olem  43259  eu0  43509  fzisoeu  45298  ellimciota  45612  euabsneu  47029  iota0ndef  47040  aiota0ndef  47098  reutruALT  48793  mo0sn  48804  thincn0eu  49420  eufunc  49511  arweutermc  49519