Metamath Proof Explorer

Theorem imaexg

Description: The image of a set is a set. Theorem 3.17 of Monk1 p. 39. (Contributed by NM, 24-Jul-1995)

Ref Expression
Assertion imaexg 
|- ( A e. V -> ( A " B ) e. _V )

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( A " B ) C_ ran A
2 rnexg 
 |-  ( A e. V -> ran A e. _V )
3 ssexg 
 |-  ( ( ( A " B ) C_ ran A /\ ran A e. _V ) -> ( A " B ) e. _V )
4 1 2 3 sylancr 
 |-  ( A e. V -> ( A " B ) e. _V )