Theorem fovcdmd

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

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

Proof

Step	Hyp	Ref	Expression
1		fovcdmd.1	|- ( ph -> F : ( R X. S ) --> C )
2		fovcdmd.2	|- ( ph -> A e. R )
3		fovcdmd.3	|- ( ph -> B e. S )
4		fovcdm	|- ( ( 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 )