Definition df-eu 2572

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1778) and uniqueness (df-mo 2543). 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 2543, 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 2613, eu2 2612, eu3v 2573, and eu6 2577. 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 2658). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2577, while this definition was then proved as dfeu 2598). (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 2571	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1777	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2541	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 206	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2573  euex  2580  eumo  2581  exmoeub  2583  moeuex  2585  eubi  2587  eubii  2588  nfeu1ALT  2592  nfeud2  2593  nfeudw  2594  cbveuvw  2608  cbveuw  2609  cbveuALT  2611  eu2  2612  eu4  2618  2euswapv  2633  2euexv  2634  2exeuv  2635  2euex  2644  2euswap  2648  2exeu  2649  2eu4  2658  reu5  3390  eueq  3730  reuss2  4345  n0moeu  4382  reusv2lem1  5416  funcnv3  6643  fnres  6702  mptfnf  6710  fnopabg  6712  brprcneu  6905  brprcneuALT  6906  dff3  7129  finnisoeu  10176  dfac2b  10194  recmulnq  11027  uptx  23646  hausflf2  24019  nosupno  27758  nosupfv  27761  noinfno  27773  noinffv  27776  adjeu  31913  bnj151  34845  bnj600  34887  cbveudavw  36209  bj-eu3f  36799  wl-euae  37463  onsucf1olem  43227  eu0  43477  fzisoeu  45204  ellimciota  45524  euabsneu  46932  iota0ndef  46943  aiota0ndef  47001  reutruALT  48527  mo0sn  48536  thincn0eu  48688