Theorem xpss1 5680

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 3959	. 2 ⊢ 𝐶 ⊆ 𝐶
2		xpss12 5676	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
3	1, 2	mpan2 703	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Syntax hints:   → wi 4   ⊆ wss 3905   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-opab 5174  df-xp 5667

This theorem is referenced by:  ssres2  6003  funssxp  6734  tposssxp  8222  tpostpos2  8239  unxpwdom2  9546  dfac12lem2  10124  unctb  10183  axdc3lem  10429  fpwwe2  10623  pwfseqlem5  10643  imasvscafn  17586  imasvscaf  17588  gasubg  19367  mamures  22554  mdetrlin  22759  mdetrsca  22760  mdetunilem9  22777  mdetmul  22780  tx1cn  23766  cxpcn3  26913  imadifxp  32946  1stmbfm  34650  sxbrsigalem0  34661  cvmlift2lem1  35794  cvmlift2lem9  35803  poimirlem32  38303  dfno2  44154  trclexi  44346  cnvtrcl0  44352  volicoff  46709  volicofmpt  46711  issmflem  47441