Theorem xpss2 5636

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

Syntax hints:   → wi 4   ⊆ wss 3902   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3919  df-opab 5154  df-xp 5622

This theorem is referenced by:  xpdom3  8988  marypha1lem  9317  canthp1lem2  10541  axresscn  11036  imasvscafn  17438  imasvscaf  17440  gass  19211  gsum2d  19882  pzriprnglem4  21419  pzriprnglem10  21425  tx2cn  23523  txtube  23553  txcmplem1  23554  hausdiag  23558  xkoinjcn  23600  caussi  25222  dvfval  25823  issh2  31184  elrgspnsubrunlem2  33210  qtophaus  33844  2ndmbfm  34269  sxbrsigalem0  34279  cvmlift2lem9  35343  cvmlift2lem11  35345  filnetlem3  36413  bj-idres  37193  idresssidinxp  38341  trclexi  43652  cnvtrcl0  43658  ovolval5lem2  46690  ovnovollem1  46693  ovnovollem2  46694