Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eumo | Structured version Visualization version GIF version |
Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) |
Ref | Expression |
---|---|
eumo | ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu5 2484 | . 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | |
2 | 1 | simprbi 479 | 1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1695 ∃!weu 2458 ∃*wmo 2459 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-eu 2462 df-mo 2463 |
This theorem is referenced by: eumoi 2488 euimmo 2510 moaneu 2521 eupick 2524 2eumo 2533 2exeu 2537 2eu2 2542 2eu5 2545 moeq3 3350 euabex 4856 nfunsn 6135 dff3 6280 fnoprabg 6659 zfrep6 7027 nqerf 9631 f1otrspeq 17690 uptx 21238 txcn 21239 pm14.12 37644 |
Copyright terms: Public domain | W3C validator |