Theorem xpss2 5686

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-opab 5179  df-xp 5672

This theorem is used by:  xpdom3  9073  marypha1lem  9403  canthp1lem2  10656  axresscn  11151  imasvscafn  17616  imasvscaf  17618  gass  19402  gsum2d  20073  pzriprnglem4  21671  pzriprnglem10  21677  tx2cn  23804  txtube  23834  txcmplem1  23835  hausdiag  23839  xkoinjcn  23881  caussi  25493  dvfval  26093  issh2  31598  elrgspnsubrunlem2  33599  qtophaus  34257  2ndmbfm  34683  sxbrsigalem0  34693  cvmlift2lem9  35824  cvmlift2lem11  35826  filnetlem3  36932  bj-idres  37845  idresssidinxp  39004  trclexi  44387  cnvtrcl0  44393  ovolval5lem2  47408  ovnovollem1  47411  ovnovollem2  47412