Definition df-eu 2566

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 2537). 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 2537, 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 2607, eu2 2606, eu3v 2567, and eu6 2571. 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 2652). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2571, while this definition was then proved as dfeu 2592). (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 2565	. 2 wff E! x ph
4	1, 2	wex 1780	. . 3 wff E. x ph
5	1, 2	wmo 2535	. . 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  2567  euex  2574  eumo  2575  exmoeub  2577  moeuex  2579  eubi  2581  eubii  2582  nfeu1ALT  2586  nfeud2  2587  nfeudw  2588  cbveuvw  2602  cbveuw  2603  cbveuALT  2605  eu2  2606  eu4  2612  2euswapv  2627  2euexv  2628  2exeuv  2629  2euex  2638  2euswap  2642  2exeu  2643  2eu4  2652  reu5  3349  eueq  3663  reuss2  4275  n0moeu  4308  reusv2lem1  5338  funcnv3  6556  fnres  6613  mptfnf  6621  fnopabg  6623  brprcneu  6818  brprcneuALT  6819  dff3  7039  finnisoeu  10011  dfac2b  10029  recmulnq  10862  uptx  23541  hausflf2  23914  nosupno  27643  nosupfv  27646  noinfno  27658  noinffv  27661  adjeu  31871  bnj151  34910  bnj600  34952  cbveudavw  36316  bj-eu3f  36906  wl-euae  37582  onsucf1olem  43387  eu0  43637  fzisoeu  45425  ellimciota  45738  euabsneu  47152  iota0ndef  47163  aiota0ndef  47221  reutruALT  48929  mo0sn  48940  thincn0eu  49556  eufunc  49647  arweutermc  49655