| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: "At most one" is preserved through implication (notice wff reversal). |
| Ref | Expression |
|---|---|
| immoi.1 |
|
| Ref | Expression |
|---|---|
| immoi |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | immo 2078 |
. 2
| |
| 2 | immoi.1 |
. 2
| |
| 3 | 1, 2 | mpg 1621 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: moan 2083 moor 2085 mooran1 2086 mooran2 2087 2moex 2103 2euex 2104 2exeu 2109 2eu1 2112 fvex 4778 nfunsn 4792 caoprmo 5096 th3qlem2 5535 brdom3 6377 brdom5 6378 brdom4 6379 ajfuni 10730 funadj 12282 cnlnadjeui 12479 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1592 ax-gen 1593 ax-8 1594 ax-9 1595 ax-10 1596 ax-11 1597 ax-12 1598 ax-17 1605 ax-4 1608 ax-5o 1610 ax-6o 1613 ax-9o 1763 ax-10o 1781 ax-16 1854 ax-11o 1864 |
| This theorem depends on definitions: df-bi 220 df-or 338 df-an 339 df-ex 1616 df-sb 1816 df-eu 2041 df-mo 2042 |