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
|- ( ph -> A e. V )
ofmresex.b
|- ( ph -> B e. W )
Assertion ofmresex
|- ( ph -> ( oF R |` ( A X. B ) ) e. _V )

Proof

Step Hyp Ref Expression
1 ofmresex.a
 |-  ( ph -> A e. V )
2 ofmresex.b
 |-  ( ph -> B e. W )
3 1 2 xpexd
 |-  ( ph -> ( A X. B ) e. _V )
4 ofexg
 |-  ( ( A X. B ) e. _V -> ( oF R |` ( A X. B ) ) e. _V )
5 3 4 syl
 |-  ( ph -> ( oF R |` ( A X. B ) ) e. _V )