Metamath Proof Explorer

Theorem imassrn

Description: The image of a class is a subset of its range. Theorem 3.16(xi) of Monk1 p. 39. (Contributed by NM, 31-Mar-1995)

Ref Expression
Assertion imassrn 
|- ( A " B ) C_ ran A

Proof

Step Hyp Ref Expression
1 exsimpr 
 |-  ( E. x ( x e. B /\ <. x , y >. e. A ) -> E. x <. x , y >. e. A )
2 1 ss2abi 
 |-  { y | E. x ( x e. B /\ <. x , y >. e. A ) } C_ { y | E. x <. x , y >. e. A }
3 dfima3 
 |-  ( A " B ) = { y | E. x ( x e. B /\ <. x , y >. e. A ) }
4 dfrn3 
 |-  ran A = { y | E. x <. x , y >. e. A }
5 2 3 4 3sstr4i 
 |-  ( A " B ) C_ ran A