Definition df-eu 2567

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 2538). 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 2538, 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 2610, eu2 2609, eu3v 2568, and eu6 2572. 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 2654). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2572, while this definition was then proved as dfeu 2593). (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 2566	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1780	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2536	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 396	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2568  euex  2575  eumo  2576  exmoeub  2578  moeuex  2580  eubi  2582  eubii  2583  nfeu1ALT  2587  nfeud2  2588  nfeudw  2589  cbveuvw  2604  cbveuw  2605  cbveuALT  2608  eu2  2609  eu4  2615  2euswapv  2630  2euexv  2631  2exeuv  2632  2euex  2641  2euswap  2645  2exeu  2646  2eu4  2654  reu5  3351  eueq  3654  reuss2  4263  n0moeu  4304  reusv2lem1  5342  funcnv3  6555  fnres  6612  mptfnf  6620  fnopabg  6622  brprcneu  6816  brprcneuALT  6817  dff3  7033  finnisoeu  9971  dfac2b  9988  recmulnq  10822  uptx  22883  hausflf2  23256  nosupno  26958  nosupfv  26961  noinfno  26973  noinffv  26976  adjeu  30540  bnj151  33156  bnj600  33198  bj-eu3f  35163  wl-euae  35832  eu0  41501  fzisoeu  43226  ellimciota  43543  euabsneu  44940  iota0ndef  44951  aiota0ndef  45007  reutruALT  46570  mo0sn  46579  thincn0eu  46731