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  5333  funcnv3  6560  fnres  6617  mptfnf  6625  fnopabg  6627  brprcneu  6822  brprcneuALT  6823  dff3  7044  finnisoeu  10024  dfac2b  10042  recmulnq  10876  uptx  23599  hausflf2  23972  nosupno  27686  nosupfv  27689  noinfno  27701  noinffv  27704  adjeu  31980  bnj151  35040  bnj600  35082  cbveudavw  36454  bj-eu3f  37161  bj-axreprepsep  37395  wl-euae  37853  ralrnmo  38693  onsucf1olem  43713  eu0  43962  fzisoeu  45748  ellimciota  46059  euabsneu  47473  iota0ndef  47484  aiota0ndef  47542  reutruALT  49277  mo0sn  49288  thincn0eu  49903  eufunc  49994  arweutermc  50002