Metamath Proof Explorer


Theorem f1ovi

Description: The identity relation is a one-to-one onto function on the universe. (Contributed by NM, 16-May-2004)

Ref Expression
Assertion f1ovi I : V 1-1 onto V

Proof

Step Hyp Ref Expression
1 f1oi I V : V 1-1 onto V
2 reli Rel I
3 dfrel3 Rel I I V = I
4 2 3 mpbi I V = I
5 f1oeq1 I V = I I V : V 1-1 onto V I : V 1-1 onto V
6 4 5 ax-mp I V : V 1-1 onto V I : V 1-1 onto V
7 1 6 mpbi I : V 1-1 onto V