![]() |
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 1774) and uniqueness (df-mo 2528). 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 2528, 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 2598, eu2 2597, eu3v 2558, and eu6 2562. 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 2643). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2562, while this definition was then proved as dfeu 2583). (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 2556 | . 2 wff ∃!𝑥𝜑 |
4 | 1, 2 | wex 1773 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | wmo 2526 | . . 3 wff ∃*𝑥𝜑 |
6 | 4, 5 | wa 394 | . 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑) |
7 | 3, 6 | wb 205 | 1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: eu3v 2558 euex 2565 eumo 2566 exmoeub 2568 moeuex 2570 eubi 2572 eubii 2573 nfeu1ALT 2577 nfeud2 2578 nfeudw 2579 cbveuvw 2593 cbveuw 2594 cbveuALT 2596 eu2 2597 eu4 2603 2euswapv 2618 2euexv 2619 2exeuv 2620 2euex 2629 2euswap 2633 2exeu 2634 2eu4 2643 reu5 3365 eueq 3700 reuss2 4315 n0moeu 4356 reusv2lem1 5398 funcnv3 6624 fnres 6683 mptfnf 6691 fnopabg 6693 brprcneu 6886 brprcneuALT 6887 dff3 7109 finnisoeu 10138 dfac2b 10155 recmulnq 10989 uptx 23573 hausflf2 23946 nosupno 27682 nosupfv 27685 noinfno 27697 noinffv 27700 adjeu 31771 bnj151 34639 bnj600 34681 bj-eu3f 36449 wl-euae 37115 onsucf1olem 42841 eu0 43092 fzisoeu 44820 ellimciota 45140 euabsneu 46548 iota0ndef 46559 aiota0ndef 46615 reutruALT 48063 mo0sn 48072 thincn0eu 48224 |
Copyright terms: Public domain | W3C validator |