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