Step 
Hyp 
Ref 
Expression 
1 

dff 
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ) 
2 

fnssres 
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ) 
3 

resss 
⊢ ( 𝐹 ↾ 𝐶 ) ⊆ 𝐹 
4 
3

rnssi 
⊢ ran ( 𝐹 ↾ 𝐶 ) ⊆ ran 𝐹 
5 

sstr 
⊢ ( ( ran ( 𝐹 ↾ 𝐶 ) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) 
6 
4 5

mpan 
⊢ ( ran 𝐹 ⊆ 𝐵 → ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) 
7 
2 6

anim12i 
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ∧ ran 𝐹 ⊆ 𝐵 ) → ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) ) 
8 
7

an32s 
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) ) 
9 
1 8

sylanb 
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) ) 
10 

dff 
⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) ) 
11 
9 10

sylibr 
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ) 