![]() |
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 2568 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
2 | 1 | simplbi 499 | 1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1782 ∃*wmo 2537 ∃!weu 2567 |
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 2568 |
This theorem is referenced by: exmoeu 2580 dfeu 2594 euan 2622 euanv 2625 2exeuv 2633 eupickbi 2637 2eu2ex 2644 2exeu 2647 euxfrw 3684 euxfr 3686 eusvnf 5352 eusvnfb 5353 reusv2lem2 5359 reusv2lem3 5360 csbiota 6494 dffv3 6843 tz6.12cOLD 6874 ndmfv 6882 dff3 7055 csbriota 7334 eusvobj2 7354 fnoprabg 7484 zfrep6 7892 dfac5lem5 10070 initoeu1 17904 initoeu1w 17905 initoeu2 17909 termoeu1 17911 termoeu1w 17912 grpidval 18523 0g0 18526 txcn 22993 bnj605 33559 bnj607 33568 bnj906 33582 bnj908 33583 neufal 34907 unqsym1 34926 bj-moeub 35344 moxfr 41044 onexomgt 41604 onexoegt 41607 omabs2 41696 eu2ndop1stv 45431 afveu 45459 afv2eu 45544 tz6.12c-afv2 45548 dfatco 45562 zrninitoringc 46443 thincn0eu 47126 prstchom2ALT 47173 |
Copyright terms: Public domain | W3C validator |