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  3353  eueq  3667  reuss2  4279  n0moeu  4312  reusv2lem1  5344  funcnv3  6563  fnres  6620  mptfnf  6628  fnopabg  6630  brprcneu  6825  brprcneuALT  6826  dff3  7047  finnisoeu  10027  dfac2b  10045  recmulnq  10879  uptx  23573  hausflf2  23946  nosupno  27675  nosupfv  27678  noinfno  27690  noinffv  27693  adjeu  31947  bnj151  35014  bnj600  35056  cbveudavw  36426  bj-eu3f  37017  wl-euae  37693  ralrnmo  38533  onsucf1olem  43548  eu0  43797  fzisoeu  45584  ellimciota  45896  euabsneu  47310  iota0ndef  47321  aiota0ndef  47379  reutruALT  49086  mo0sn  49097  thincn0eu  49712  eufunc  49803  arweutermc  49811