Theorem funres11

Description: The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998)

	Ref	Expression
Assertion	funres11	⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		resss	⊢ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹
2		cnvss	⊢ ( ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 → ◡ ( 𝐹 ↾ 𝐴 ) ⊆ ◡ 𝐹 )
3		funss	⊢ ( ◡ ( 𝐹 ↾ 𝐴 ) ⊆ ◡ 𝐹 → ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ 𝐴 ) ) )
4	1 2 3	mp2b	⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ 𝐴 ) )