Definition df-eu 2563

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 2534). 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 2534, 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 2604, eu2 2603, eu3v 2564, and eu6 2568. 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 2649). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2568, while this definition was then proved as dfeu 2589). (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 2562	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1780	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2532	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 206	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2564  euex  2571  eumo  2572  exmoeub  2574  moeuex  2576  eubi  2578  eubii  2579  nfeu1ALT  2583  nfeud2  2584  nfeudw  2585  cbveuvw  2599  cbveuw  2600  cbveuALT  2602  eu2  2603  eu4  2609  2euswapv  2624  2euexv  2625  2exeuv  2626  2euex  2635  2euswap  2639  2exeu  2640  2eu4  2649  reu5  3346  eueq  3665  reuss2  4274  n0moeu  4307  reusv2lem1  5334  funcnv3  6547  fnres  6604  mptfnf  6612  fnopabg  6614  brprcneu  6807  brprcneuALT  6808  dff3  7028  finnisoeu  9996  dfac2b  10014  recmulnq  10847  uptx  23533  hausflf2  23906  nosupno  27635  nosupfv  27638  noinfno  27650  noinffv  27653  adjeu  31859  bnj151  34879  bnj600  34921  cbveudavw  36264  bj-eu3f  36854  wl-euae  37530  onsucf1olem  43282  eu0  43532  fzisoeu  45320  ellimciota  45633  euabsneu  47038  iota0ndef  47049  aiota0ndef  47107  reutruALT  48815  mo0sn  48826  thincn0eu  49442  eufunc  49533  arweutermc  49541