Theorem xpss2 5687

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

Syntax hints:   → wi 4   ⊆ wss 3941   × cxp 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3948  df-ss 3958  df-opab 5202  df-xp 5673

This theorem is referenced by:  xpdom3  9067  marypha1lem  9425  canthp1lem2  10645  axresscn  11140  imasvscafn  17484  imasvscaf  17486  gass  19209  gsum2d  19884  pzriprnglem4  21341  pzriprnglem10  21347  tx2cn  23438  txtube  23468  txcmplem1  23469  hausdiag  23473  xkoinjcn  23515  caussi  25149  dvfval  25750  issh2  30934  qtophaus  33308  2ndmbfm  33752  sxbrsigalem0  33762  cvmlift2lem9  34793  cvmlift2lem11  34795  filnetlem3  35756  bj-idres  36532  idresssidinxp  37671  trclexi  42885  cnvtrcl0  42891  ovolval5lem2  45879  ovnovollem1  45882  ovnovollem2  45883