Theorem xpss2 5683

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

Syntax hints:   → wi 4   ⊆ wss 3906   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-opab 5175  df-xp 5669

This theorem is referenced by:  xpdom3  9064  marypha1lem  9394  canthp1lem2  10639  axresscn  11134  imasvscafn  17592  imasvscaf  17594  gass  19372  gsum2d  20043  pzriprnglem4  21615  pzriprnglem10  21621  tx2cn  23748  txtube  23778  txcmplem1  23779  hausdiag  23783  xkoinjcn  23825  caussi  25437  dvfval  26037  issh2  31539  elrgspnsubrunlem2  33546  qtophaus  34204  2ndmbfm  34629  sxbrsigalem0  34639  cvmlift2lem9  35781  cvmlift2lem11  35783  filnetlem3  36869  bj-idres  37782  idresssidinxp  38941  trclexi  44326  cnvtrcl0  44332  ovolval5lem2  47347  ovnovollem1  47350  ovnovollem2  47351