Theorem xpss2 5660

Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)

Assertion

Ref	Expression
xpss2	⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

Proof of Theorem xpss2

Step	Hyp	Ref	Expression
1		ssid 3971	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5655	. 2 ⊢ ((𝐶 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
3	1, 2	mpan 690	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

Syntax hints:   → wi 4   ⊆ wss 3916   × cxp 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3933  df-opab 5172  df-xp 5646

This theorem is referenced by:  xpdom3  9043  marypha1lem  9390  canthp1lem2  10612  axresscn  11107  imasvscafn  17506  imasvscaf  17508  gass  19239  gsum2d  19908  pzriprnglem4  21400  pzriprnglem10  21406  tx2cn  23503  txtube  23533  txcmplem1  23534  hausdiag  23538  xkoinjcn  23580  caussi  25203  dvfval  25804  issh2  31144  elrgspnsubrunlem2  33205  qtophaus  33832  2ndmbfm  34258  sxbrsigalem0  34268  cvmlift2lem9  35298  cvmlift2lem11  35300  filnetlem3  36363  bj-idres  37143  idresssidinxp  38291  trclexi  43602  cnvtrcl0  43608  ovolval5lem2  46644  ovnovollem1  46647  ovnovollem2  46648