Theorem xpss2 5720

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

Syntax hints:   → wi 4   ⊆ wss 3976   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpdom3  9136  marypha1lem  9502  canthp1lem2  10722  axresscn  11217  imasvscafn  17597  imasvscaf  17599  gass  19341  gsum2d  20014  pzriprnglem4  21518  pzriprnglem10  21524  tx2cn  23639  txtube  23669  txcmplem1  23670  hausdiag  23674  xkoinjcn  23716  caussi  25350  dvfval  25952  issh2  31241  qtophaus  33782  2ndmbfm  34226  sxbrsigalem0  34236  cvmlift2lem9  35279  cvmlift2lem11  35281  filnetlem3  36346  bj-idres  37126  idresssidinxp  38264  trclexi  43582  cnvtrcl0  43588  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578