Metamath Proof Explorer


Theorem ofmresval

Description: Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014)

Ref Expression
Hypotheses ofmresval.f φ F A
ofmresval.g φ G B
Assertion ofmresval φ F f R A × B G = F R f G

Proof

Step Hyp Ref Expression
1 ofmresval.f φ F A
2 ofmresval.g φ G B
3 ovres F A G B F f R A × B G = F R f G
4 1 2 3 syl2anc φ F f R A × B G = F R f G