Theorem ofexg

Description: A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014)

	Ref	Expression
Assertion	ofexg	$$⊢A\in V\to {{\circ }_{f}R\upharpoonright }_A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-of	$$⊢{\circ }_{f}R=\left(f\in \mathrm{V},g\in \mathrm{V}⟼\left(x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)⟼f\left(x\right)Rg\left(x\right)\right)\right)$$
2	1	mpofun	$$⊢\mathrm{Fun}{\circ }_{f}R$$
3		resfunexg	$$⊢\left(\mathrm{Fun}{\circ }_{f}R\wedge A\in V\right)\to {{\circ }_{f}R\upharpoonright }_A\in \mathrm{V}$$
4	2 3	mpan	$$⊢A\in V\to {{\circ }_{f}R\upharpoonright }_A\in \mathrm{V}$$