Definition df-eu 2612

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1762) and uniqueness (df-mo 2576). 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 2576, 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 2659, eu2 2658, eu3v 2613, and eu6 2617. 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 2711). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2617, while this definition was then proved as dfeu 2640). (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 2611	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1761	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2574	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 396	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 207	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2613  eu6OLDOLD  2620  euex  2622  eumo  2623  exmoeub  2625  moeuex  2627  eubi  2629  eubii  2630  eubidOLD  2634  nfeu1ALT  2636  nfeud2  2637  moeuOLD  2644  cbveuALT  2656  eu2  2658  eu4  2667  euimOLD  2670  2euswapv  2685  2euexv  2686  2exeuv  2687  2euex  2696  2euswap  2700  2exeu  2701  2eu4  2711  reu5  3390  eueq  3635  reuss2  4203  n0moeu  4236  reusv2lem1  5190  funcnv3  6294  fnres  6344  mptfnf  6351  fnopabg  6353  brprcneu  6530  dff3  6729  finnisoeu  9385  dfac2b  9402  recmulnq  10232  uptx  21917  hausflf2  22290  adjeu  29357  bnj151  31765  bnj600  31807  nosupno  32812  nosupfv  32815  bj-eu3f  33735  wl-euae  34288  wl-dfreusb  34388  wl-dfreuv  34389  wl-dfreuf  34390  eu0  39371  fzisoeu  41108  ellimciota  41437  euabsneu  42779  iota0ndef  42790  aiota0ndef  42811