Theorem fovcdmd

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

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

Proof

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