Definition df-eu 2563

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1780) and uniqueness (df-mo 2534). 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 2534, 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 2604, eu2 2603, eu3v 2564, and eu6 2568. 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 2649). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2568, while this definition was then proved as dfeu 2589). (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 2562	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1779	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2532	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 206	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2564  euex  2571  eumo  2572  exmoeub  2574  moeuex  2576  eubi  2578  eubii  2579  nfeu1ALT  2583  nfeud2  2584  nfeudw  2585  cbveuvw  2599  cbveuw  2600  cbveuALT  2602  eu2  2603  eu4  2609  2euswapv  2624  2euexv  2625  2exeuv  2626  2euex  2635  2euswap  2639  2exeu  2640  2eu4  2649  reu5  3358  eueq  3681  reuss2  4291  n0moeu  4324  reusv2lem1  5355  funcnv3  6588  fnres  6647  mptfnf  6655  fnopabg  6657  brprcneu  6850  brprcneuALT  6851  dff3  7074  finnisoeu  10072  dfac2b  10090  recmulnq  10923  uptx  23518  hausflf2  23891  nosupno  27621  nosupfv  27624  noinfno  27636  noinffv  27639  adjeu  31824  bnj151  34873  bnj600  34915  cbveudavw  36234  bj-eu3f  36824  wl-euae  37500  onsucf1olem  43252  eu0  43502  fzisoeu  45291  ellimciota  45605  euabsneu  47019  iota0ndef  47030  aiota0ndef  47088  reutruALT  48783  mo0sn  48794  thincn0eu  49400  eufunc  49491  arweutermc  49499