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) Avoid ax-12 . (Revised by TM, 10-Feb-2026)

	Ref	Expression
Assertion	f1oi	⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴

Proof

Step	Hyp	Ref	Expression
1		fnresi	⊢ ( I ↾ 𝐴 ) Fn 𝐴
2		funi	⊢ Fun I
3		cnvi	⊢ ◡ I = I
4	3	funeqi	⊢ ( Fun ◡ I ↔ Fun I )
5	2 4	mpbir	⊢ Fun ◡ I
6		funres11	⊢ ( Fun ◡ I → Fun ◡ ( I ↾ 𝐴 ) )
7	5 6	ax-mp	⊢ Fun ◡ ( I ↾ 𝐴 )
8		rnresi	⊢ ran ( I ↾ 𝐴 ) = 𝐴
9		dff1o2	⊢ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 ↔ ( ( I ↾ 𝐴 ) Fn 𝐴 ∧ Fun ◡ ( I ↾ 𝐴 ) ∧ ran ( I ↾ 𝐴 ) = 𝐴 ) )
10	1 7 8 9	mpbir3an	⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴