Metamath Proof Explorer

Theorem imaex

Description: The image of a set is a set. Theorem 3.17 of Monk1 p. 39. (Contributed by JJ, 24-Sep-2021)

Ref Expression
Hypothesis imaex.1 
|- A e. _V
Assertion imaex 
|- ( A " B ) e. _V

Proof

Step Hyp Ref Expression
1 imaex.1 
 |-  A e. _V
2 imaexg 
 |-  ( A e. _V -> ( A " B ) e. _V )
3 1 2 ax-mp 
 |-  ( A " B ) e. _V