Metamath Proof Explorer


Theorem fovcdmda

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

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

Proof

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