Definition df-eu 2565

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1775) and uniqueness (df-mo 2536). 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 2536, 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 2606, eu2 2605, eu3v 2566, and eu6 2570. 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 2570, while this definition was then proved as dfeu 2591). (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 2564	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1774	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2534	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 206	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2566  euex  2573  eumo  2574  exmoeub  2576  moeuex  2578  eubi  2580  eubii  2581  nfeu1ALT  2585  nfeud2  2586  nfeudw  2587  cbveuvw  2601  cbveuw  2602  cbveuALT  2604  eu2  2605  eu4  2611  2euswapv  2626  2euexv  2627  2exeuv  2628  2euex  2637  2euswap  2641  2exeu  2642  2eu4  2651  reu5  3378  eueq  3717  reuss2  4332  n0moeu  4365  reusv2lem1  5399  funcnv3  6633  fnres  6691  mptfnf  6699  fnopabg  6701  brprcneu  6891  brprcneuALT  6892  dff3  7114  finnisoeu  10144  dfac2b  10162  recmulnq  10995  uptx  23630  hausflf2  24003  nosupno  27744  nosupfv  27747  noinfno  27759  noinffv  27762  adjeu  31899  bnj151  34831  bnj600  34873  cbveudavw  36194  bj-eu3f  36784  wl-euae  37458  onsucf1olem  43218  eu0  43468  fzisoeu  45201  ellimciota  45520  euabsneu  46928  iota0ndef  46939  aiota0ndef  46997  reutruALT  48575  mo0sn  48585  thincn0eu  48753