Theorem fovrnd

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

	Ref	Expression
Hypotheses	fovrnd.1	|- ( ph -> F : ( R X. S ) --> C )
	fovrnd.2	|- ( ph -> A e. R )
	fovrnd.3	|- ( ph -> B e. S )
Assertion	fovrnd	|- ( ph -> ( A F B ) e. C )

Proof

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