Theorem xpss2 5665

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

Syntax hints:   → wi 4   ⊆ wss 3904   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-opab 5162  df-xp 5651

This theorem is referenced by:  xpdom3  9043  marypha1lem  9376  canthp1lem2  10608  axresscn  11103  imasvscafn  17550  imasvscaf  17552  gass  19324  gsum2d  19995  pzriprnglem4  21516  pzriprnglem10  21522  tx2cn  23650  txtube  23680  txcmplem1  23681  hausdiag  23685  xkoinjcn  23727  caussi  25339  dvfval  25939  issh2  31358  elrgspnsubrunlem2  33390  qtophaus  34094  2ndmbfm  34519  sxbrsigalem0  34529  cvmlift2lem9  35625  cvmlift2lem11  35627  filnetlem3  36704  bj-idres  37616  idresssidinxp  38777  trclexi  44160  cnvtrcl0  44166  ovolval5lem2  47191  ovnovollem1  47194  ovnovollem2  47195