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 ran A

Proof

Step Hyp Ref Expression
1 exsimpr x x B x y A x x y A
2 1 ss2abi y | x x B x y A y | x x y A
3 dfima3 A B = y | x x B x y A
4 dfrn3 ran A = y | x x y A
5 2 3 4 3sstr4i A B ran A