Metamath Proof Explorer

Theorem ofexg

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 )

Proof

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 )