Theorem xpss2 5661

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

Syntax hints:   → wi 4   ⊆ wss 3917   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpdom3  9044  marypha1lem  9391  canthp1lem2  10613  axresscn  11108  imasvscafn  17507  imasvscaf  17509  gass  19240  gsum2d  19909  pzriprnglem4  21401  pzriprnglem10  21407  tx2cn  23504  txtube  23534  txcmplem1  23535  hausdiag  23539  xkoinjcn  23581  caussi  25204  dvfval  25805  issh2  31145  elrgspnsubrunlem2  33206  qtophaus  33833  2ndmbfm  34259  sxbrsigalem0  34269  cvmlift2lem9  35305  cvmlift2lem11  35307  filnetlem3  36375  bj-idres  37155  idresssidinxp  38303  trclexi  43616  cnvtrcl0  43622  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662