Metamath Proof Explorer


Theorem fovrnda

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

Ref Expression
Hypothesis fovrnd.1 φF:R×SC
Assertion fovrnda φARBSAFBC

Proof

Step Hyp Ref Expression
1 fovrnd.1 φF:R×SC
2 fovrn F:R×SCARBSAFBC
3 1 2 syl3an1 φARBSAFBC
4 3 3expb φARBSAFBC