Definition df-eu 2558

Description: Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1775) and uniqueness (df-mo 2529). 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 2529, 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 2601, eu2 2600, eu3v 2559, and eu6 2563. 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 2645). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2563, while this definition was then proved as dfeu 2584). (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 2557	. 2 wff ∃!𝑥𝜑
4	1, 2	wex 1774	. . 3 wff ∃𝑥𝜑
5	1, 2	wmo 2527	. . 3 wff ∃*𝑥𝜑
6	4, 5	wa 395	. 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑)
7	3, 6	wb 205	1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

This definition is referenced by:  eu3v  2559  euex  2566  eumo  2567  exmoeub  2569  moeuex  2571  eubi  2573  eubii  2574  nfeu1ALT  2578  nfeud2  2579  nfeudw  2580  cbveuvw  2595  cbveuw  2596  cbveuALT  2599  eu2  2600  eu4  2606  2euswapv  2621  2euexv  2622  2exeuv  2623  2euex  2632  2euswap  2636  2exeu  2637  2eu4  2645  reu5  3373  eueq  3701  reuss2  4311  n0moeu  4352  reusv2lem1  5392  funcnv3  6617  fnres  6676  mptfnf  6684  fnopabg  6686  brprcneu  6881  brprcneuALT  6882  dff3  7104  finnisoeu  10128  dfac2b  10145  recmulnq  10979  uptx  23516  hausflf2  23889  nosupno  27623  nosupfv  27626  noinfno  27638  noinffv  27641  adjeu  31686  bnj151  34444  bnj600  34486  bj-eu3f  36254  wl-euae  36920  onsucf1olem  42622  eu0  42873  fzisoeu  44605  ellimciota  44925  euabsneu  46333  iota0ndef  46344  aiota0ndef  46400  reutruALT  47800  mo0sn  47809  thincn0eu  47961

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »