Definition df-eu 2569

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1784) and uniqueness (df-mo 2540). 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 2540, 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 2612, eu2 2611, eu3v 2570, and eu6 2574. 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 2656). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2574, while this definition was then proved as dfeu 2595). (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 2568	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1783	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2538	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2570  euex  2577  eumo  2578  exmoeub  2580  moeuex  2582  eubi  2584  eubii  2585  nfeu1ALT  2589  nfeud2  2590  nfeudw  2591  cbveuvw  2606  cbveuw  2607  cbveuALT  2610  eu2  2611  eu4  2617  2euswapv  2632  2euexv  2633  2exeuv  2634  2euex  2643  2euswap  2647  2exeu  2648  2eu4  2656  reu5  3351  eueq  3638  reuss2  4246  n0moeu  4287  reusv2lem1  5316  funcnv3  6488  fnres  6543  mptfnf  6552  fnopabg  6554  brprcneu  6747  fvprc  6748  dff3  6958  finnisoeu  9800  dfac2b  9817  recmulnq  10651  uptx  22684  hausflf2  23057  adjeu  30152  bnj151  32757  bnj600  32799  nosupno  33833  nosupfv  33836  noinfno  33848  noinffv  33851  bj-eu3f  34952  wl-euae  35603  eu0  41025  fzisoeu  42729  ellimciota  43045  euabsneu  44409  iota0ndef  44420  aiota0ndef  44476  reutruALT  46040  mo0sn  46049  thincn0eu  46201