Theorem ofmresex

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

	Ref	Expression
Hypotheses	ofmresex.a	$$⊢\phi \to A\in V$$
	ofmresex.b	$$⊢\phi \to B\in W$$
Assertion	ofmresex	$$⊢\phi \to {{\circ }_{f}R\upharpoonright }_{\left(A\times B\right)}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ofmresex.a	$$⊢\phi \to A\in V$$
2		ofmresex.b	$$⊢\phi \to B\in W$$
3	1 2	xpexd	$$⊢\phi \to A\times B\in \mathrm{V}$$
4		ofexg	$$⊢A\times B\in \mathrm{V}\to {{\circ }_{f}R\upharpoonright }_{\left(A\times B\right)}\in \mathrm{V}$$
5	3 4	syl	$$⊢\phi \to {{\circ }_{f}R\upharpoonright }_{\left(A\times B\right)}\in \mathrm{V}$$