Theorem fovrnda

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

	Ref	Expression
Hypothesis	fovrnd.1	|- ( ph -> F : ( R X. S ) --> C )
Assertion	fovrnda	|- ( ( ph /\ ( A e. R /\ B e. S ) ) -> ( A F B ) e. C )

Proof

Step	Hyp	Ref	Expression
1		fovrnd.1	|- ( ph -> F : ( R X. S ) --> C )
2		fovrn	|- ( ( F : ( R X. S ) --> C /\ A e. R /\ B e. S ) -> ( A F B ) e. C )
3	1 2	syl3an1	|- ( ( ph /\ A e. R /\ B e. S ) -> ( A F B ) e. C )
4	3	3expb	|- ( ( ph /\ ( A e. R /\ B e. S ) ) -> ( A F B ) e. C )