Theorem xpss2 5651

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

Syntax hints:   → wi 4   ⊆ wss 3889   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpdom3  9013  marypha1lem  9346  canthp1lem2  10576  axresscn  11071  imasvscafn  17501  imasvscaf  17503  gass  19276  gsum2d  19947  pzriprnglem4  21464  pzriprnglem10  21470  tx2cn  23575  txtube  23605  txcmplem1  23606  hausdiag  23610  xkoinjcn  23652  caussi  25264  dvfval  25864  issh2  31280  elrgspnsubrunlem2  33309  qtophaus  33980  2ndmbfm  34405  sxbrsigalem0  34415  cvmlift2lem9  35493  cvmlift2lem11  35495  filnetlem3  36562  bj-idres  37474  idresssidinxp  38635  trclexi  44047  cnvtrcl0  44053  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085