Theorem xpss1 5708

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

Syntax hints:   → wi 4   ⊆ wss 3963   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-opab 5211  df-xp 5695

This theorem is referenced by:  ssres2  6025  funssxp  6765  tposssxp  8254  tpostpos2  8271  unxpwdom2  9626  dfac12lem2  10183  unctb  10242  axdc3lem  10488  fpwwe2  10681  pwfseqlem5  10701  imasvscafn  17584  imasvscaf  17586  gasubg  19333  mamures  22417  mdetrlin  22624  mdetrsca  22625  mdetunilem9  22642  mdetmul  22645  tx1cn  23633  cxpcn3  26806  imadifxp  32621  1stmbfm  34242  sxbrsigalem0  34253  cvmlift2lem1  35287  cvmlift2lem9  35296  poimirlem32  37639  dfno2  43418  trclexi  43610  cnvtrcl0  43616  volicoff  45951  volicofmpt  45953  issmflem  46683