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

Syntax hints:   → wi 4   ⊆ wss 3890   × 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 3907  df-opab 5149  df-xp 5638

This theorem is referenced by:  xpdom3  9015  marypha1lem  9348  canthp1lem2  10578  axresscn  11073  imasvscafn  17503  imasvscaf  17505  gass  19278  gsum2d  19949  pzriprnglem4  21466  pzriprnglem10  21472  tx2cn  23577  txtube  23607  txcmplem1  23608  hausdiag  23612  xkoinjcn  23654  caussi  25266  dvfval  25866  issh2  31282  elrgspnsubrunlem2  33311  qtophaus  33982  2ndmbfm  34407  sxbrsigalem0  34417  cvmlift2lem9  35495  cvmlift2lem11  35497  filnetlem3  36564  bj-idres  37476  idresssidinxp  38637  trclexi  44049  cnvtrcl0  44055  ovolval5lem2  47083  ovnovollem1  47086  ovnovollem2  47087