Theorem f1ssres

Description: A function that is one-to-one is also one-to-one on any subclass of its domain. (Contributed by Mario Carneiro, 17-Jan-2015)

	Ref	Expression
Assertion	f1ssres	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fssres	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
3	1 2	sylan	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
4		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
5		funres11	⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
6	4 5	simplbiim	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
7	6	adantr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
8		df-f1	⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ 𝐶 ) ) )
9	3 7 8	sylanbrc	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )