Theorem xpss2 5539

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

Syntax hints:   → wi 4   ⊆ wss 3881   × cxp 5517

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpdom3  8598  marypha1lem  8881  canthp1lem2  10064  axresscn  10559  imasvscafn  16802  imasvscaf  16804  gass  18423  gsum2d  19085  tx2cn  22215  txtube  22245  txcmplem1  22246  hausdiag  22250  xkoinjcn  22292  caussi  23901  dvfval  24500  issh2  28992  qtophaus  31189  2ndmbfm  31629  sxbrsigalem0  31639  cvmlift2lem9  32671  cvmlift2lem11  32673  filnetlem3  33841  bj-idres  34575  idresssidinxp  35726  trclexi  40320  cnvtrcl0  40326  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296