|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > eumo | Structured version Visualization version GIF version | ||
| Description: Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995.) | 
| Ref | Expression | 
|---|---|
| eumo | ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-eu 2569 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
| 2 | 1 | simprbi 496 | 1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃wex 1779 ∃*wmo 2538 ∃!weu 2568 | 
| 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 2569 | 
| This theorem is referenced by: eumoi 2579 euimmo 2616 moaneu 2623 2exeuv 2632 eupick 2633 2eumo 2642 2exeu 2646 2eu2 2653 2eu5 2656 moeq3 3718 euabex 5466 nfunsn 6948 dff3 7120 fnoprabg 7556 zfrep6 7979 nqerf 10970 f1otrspeq 19465 uptx 23633 txcn 23634 pm14.12 44440 mndtcbas2 49180 | 
| Copyright terms: Public domain | W3C validator |