Description: Any image by a class is included in the range of the class. Theorem 3.16(xi) of Monk1 p. 39. (Contributed by NM, 31-Mar-1995) (Proof shortened by BJ, 27-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | imassrn | |- ( A " B ) C_ ran A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssv | |- B C_ _V |
|
| 2 | imass2 | |- ( B C_ _V -> ( A " B ) C_ ( A " _V ) ) |
|
| 3 | 1 2 | ax-mp | |- ( A " B ) C_ ( A " _V ) |
| 4 | dfrn4 | |- ran A = ( A " _V ) |
|
| 5 | 3 4 | sseqtrri | |- ( A " B ) C_ ran A |