| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Existential uniqueness implies "at most one." |
| Ref | Expression |
|---|---|
| eumo |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eu5 1642 |
. 2
| |
| 2 | 1 | pm3.27bi 351 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: eumoi 1645 euimmo 1653 moaneu 1667 eupick 1671 euor2OLD 1677 2eumo 1683 2eu2 1691 2eu5 1694 moeq3 2265 euabex 3329 reuxfrd 3657 dffun8OLD 4260 zfrep6 4356 fnopabg 4357 nfunsn 4517 dff3 4601 fnoprabg 4752 uptx 10018 isline1 14976 ufileu 15255 pm14.12 16067 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1142 ax-gen 1143 ax-8 1144 ax-9 1145 ax-10 1146 ax-11 1147 ax-12 1148 ax-17 1155 ax-4 1157 ax-5o 1159 ax-6o 1162 ax-9o 1319 ax-10o 1338 ax-16 1418 ax-11o 1426 |
| This theorem depends on definitions: df-bi 163 df-or 240 df-an 241 df-ex 1165 df-sb 1374 df-eu 1613 df-mo 1614 |