Theorem xpss2 5679

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902   × cxp 5657

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-opab 5172  df-xp 5665

This theorem is used by:  xpdom3  9077  marypha1lem  9407  canthp1lem2  10666  axresscn  11161  imasvscafn  17629  imasvscaf  17631  gass  19434  gsum2d  20105  pzriprnglem4  21703  pzriprnglem10  21709  tx2cn  23842  txtube  23872  txcmplem1  23873  hausdiag  23877  xkoinjcn  23919  caussi  25531  dvfval  26131  issh2  31698  elrgspnsubrunlem2  33696  qtophaus  34354  2ndmbfm  34780  sxbrsigalem0  34790  cvmlift2lem9  35898  cvmlift2lem11  35900  filnetlem3  37007  bj-idres  37920  idresssidinxp  39070  trclexi  44468  cnvtrcl0  44474  ovolval5lem2  47489  ovnovollem1  47492  ovnovollem2  47493