Theorem xpss2 5639

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

Syntax hints:   → wi 4   ⊆ wss 3898   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-opab 5156  df-xp 5625

This theorem is referenced by:  xpdom3  8995  marypha1lem  9324  canthp1lem2  10551  axresscn  11046  imasvscafn  17443  imasvscaf  17445  gass  19215  gsum2d  19886  pzriprnglem4  21423  pzriprnglem10  21429  tx2cn  23526  txtube  23556  txcmplem1  23557  hausdiag  23561  xkoinjcn  23603  caussi  25225  dvfval  25826  issh2  31191  elrgspnsubrunlem2  33222  qtophaus  33870  2ndmbfm  34295  sxbrsigalem0  34305  cvmlift2lem9  35376  cvmlift2lem11  35378  filnetlem3  36445  bj-idres  37225  idresssidinxp  38367  trclexi  43738  cnvtrcl0  43744  ovolval5lem2  46776  ovnovollem1  46779  ovnovollem2  46780