Definition df-eu 2564

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1783) and uniqueness (df-mo 2535). 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 2535, 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 2607, eu2 2606, eu3v 2565, and eu6 2569. 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 2651). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2569, while this definition was then proved as dfeu 2590). (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 2563	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1782	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2533	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 397	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2565  euex  2572  eumo  2573  exmoeub  2575  moeuex  2577  eubi  2579  eubii  2580  nfeu1ALT  2584  nfeud2  2585  nfeudw  2586  cbveuvw  2601  cbveuw  2602  cbveuALT  2605  eu2  2606  eu4  2612  2euswapv  2627  2euexv  2628  2exeuv  2629  2euex  2638  2euswap  2642  2exeu  2643  2eu4  2651  reu5  3379  eueq  3704  reuss2  4315  n0moeu  4356  reusv2lem1  5396  funcnv3  6616  fnres  6675  mptfnf  6683  fnopabg  6685  brprcneu  6879  brprcneuALT  6880  dff3  7099  finnisoeu  10105  dfac2b  10122  recmulnq  10956  uptx  23121  hausflf2  23494  nosupno  27196  nosupfv  27199  noinfno  27211  noinffv  27214  adjeu  31130  bnj151  33877  bnj600  33919  bj-eu3f  35709  wl-euae  36375  onsucf1olem  42006  eu0  42257  fzisoeu  43997  ellimciota  44317  euabsneu  45725  iota0ndef  45736  aiota0ndef  45792  reutruALT  47445  mo0sn  47454  thincn0eu  47606