![]() |
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 1762) and uniqueness (df-mo 2576). 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 2576, 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 2659, eu2 2658, eu3v 2613, and eu6 2617. 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 2711). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2617, while this definition was then proved as dfeu 2640). (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 2611 | . 2 wff ∃!𝑥𝜑 |
4 | 1, 2 | wex 1761 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | wmo 2574 | . . 3 wff ∃*𝑥𝜑 |
6 | 4, 5 | wa 396 | . 2 wff (∃𝑥𝜑 ∧ ∃*𝑥𝜑) |
7 | 3, 6 | wb 207 | 1 wff (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: eu3v 2613 eu6OLDOLD 2620 euex 2622 eumo 2623 exmoeub 2625 moeuex 2627 eubi 2629 eubii 2630 eubidOLD 2634 nfeu1ALT 2636 nfeud2 2637 moeuOLD 2644 cbveuALT 2656 eu2 2658 eu4 2667 euimOLD 2670 2euswapv 2685 2euexv 2686 2exeuv 2687 2euex 2696 2euswap 2700 2exeu 2701 2eu4 2711 reu5 3390 eueq 3635 reuss2 4203 n0moeu 4236 reusv2lem1 5190 funcnv3 6294 fnres 6344 mptfnf 6351 fnopabg 6353 brprcneu 6530 dff3 6729 finnisoeu 9385 dfac2b 9402 recmulnq 10232 uptx 21917 hausflf2 22290 adjeu 29357 bnj151 31765 bnj600 31807 nosupno 32812 nosupfv 32815 bj-eu3f 33735 wl-euae 34288 wl-dfreusb 34388 wl-dfreuv 34389 wl-dfreuf 34390 eu0 39371 fzisoeu 41108 ellimciota 41437 euabsneu 42779 iota0ndef 42790 aiota0ndef 42811 |
Copyright terms: Public domain | W3C validator |