# Metamath Proof Explorer

## Theorem xpss12

Description: Subset theorem for Cartesian product. Generalization of Theorem 101 of Suppes p. 52. (Contributed by NM, 26-Aug-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion xpss12 ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to {A}×{C}\subseteq {B}×{D}$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {B}\to \left({x}\in {A}\to {x}\in {B}\right)$
2 ssel ${⊢}{C}\subseteq {D}\to \left({y}\in {C}\to {y}\in {D}\right)$
3 1 2 im2anan9 ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to \left(\left({x}\in {A}\wedge {y}\in {C}\right)\to \left({x}\in {B}\wedge {y}\in {D}\right)\right)$
4 3 ssopab2dv ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to \left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {C}\right)\right\}\subseteq \left\{⟨{x},{y}⟩|\left({x}\in {B}\wedge {y}\in {D}\right)\right\}$
5 df-xp ${⊢}{A}×{C}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {C}\right)\right\}$
6 df-xp ${⊢}{B}×{D}=\left\{⟨{x},{y}⟩|\left({x}\in {B}\wedge {y}\in {D}\right)\right\}$
7 4 5 6 3sstr4g ${⊢}\left({A}\subseteq {B}\wedge {C}\subseteq {D}\right)\to {A}×{C}\subseteq {B}×{D}$