Theorem xpss2 5674

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

Syntax hints:   → wi 4   ⊆ wss 3926   × cxp 5652

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-opab 5182  df-xp 5660

This theorem is referenced by:  xpdom3  9084  marypha1lem  9445  canthp1lem2  10667  axresscn  11162  imasvscafn  17551  imasvscaf  17553  gass  19284  gsum2d  19953  pzriprnglem4  21445  pzriprnglem10  21451  tx2cn  23548  txtube  23578  txcmplem1  23579  hausdiag  23583  xkoinjcn  23625  caussi  25249  dvfval  25850  issh2  31190  elrgspnsubrunlem2  33243  qtophaus  33867  2ndmbfm  34293  sxbrsigalem0  34303  cvmlift2lem9  35333  cvmlift2lem11  35335  filnetlem3  36398  bj-idres  37178  idresssidinxp  38326  trclexi  43644  cnvtrcl0  43650  ovolval5lem2  46682  ovnovollem1  46685  ovnovollem2  46686