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 V A B V


Step Hyp Ref Expression
1 imassrn A B ran A
2 rnexg A V ran A V
3 ssexg A B ran A ran A V A B V
4 1 2 3 sylancr A V A B V