Definition df-eu 2564

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

This definition is referenced by:  eu3v  2565  euex  2572  eumo  2573  exmoeub  2575  moeuex  2577  eubi  2579  eubii  2580  nfeu1ALT  2584  nfeud2  2585  nfeudw  2586  cbveuvw  2600  cbveuw  2601  cbveuALT  2603  eu2  2604  eu4  2610  2euswapv  2625  2euexv  2626  2exeuv  2627  2euex  2636  2euswap  2640  2exeu  2641  2eu4  2650  reu5  3348  eueq  3662  reuss2  4275  n0moeu  4308  reusv2lem1  5338  funcnv3  6557  fnres  6614  mptfnf  6622  fnopabg  6624  brprcneu  6818  brprcneuALT  6819  dff3  7039  finnisoeu  10010  dfac2b  10028  recmulnq  10861  uptx  23546  hausflf2  23919  nosupno  27648  nosupfv  27651  noinfno  27663  noinffv  27666  adjeu  31876  bnj151  34896  bnj600  34938  cbveudavw  36302  bj-eu3f  36892  wl-euae  37568  onsucf1olem  43368  eu0  43618  fzisoeu  45406  ellimciota  45719  euabsneu  47133  iota0ndef  47144  aiota0ndef  47202  reutruALT  48910  mo0sn  48921  thincn0eu  49537  eufunc  49628  arweutermc  49636