Definition df-eu 2595

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1808) and uniqueness (df-mo 2565). 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 2565, 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 2636, eu2 2635, eu3v 2596, and eu6 2600. 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 2680). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2600, while this definition was then proved as dfeu 2621). (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 2594	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1807	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2563	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 400	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2596  euex  2603  eumo  2604  exmoeub  2606  moeuex  2608  eubi  2610  nfeu1  2615  nfeud2  2616  nfeudw  2617  cbveuvw  2631  cbveuw  2632  cbveuALT  2634  eu2  2635  eu4  2641  2euswapv  2656  2euexv  2657  2exeuv  2658  2euex  2667  2euswap  2671  2exeu  2672  2eu4  2680  reu5  3369  eueq  3670  reuss2  4278  n0moeu  4313  reusv2lem1  5369  funcnv3  6606  fnres  6662  mptfnf  6670  fnopabg  6672  brprcneu  6871  brprcneuALT  6872  dff3  7095  finnisoeu  10096  dfac2b  10113  recmulnq  10948  uptx  23761  hausflf2  24134  nosupno  27843  nosupfv  27846  noinfno  27858  noinffv  27861  adjeu  32207  bnj151  35231  bnj600  35273  cbveudavw  36729  bj-eu3f  37442  bj-axreprepsep  37678  wl-euae  38138  ralrnmo  38978  onsucf1olem  43967  eu0  44216  fzisoeu  45989  ellimciota  46300  euabsneu  47732  iota0ndef  47743  aiota0ndef  47801  reutruALT  49550  mo0sn  49561  thincn0eu  50176  eufunc  50267  arweutermc  50275  alsanmo  50555