Theorem f1oi

Description: A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Assertion	f1oi	|- ( _I |` A ) : A -1-1-onto-> A

Proof

Step	Hyp	Ref	Expression
1		fnresi	|- ( _I |` A ) Fn A
2		cnvresid	|- `' ( _I |` A ) = ( _I |` A )
3	2	fneq1i	|- ( `' ( _I |` A ) Fn A <-> ( _I |` A ) Fn A )
4	1 3	mpbir	|- `' ( _I |` A ) Fn A
5		dff1o4	|- ( ( _I |` A ) : A -1-1-onto-> A <-> ( ( _I |` A ) Fn A /\ `' ( _I |` A ) Fn A ) )
6	1 4 5	mpbir2an	|- ( _I |` A ) : A -1-1-onto-> A