Theorem fovrnd

Description: An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016)

	Ref	Expression
Hypotheses	fovrnd.1	⊢ ( 𝜑 → 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
	fovrnd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
	fovrnd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
Assertion	fovrnd	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fovrnd.1	⊢ ( 𝜑 → 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
2		fovrnd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
3		fovrnd.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
4		fovrn	⊢ ( ( 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )