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