Definition df-eu 2586

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1790) and uniqueness (df-mo 2556). 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 2556, 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 2627, eu2 2626, eu3v 2587, and eu6 2591. 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 2671). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2591, while this definition was then proved as dfeu 2612). (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 2585	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1789	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2554	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 398	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 208	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2587  euex  2594  eumo  2595  exmoeub  2597  moeuex  2599  eubi  2601  nfeu1  2606  nfeud2  2607  nfeudw  2608  cbveuvw  2622  cbveuw  2623  cbveuALT  2625  eu2  2626  eu4  2632  2euswapv  2647  2euexv  2648  2exeuv  2649  2euex  2658  2euswap  2662  2exeu  2663  2eu4  2671  reu5  3359  eueq  3661  reuss2  4269  n0moeu  4302  reusv2lem1  5345  funcnv3  6576  fnres  6633  mptfnf  6641  fnopabg  6643  brprcneu  6842  brprcneuALT  6843  dff3  7066  finnisoeu  10055  dfac2b  10073  recmulnq  10908  uptx  23654  hausflf2  24027  nosupno  27733  nosupfv  27736  noinfno  27748  noinffv  27751  adjeu  32027  bnj151  35119  bnj600  35161  cbveudavw  36549  bj-eu3f  37264  bj-axreprepsep  37498  wl-euae  37958  ralrnmo  38798  onsucf1olem  43785  eu0  44034  fzisoeu  45817  ellimciota  46128  euabsneu  47560  iota0ndef  47571  aiota0ndef  47629  reutruALT  49364  mo0sn  49375  thincn0eu  49990  eufunc  50081  arweutermc  50089