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