Metamath Proof Explorer


Theorem ofmresex

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

Ref Expression
Hypotheses ofmresex.a φ A V
ofmresex.b φ B W
Assertion ofmresex φ f R A × B V

Proof

Step Hyp Ref Expression
1 ofmresex.a φ A V
2 ofmresex.b φ B W
3 1 2 xpexd φ A × B V
4 ofexg A × B V f R A × B V
5 3 4 syl φ f R A × B V