Definition df-eu 2562

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 2533). The expression E! x ph is read "there exists exactly one x such that ph " or "there exists a unique x such that ph". This is also called the "uniqueness quantifier" but that expression is also used for the at-most-one quantifier df-mo 2533, 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 2603, eu2 2602, eu3v 2563, and eu6 2567. As for double unique existence, beware that the expression E! x E! y ph means "there exists a unique x such that there exists a unique y such that ph " which is a weaker property than "there exists exactly one x and one y such that ph " (see 2eu4 2648). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2567, while this definition was then proved as dfeu 2588). (Revised by BJ, 30-Sep-2022.)

Assertion

Ref	Expression
df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	weu 2561	. 2 wff E! x ph
4	1, 2	wex 1779	. . 3 wff E. x ph
5	1, 2	wmo 2531	. . 3 wff E* x ph
6	4, 5	wa 395	. 2 wff ( E. x ph /\ E* x ph )
7	3, 6	wb 206	1 wff ( E! x ph <-> ( E. x ph /\ E* x ph ) )

This definition is referenced by:  eu3v  2563  euex  2570  eumo  2571  exmoeub  2573  moeuex  2575  eubi  2577  eubii  2578  nfeu1ALT  2582  nfeud2  2583  nfeudw  2584  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  eu2  2602  eu4  2608  2euswapv  2623  2euexv  2624  2exeuv  2625  2euex  2634  2euswap  2638  2exeu  2639  2eu4  2648  reu5  3353  eueq  3676  reuss2  4285  n0moeu  4318  reusv2lem1  5348  funcnv3  6570  fnres  6627  mptfnf  6635  fnopabg  6637  brprcneu  6830  brprcneuALT  6831  dff3  7054  finnisoeu  10044  dfac2b  10062  recmulnq  10895  uptx  23546  hausflf2  23919  nosupno  27649  nosupfv  27652  noinfno  27664  noinffv  27667  adjeu  31869  bnj151  34861  bnj600  34903  cbveudavw  36233  bj-eu3f  36823  wl-euae  37499  onsucf1olem  43253  eu0  43503  fzisoeu  45292  ellimciota  45606  euabsneu  47023  iota0ndef  47034  aiota0ndef  47092  reutruALT  48787  mo0sn  48798  thincn0eu  49414  eufunc  49505  arweutermc  49513