![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > euex | Structured version Visualization version GIF version |
Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.) |
Ref | Expression |
---|---|
euex | ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-eu 2564 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
2 | 1 | simplbi 499 | 1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1782 ∃*wmo 2533 ∃!weu 2563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 398 df-eu 2564 |
This theorem is referenced by: exmoeu 2576 dfeu 2590 euan 2618 euanv 2621 2exeuv 2629 eupickbi 2633 2eu2ex 2640 2exeu 2643 euxfrw 3717 euxfr 3719 eusvnf 5390 eusvnfb 5391 reusv2lem2 5397 reusv2lem3 5398 csbiota 6534 dffv3 6885 tz6.12cOLD 6916 ndmfv 6924 dff3 7099 csbriota 7378 eusvobj2 7398 fnoprabg 7528 zfrep6 7938 dfac5lem5 10119 initoeu1 17958 initoeu1w 17959 initoeu2 17963 termoeu1 17965 termoeu1w 17966 grpidval 18577 0g0 18580 txcn 23122 bnj605 33907 bnj607 33916 bnj906 33930 bnj908 33931 neufal 35280 unqsym1 35299 bj-moeub 35717 moxfr 41416 onexomgt 41976 onexoegt 41979 omabs2 42068 eu2ndop1stv 45820 afveu 45848 afv2eu 45933 tz6.12c-afv2 45937 dfatco 45951 zrninitoringc 46923 thincn0eu 47606 prstchom2ALT 47653 |
Copyright terms: Public domain | W3C validator |