Definition df-eu 2654

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1781) and uniqueness (df-mo 2622). 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 2622, 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 2694, eu2 2693, eu3v 2655, and eu6 2659. 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 2739). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2659, while this definition was then proved as dfeu 2681). (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 2653	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1780	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2620	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 398	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 208	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2655  euex  2662  eumo  2663  exmoeub  2665  moeuex  2667  eubi  2669  eubii  2670  nfeu1ALT  2675  nfeud2  2676  nfeudw  2677  cbveuALT  2692  eu2  2693  eu4  2699  euimOLD  2702  2euswapv  2715  2euexv  2716  2exeuv  2717  2euex  2726  2euswap  2730  2exeu  2731  2eu4  2739  reu5  3430  eueq  3699  reuss2  4283  n0moeu  4316  reusv2lem1  5299  funcnv3  6424  fnres  6474  mptfnf  6483  fnopabg  6485  brprcneu  6662  dff3  6866  finnisoeu  9539  dfac2b  9556  recmulnq  10386  uptx  22233  hausflf2  22606  adjeu  29666  bnj151  32149  bnj600  32191  nosupno  33203  nosupfv  33206  bj-eu3f  34165  wl-euae  34772  wl-dfreusb  34872  wl-dfreuv  34873  wl-dfreuf  34874  eu0  39935  fzisoeu  41616  ellimciota  41944  euabsneu  43312  iota0ndef  43323  aiota0ndef  43344