Theorem xpss2 5545

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

Syntax hints:   → wi 4   ⊆ wss 3843   × cxp 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850  df-ss 3860  df-opab 5093  df-xp 5531

This theorem is referenced by:  xpdom3  8664  marypha1lem  8970  canthp1lem2  10153  axresscn  10648  imasvscafn  16913  imasvscaf  16915  gass  18549  gsum2d  19211  tx2cn  22361  txtube  22391  txcmplem1  22392  hausdiag  22396  xkoinjcn  22438  caussi  24049  dvfval  24649  issh2  29144  qtophaus  31358  2ndmbfm  31798  sxbrsigalem0  31808  cvmlift2lem9  32844  cvmlift2lem11  32846  filnetlem3  34207  bj-idres  34952  idresssidinxp  36067  trclexi  40773  cnvtrcl0  40779  ovolval5lem2  43733  ovnovollem1  43736  ovnovollem2  43737