Theorem xpss2 5644

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

Syntax hints:   → wi 4   ⊆ wss 3901   × cxp 5622

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpdom3  9003  marypha1lem  9336  canthp1lem2  10564  axresscn  11059  imasvscafn  17458  imasvscaf  17460  gass  19230  gsum2d  19901  pzriprnglem4  21439  pzriprnglem10  21445  tx2cn  23554  txtube  23584  txcmplem1  23585  hausdiag  23589  xkoinjcn  23631  caussi  25253  dvfval  25854  issh2  31284  elrgspnsubrunlem2  33330  qtophaus  33993  2ndmbfm  34418  sxbrsigalem0  34428  cvmlift2lem9  35505  cvmlift2lem11  35507  filnetlem3  36574  bj-idres  37361  idresssidinxp  38503  trclexi  43857  cnvtrcl0  43863  ovolval5lem2  46893  ovnovollem1  46896  ovnovollem2  46897