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 φAV
ofmresex.b φBW
Assertion ofmresex φfRA×BV

Proof

Step Hyp Ref Expression
1 ofmresex.a φAV
2 ofmresex.b φBW
3 1 2 xpexd φA×BV
4 ofexg A×BVfRA×BV
5 3 4 syl φfRA×BV