![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-eu | Structured version Visualization version GIF version |
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 2539). 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 2539, 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 2609, eu2 2608, eu3v 2569, and eu6 2573. 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 2573, while this definition was then proved as dfeu 2594). (Revised by BJ, 30-Sep-2022.) |
Ref | Expression |
---|---|
df-eu | ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | weu 2567 | . 2 wff ∃!𝑥𝜑 |
4 | 1, 2 | wex 1779 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | wmo 2537 | . . 3 wff ∃*𝑥𝜑 |
6 | 4, 5 | wa 395 | . 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑) |
7 | 3, 6 | wb 206 | 1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: eu3v 2569 euex 2576 eumo 2577 exmoeub 2579 moeuex 2581 eubi 2583 eubii 2584 nfeu1ALT 2588 nfeud2 2589 nfeudw 2590 cbveuvw 2604 cbveuw 2605 cbveuALT 2607 eu2 2608 eu4 2614 2euswapv 2629 2euexv 2630 2exeuv 2631 2euex 2640 2euswap 2644 2exeu 2645 2eu4 2654 reu5 3381 eueq 3713 reuss2 4325 n0moeu 4358 reusv2lem1 5396 funcnv3 6634 fnres 6693 mptfnf 6701 fnopabg 6703 brprcneu 6894 brprcneuALT 6895 dff3 7118 finnisoeu 10149 dfac2b 10167 recmulnq 11000 uptx 23623 hausflf2 23996 nosupno 27738 nosupfv 27741 noinfno 27753 noinffv 27756 adjeu 31898 bnj151 34869 bnj600 34911 cbveudavw 36230 bj-eu3f 36820 wl-euae 37496 onsucf1olem 43261 eu0 43511 fzisoeu 45285 ellimciota 45602 euabsneu 47013 iota0ndef 47024 aiota0ndef 47082 reutruALT 48698 mo0sn 48708 thincn0eu 49053 |
Copyright terms: Public domain | W3C validator |