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 2647 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
2 | 1 | simprbi 497 | 1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1771 ∃*wmo 2613 ∃!weu 2646 |
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 208 df-an 397 df-eu 2647 |
This theorem is referenced by: eumoi 2657 euimmo 2693 moaneu 2701 2exeuv 2710 eupick 2711 2eumo 2720 2exeu 2724 2eu2 2731 2eu5 2735 2eu5OLD 2736 moeq3 3700 euabex 5344 nfunsn 6700 dff3 6858 fnoprabg 7264 zfrep6 7645 nqerf 10340 f1otrspeq 18504 uptx 22161 txcn 22162 pm14.12 40630 |
Copyright terms: Public domain | W3C validator |