Theorem fssres2

Description: Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005)

	Ref	Expression
Assertion	fssres2	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fssres	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
2		resabs1	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐶 ) = ( 𝐹 ↾ 𝐶 ) )
3	2	feq1d	⊢ ( 𝐶 ⊆ 𝐴 → ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ) )
4	3	adantl	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ) )
5	1 4	mpbid	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )