Description: The identity relation is a one-to-one onto function on the universe. (Contributed by NM, 16-May-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | f1ovi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oi | ||
2 | reli | ||
3 | dfrel3 | ||
4 | 2 3 | mpbi | |
5 | f1oeq1 | ||
6 | 4 5 | ax-mp | |
7 | 1 6 | mpbi |