This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )