![]() |
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.) Reduce axiom usage. (Revised by GL, 19-Feb-2022.) |
Ref | Expression |
---|---|
eumo | ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . 2 ⊢ (∃!𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑)) | |
2 | df-mo 2623 | . 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | |
3 | 1, 2 | sylibr 224 | 1 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1852 ∃!weu 2618 ∃*wmo 2619 |
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 197 df-mo 2623 |
This theorem is referenced by: eumoi 2649 euimmo 2671 moaneu 2682 eupick 2685 2eumo 2694 2exeu 2698 2eu2 2703 2eu5 2706 moeq3 3535 euabex 5057 nfunsn 6366 dff3 6515 fnoprabg 6908 zfrep6 7281 nqerf 9954 f1otrspeq 18074 uptx 21649 txcn 21650 pm14.12 39148 |
Copyright terms: Public domain | W3C validator |