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 1772) and uniqueness (df-mo 2618). 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 2618, 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 2690, eu2 2689, eu3v 2651, and eu6 2655. 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 2737). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2655, while this definition was then proved as dfeu 2677). (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 2649 | . 2 wff ∃!𝑥𝜑 |
4 | 1, 2 | wex 1771 | . . 3 wff ∃𝑥𝜑 |
5 | 1, 2 | wmo 2616 | . . 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 2651 euex 2658 eumo 2659 exmoeub 2661 moeuex 2663 eubi 2665 eubii 2666 nfeu1ALT 2671 nfeud2 2672 nfeudw 2673 cbveuALT 2688 eu2 2689 eu4 2695 euimOLD 2698 2euswapv 2711 2euexv 2712 2exeuv 2713 2euex 2722 2euswap 2726 2exeu 2727 2eu4 2737 reu5 3431 eueq 3698 reuss2 4282 n0moeu 4315 reusv2lem1 5290 funcnv3 6418 fnres 6468 mptfnf 6477 fnopabg 6479 brprcneu 6656 dff3 6859 finnisoeu 9528 dfac2b 9545 recmulnq 10375 uptx 22163 hausflf2 22536 adjeu 29594 bnj151 32049 bnj600 32091 nosupno 33101 nosupfv 33104 bj-eu3f 34063 wl-euae 34640 wl-dfreusb 34739 wl-dfreuv 34740 wl-dfreuf 34741 eu0 39766 fzisoeu 41447 ellimciota 41775 euabsneu 43144 iota0ndef 43155 aiota0ndef 43176 |
Copyright terms: Public domain | W3C validator |