Definition df-eu 2555

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1774) and uniqueness (df-mo 2526). 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 2526, 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 2598, eu2 2597, eu3v 2556, and eu6 2560. 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 2642). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2560, while this definition was then proved as dfeu 2581). (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 2554	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1773	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2524	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2556  euex  2563  eumo  2564  exmoeub  2566  moeuex  2568  eubi  2570  eubii  2571  nfeu1ALT  2575  nfeud2  2576  nfeudw  2577  cbveuvw  2592  cbveuw  2593  cbveuALT  2596  eu2  2597  eu4  2603  2euswapv  2618  2euexv  2619  2exeuv  2620  2euex  2629  2euswap  2633  2exeu  2634  2eu4  2642  reu5  3370  eueq  3697  reuss2  4308  n0moeu  4349  reusv2lem1  5387  funcnv3  6609  fnres  6668  mptfnf  6676  fnopabg  6678  brprcneu  6872  brprcneuALT  6873  dff3  7092  finnisoeu  10105  dfac2b  10122  recmulnq  10956  uptx  23473  hausflf2  23846  nosupno  27577  nosupfv  27580  noinfno  27592  noinffv  27595  adjeu  31637  bnj151  34407  bnj600  34449  bj-eu3f  36221  wl-euae  36887  onsucf1olem  42570  eu0  42821  fzisoeu  44556  ellimciota  44876  euabsneu  46284  iota0ndef  46295  aiota0ndef  46351  reutruALT  47739  mo0sn  47748  thincn0eu  47900