|   | 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 497 | 1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃wex 1778 ∃*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 207 df-an 396 df-eu 2568 | 
| This theorem is referenced by: exmoeu 2580 dfeu 2594 euan 2620 euanv 2623 2exeuv 2631 eupickbi 2635 2eu2ex 2642 2exeu 2645 euxfrw 3726 euxfr 3728 eusvnf 5391 eusvnfb 5392 reusv2lem2 5398 reusv2lem3 5399 csbiota 6553 dffv3 6901 tz6.12cOLD 6932 ndmfv 6940 dff3 7119 csbriota 7404 eusvobj2 7424 fnoprabg 7557 zfrep6 7980 dfac5lem5 10168 initoeu1 18057 initoeu1w 18058 initoeu2 18062 termoeu1 18064 termoeu1w 18065 grpidval 18675 0g0 18678 zrninitoringc 20677 txcn 23635 bnj605 34922 bnj607 34931 bnj906 34945 bnj908 34946 neufal 36408 unqsym1 36427 bj-moeub 36851 moxfr 42708 onexomgt 43258 onexoegt 43261 omabs2 43350 eu2ndop1stv 47142 afveu 47170 afv2eu 47255 tz6.12c-afv2 47259 dfatco 47273 thincn0eu 49105 termcterm2 49174 termc2 49176 eufunclem 49179 eufunc 49180 euendfunc 49184 arweuthinc 49187 arweutermc 49188 diag1f1o 49192 diag2f1o 49195 prstchom2ALT 49216 | 
| Copyright terms: Public domain | W3C validator |