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  3354  eueq  3668  reuss2  4280  n0moeu  4313  reusv2lem1  5345  funcnv3  6570  fnres  6627  mptfnf  6635  fnopabg  6637  brprcneu  6832  brprcneuALT  6833  dff3  7054  finnisoeu  10035  dfac2b  10053  recmulnq  10887  uptx  23581  hausflf2  23954  nosupno  27683  nosupfv  27686  noinfno  27698  noinffv  27701  adjeu  31976  bnj151  35052  bnj600  35094  cbveudavw  36464  bj-eu3f  37080  bj-axreprepsep  37314  wl-euae  37761  ralrnmo  38601  onsucf1olem  43616  eu0  43865  fzisoeu  45651  ellimciota  45963  euabsneu  47377  iota0ndef  47388  aiota0ndef  47446  reutruALT  49153  mo0sn  49164  thincn0eu  49779  eufunc  49870  arweutermc  49878