Theorem xpss2 5658

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

Syntax hints:   → wi 4   ⊆ wss 3914   × cxp 5636

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpdom3  9039  marypha1lem  9384  canthp1lem2  10606  axresscn  11101  imasvscafn  17500  imasvscaf  17502  gass  19233  gsum2d  19902  pzriprnglem4  21394  pzriprnglem10  21400  tx2cn  23497  txtube  23527  txcmplem1  23528  hausdiag  23532  xkoinjcn  23574  caussi  25197  dvfval  25798  issh2  31138  elrgspnsubrunlem2  33199  qtophaus  33826  2ndmbfm  34252  sxbrsigalem0  34262  cvmlift2lem9  35298  cvmlift2lem11  35300  filnetlem3  36368  bj-idres  37148  idresssidinxp  38296  trclexi  43609  cnvtrcl0  43615  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655