Theorem xpss2 5600

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

Syntax hints:   → wi 4   ⊆ wss 3883   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpdom3  8810  marypha1lem  9122  canthp1lem2  10340  axresscn  10835  imasvscafn  17165  imasvscaf  17167  gass  18822  gsum2d  19488  tx2cn  22669  txtube  22699  txcmplem1  22700  hausdiag  22704  xkoinjcn  22746  caussi  24366  dvfval  24966  issh2  29472  qtophaus  31688  2ndmbfm  32128  sxbrsigalem0  32138  cvmlift2lem9  33173  cvmlift2lem11  33175  filnetlem3  34496  bj-idres  35258  idresssidinxp  36371  trclexi  41117  cnvtrcl0  41123  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085