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 1783) and uniqueness (df-mo 2541). 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 2541, 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 2613, eu2 2612, 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 2657). (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 1782	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2539	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 396	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2571  euex  2578  eumo  2579  exmoeub  2581  moeuex  2583  eubi  2585  eubii  2586  nfeu1ALT  2590  nfeud2  2591  nfeudw  2592  cbveuvw  2607  cbveuw  2608  cbveuALT  2611  eu2  2612  eu4  2618  2euswapv  2633  2euexv  2634  2exeuv  2635  2euex  2644  2euswap  2648  2exeu  2649  2eu4  2657  reu5  3362  eueq  3644  reuss2  4250  n0moeu  4291  reusv2lem1  5322  funcnv3  6511  fnres  6568  mptfnf  6577  fnopabg  6579  brprcneu  6773  brprcneuALT  6774  dff3  6985  finnisoeu  9878  dfac2b  9895  recmulnq  10729  uptx  22785  hausflf2  23158  adjeu  30260  bnj151  32866  bnj600  32908  nosupno  33915  nosupfv  33918  noinfno  33930  noinffv  33933  bj-eu3f  35034  wl-euae  35685  eu0  41134  fzisoeu  42846  ellimciota  43162  euabsneu  44533  iota0ndef  44544  aiota0ndef  44600  reutruALT  46163  mo0sn  46172  thincn0eu  46324