Description: The range of a Cartesian product is included in its second factor. (Contributed by NM, 16-Jan-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rnxpss | |- ran ( A X. B ) C_ B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rn | |- ran ( A X. B ) = dom `' ( A X. B ) |
|
| 2 | cnvxp | |- `' ( A X. B ) = ( B X. A ) |
|
| 3 | 2 | dmeqi | |- dom `' ( A X. B ) = dom ( B X. A ) |
| 4 | dmxpss | |- dom ( B X. A ) C_ B |
|
| 5 | 3 4 | eqsstri | |- dom `' ( A X. B ) C_ B |
| 6 | 1 5 | eqsstri | |- ran ( A X. B ) C_ B |