Description: Obsolete version of imassrn as of 27-Sep-2026. (Contributed by NM, 31-Mar-1995) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | imassrnOLD | |- ( A " B ) C_ ran A |
| 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 |