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 2654 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
2 | 1 | simplbi 500 | 1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1780 ∃*wmo 2620 ∃!weu 2653 |
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 209 df-an 399 df-eu 2654 |
This theorem is referenced by: exmoeu 2666 dfeu 2681 euan 2706 euanv 2709 2exeuv 2717 eupickbi 2721 2eu2ex 2728 2exeu 2731 euxfrw 3714 euxfr 3716 eusvnf 5295 eusvnfb 5296 reusv2lem2 5302 reusv2lem3 5303 csbiota 6350 dffv3 6668 tz6.12c 6697 ndmfv 6702 dff3 6868 csbriota 7131 eusvobj2 7151 fnoprabg 7277 zfrep6 7658 dfac5lem5 9555 initoeu1 17273 initoeu1w 17274 initoeu2 17278 termoeu1 17280 termoeu1w 17281 grpidval 17873 0g0 17876 txcn 22236 bnj605 32181 bnj607 32190 bnj906 32204 bnj908 32205 neufal 33756 unqsym1 33775 bj-moeub 34175 moxfr 39296 eu2ndop1stv 43331 afveu 43359 afv2eu 43444 tz6.12c-afv2 43448 dfatco 43462 zrninitoringc 44349 |
Copyright terms: Public domain | W3C validator |