Theorem xpss2 5697

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

Syntax hints:   → wi 4   ⊆ wss 3949   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683

This theorem is referenced by:  xpdom3  9070  marypha1lem  9428  canthp1lem2  10648  axresscn  11143  imasvscafn  17483  imasvscaf  17485  gass  19165  gsum2d  19840  tx2cn  23114  txtube  23144  txcmplem1  23145  hausdiag  23149  xkoinjcn  23191  caussi  24814  dvfval  25414  issh2  30462  qtophaus  32816  2ndmbfm  33260  sxbrsigalem0  33270  cvmlift2lem9  34302  cvmlift2lem11  34304  filnetlem3  35265  bj-idres  36041  idresssidinxp  37177  trclexi  42371  cnvtrcl0  42377  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  pzriprnglem4  46808  pzriprnglem10  46814