Step 
Hyp 
Ref 
Expression 
1 

f1fn 
⊢ ( 𝐹 : 𝐴 –11→ 𝐵 → 𝐹 Fn 𝐴 ) 
2 
1

adantr 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 Fn 𝐴 ) 
3 

simpr 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → ran 𝐹 ⊆ 𝐶 ) 
4 

dff 
⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ) 
5 
2 3 4

sylanbrc 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐶 ) 
6 

dff1 
⊢ ( 𝐹 : 𝐴 –11→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^{◡} 𝐹 ) ) 
7 
6

simprbi 
⊢ ( 𝐹 : 𝐴 –11→ 𝐵 → Fun ^{◡} 𝐹 ) 
8 
7

adantr 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → Fun ^{◡} 𝐹 ) 
9 

dff1 
⊢ ( 𝐹 : 𝐴 –11→ 𝐶 ↔ ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ Fun ^{◡} 𝐹 ) ) 
10 
5 8 9

sylanbrc 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 : 𝐴 –11→ 𝐶 ) 