Definition df-eu 2597

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1813) and uniqueness (df-mo 2567). 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 2567, 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 2638, eu2 2637, eu3v 2598, and eu6 2602. 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 2682). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2602, while this definition was then proved as dfeu 2623). (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 2596	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1812	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2565	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 401	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 209	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is used by:  eu3v  2598  euex  2605  eumo  2606  exmoeub  2608  moeuex  2610  eubi  2612  nfeu1  2617  nfeud2  2618  nfeudw  2619  cbveuvw  2633  cbveuw  2634  cbveuALT  2636  eu2  2637  eu4  2643  2euswapv  2658  2euexv  2659  2exeuv  2660  2euex  2669  2euswap  2673  2exeu  2674  2eu4  2682  reu5  3371  eueq  3669  reuss2  4274  n0moeu  4310  reusv2lem1  5364  funcnv3  6632  fnres  6688  mptfnf  6696  fnopabg  6698  brprcneu  6898  brprcneuALT  6899  dff3  7124  finnisoeu  10219  dfac2b  10236  recmulnq  11076  uptx  23974  hausflf2  24347  nosupno  28090  nosupfv  28093  noinfno  28105  noinffv  28108  adjeu  32521  bnj151  35577  bnj600  35619  elpsseu  36637  cbveudavw  37218  bj-eu3f  37931  bj-axreprepsep  38182  wl-euae  38641  ralrnmo  39485  onsucf1olem  44464  eu0  44713  fzisoeu  46521  ellimciota  46831  euabsneu  48303  iota0ndef  48314  aiota0ndef  48372  reutruALT  50120  mo0sn  50132  thincn0eu  50771  eufunc  50862  arweutermc  50870  alsanmo  51186