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 )