Description: A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ofexg | |- ( A e. V -> ( oF R |` A ) e. _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-of | |- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
|
2 | 1 | mpofun | |- Fun oF R |
3 | resfunexg | |- ( ( Fun oF R /\ A e. V ) -> ( oF R |` A ) e. _V ) |
|
4 | 2 3 | mpan | |- ( A e. V -> ( oF R |` A ) e. _V ) |