Theorem xpss2 5705

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 4006	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5700	. 2 ⊢ ((𝐶 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐵) → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))
3	1, 2	mpan 690	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 × 𝐴) ⊆ (𝐶 × 𝐵))

Syntax hints:   → wi 4   ⊆ wss 3951   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpdom3  9110  marypha1lem  9473  canthp1lem2  10693  axresscn  11188  imasvscafn  17582  imasvscaf  17584  gass  19319  gsum2d  19990  pzriprnglem4  21495  pzriprnglem10  21501  tx2cn  23618  txtube  23648  txcmplem1  23649  hausdiag  23653  xkoinjcn  23695  caussi  25331  dvfval  25932  issh2  31228  elrgspnsubrunlem2  33252  qtophaus  33835  2ndmbfm  34263  sxbrsigalem0  34273  cvmlift2lem9  35316  cvmlift2lem11  35318  filnetlem3  36381  bj-idres  37161  idresssidinxp  38309  trclexi  43633  cnvtrcl0  43639  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672