Definition df-eu 2567

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

This definition is referenced by:  eu3v  2568  euex  2575  eumo  2576  exmoeub  2578  moeuex  2580  eubi  2582  eubii  2583  nfeu1ALT  2587  nfeud2  2588  nfeudw  2589  cbveuvw  2603  cbveuw  2604  cbveuALT  2606  eu2  2607  eu4  2613  2euswapv  2628  2euexv  2629  2exeuv  2630  2euex  2639  2euswap  2643  2exeu  2644  2eu4  2653  reu5  3365  eueq  3696  reuss2  4306  n0moeu  4339  reusv2lem1  5378  funcnv3  6616  fnres  6675  mptfnf  6683  fnopabg  6685  brprcneu  6876  brprcneuALT  6877  dff3  7100  finnisoeu  10135  dfac2b  10153  recmulnq  10986  uptx  23580  hausflf2  23953  nosupno  27685  nosupfv  27688  noinfno  27700  noinffv  27703  adjeu  31837  bnj151  34866  bnj600  34908  cbveudavw  36227  bj-eu3f  36817  wl-euae  37493  onsucf1olem  43260  eu0  43510  fzisoeu  45284  ellimciota  45601  euabsneu  47013  iota0ndef  47024  aiota0ndef  47082  reutruALT  48698  mo0sn  48708  thincn0eu  49132  eufunc  49220  arweutermc  49228