Definition df-eu 2568

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1788) and uniqueness (df-mo 2539). 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 2539, 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 2569, and eu6 2573. 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 2655). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2573, while this definition was then proved as dfeu 2594). (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 2567	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1787	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2537	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 399	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2569  euex  2576  eumo  2577  exmoeub  2579  moeuex  2581  eubi  2583  eubii  2584  nfeu1ALT  2588  nfeud2  2589  nfeudw  2590  cbveuvw  2605  cbveuw  2606  cbveuALT  2609  eu2  2610  eu4  2616  2euswapv  2631  2euexv  2632  2exeuv  2633  2euex  2642  2euswap  2646  2exeu  2647  2eu4  2655  reu5  3327  eueq  3610  reuss2  4216  n0moeu  4257  reusv2lem1  5276  funcnv3  6428  fnres  6482  mptfnf  6491  fnopabg  6493  brprcneu  6686  fvprc  6687  dff3  6897  finnisoeu  9692  dfac2b  9709  recmulnq  10543  uptx  22476  hausflf2  22849  adjeu  29924  bnj151  32524  bnj600  32566  nosupno  33592  nosupfv  33595  noinfno  33607  noinffv  33610  bj-eu3f  34711  wl-euae  35362  eu0  40753  fzisoeu  42453  ellimciota  42773  euabsneu  44137  iota0ndef  44148  aiota0ndef  44204  reutruALT  45768  mo0sn  45777  thincn0eu  45929