Theorem xpss1 5640

Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)

Assertion

Ref	Expression
xpss1	⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Proof of Theorem xpss1

Step	Hyp	Ref	Expression
1		ssid 3953	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5636	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
3	1, 2	mpan2 691	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Syntax hints:   → wi 4   ⊆ wss 3898   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-opab 5158  df-xp 5627

This theorem is referenced by:  ssres2  5960  funssxp  6687  tposssxp  8169  tpostpos2  8186  unxpwdom2  9485  dfac12lem2  10047  unctb  10106  axdc3lem  10352  fpwwe2  10545  pwfseqlem5  10565  imasvscafn  17449  imasvscaf  17451  gasubg  19222  mamures  22332  mdetrlin  22537  mdetrsca  22538  mdetunilem9  22555  mdetmul  22558  tx1cn  23544  cxpcn3  26705  imadifxp  32602  1stmbfm  34345  sxbrsigalem0  34356  cvmlift2lem1  35418  cvmlift2lem9  35427  poimirlem32  37765  dfno2  43585  trclexi  43777  cnvtrcl0  43783  volicoff  46155  volicofmpt  46157  issmflem  46887