Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eumo | Structured version Visualization version Unicode version |
Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) |
Ref | Expression |
---|---|
eumo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu5 2496 | . 2 | |
2 | 1 | simprbi 480 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wex 1704 weu 2470 wmo 2471 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-eu 2474 df-mo 2475 |
This theorem is referenced by: eumoi 2500 euimmo 2522 moaneu 2533 eupick 2536 2eumo 2545 2exeu 2549 2eu2 2554 2eu5 2557 moeq3 3383 euabex 4929 nfunsn 6225 dff3 6372 fnoprabg 6761 zfrep6 7134 nqerf 9752 f1otrspeq 17867 uptx 21428 txcn 21429 pm14.12 38622 |
Copyright terms: Public domain | W3C validator |