Definition df-eu 2570

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

This definition is referenced by:  eu3v  2571  euex  2578  eumo  2579  exmoeub  2581  moeuex  2583  eubi  2585  nfeu1  2590  nfeud2  2591  nfeudw  2592  cbveuvw  2606  cbveuw  2607  cbveuALT  2609  eu2  2610  eu4  2616  2euswapv  2631  2euexv  2632  2exeuv  2633  2euex  2642  2euswap  2646  2exeu  2647  2eu4  2656  reu5  3345  eueq  3655  reuss2  4267  n0moeu  4300  reusv2lem1  5341  funcnv3  6569  fnres  6626  mptfnf  6634  fnopabg  6636  brprcneu  6831  brprcneuALT  6832  dff3  7053  finnisoeu  10035  dfac2b  10053  recmulnq  10887  uptx  23590  hausflf2  23963  nosupno  27667  nosupfv  27670  noinfno  27682  noinffv  27685  adjeu  31960  bnj151  35019  bnj600  35061  cbveudavw  36433  bj-eu3f  37148  bj-axreprepsep  37382  wl-euae  37842  ralrnmo  38682  onsucf1olem  43698  eu0  43947  fzisoeu  45733  ellimciota  46044  euabsneu  47470  iota0ndef  47481  aiota0ndef  47539  reutruALT  49274  mo0sn  49285  thincn0eu  49900  eufunc  49991  arweutermc  49999