Metamath Proof Explorer
Description: A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29Dec2016)


Ref 
Expression 

Hypothesis 
ffvelrnd.1 
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) 

Assertion 
ffvelrnda 
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) ∈ 𝐵 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

ffvelrnd.1 
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) 
2 

ffvelrn 
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) ∈ 𝐵 ) 
3 
1 2

sylan 
⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐶 ) ∈ 𝐵 ) 