Definition df-eu 2557

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

This definition is referenced by:  eu3v  2558  euex  2565  eumo  2566  exmoeub  2568  moeuex  2570  eubi  2572  eubii  2573  nfeu1ALT  2577  nfeud2  2578  nfeudw  2579  cbveuvw  2593  cbveuw  2594  cbveuALT  2596  eu2  2597  eu4  2603  2euswapv  2618  2euexv  2619  2exeuv  2620  2euex  2629  2euswap  2633  2exeu  2634  2eu4  2643  reu5  3365  eueq  3700  reuss2  4315  n0moeu  4356  reusv2lem1  5398  funcnv3  6624  fnres  6683  mptfnf  6691  fnopabg  6693  brprcneu  6886  brprcneuALT  6887  dff3  7109  finnisoeu  10138  dfac2b  10155  recmulnq  10989  uptx  23573  hausflf2  23946  nosupno  27682  nosupfv  27685  noinfno  27697  noinffv  27700  adjeu  31771  bnj151  34639  bnj600  34681  bj-eu3f  36449  wl-euae  37115  onsucf1olem  42841  eu0  43092  fzisoeu  44820  ellimciota  45140  euabsneu  46548  iota0ndef  46559  aiota0ndef  46615  reutruALT  48063  mo0sn  48072  thincn0eu  48224