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 ⊢ φ → F : R × S ⟶ C
fovcdmd.2 ⊢ φ → A ∈ R
fovcdmd.3 ⊢ φ → B ∈ S
Assertion fovcdmd ⊢ φ → A F B ∈ C

Proof

Step Hyp Ref Expression
1 fovcdmd.1 ⊢ φ → F : R × S ⟶ C
2 fovcdmd.2 ⊢ φ → A ∈ R
3 fovcdmd.3 ⊢ φ → B ∈ S
4 fovcdm ⊢ F : R × S ⟶ C ∧ A ∈ R ∧ B ∈ S → A F B ∈ C
5 1 2 3 4 syl3anc ⊢ φ → A F B ∈ C