Theorem xpss2 5652

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

Syntax hints:   → wi 4   ⊆ wss 3903   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpdom3  9015  marypha1lem  9348  canthp1lem2  10576  axresscn  11071  imasvscafn  17470  imasvscaf  17472  gass  19242  gsum2d  19913  pzriprnglem4  21451  pzriprnglem10  21457  tx2cn  23566  txtube  23596  txcmplem1  23597  hausdiag  23601  xkoinjcn  23643  caussi  25265  dvfval  25866  issh2  31296  elrgspnsubrunlem2  33341  qtophaus  34013  2ndmbfm  34438  sxbrsigalem0  34448  cvmlift2lem9  35524  cvmlift2lem11  35526  filnetlem3  36593  bj-idres  37409  idresssidinxp  38559  trclexi  43970  cnvtrcl0  43976  ovolval5lem2  47005  ovnovollem1  47008  ovnovollem2  47009