Theorem xpss1 5651

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

Syntax hints:   → wi 4   ⊆ wss 3903   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-opab 5163  df-xp 5638

This theorem is referenced by:  ssres2  5971  funssxp  6698  tposssxp  8182  tpostpos2  8199  unxpwdom2  9505  dfac12lem2  10067  unctb  10126  axdc3lem  10372  fpwwe2  10566  pwfseqlem5  10586  imasvscafn  17470  imasvscaf  17472  gasubg  19243  mamures  22353  mdetrlin  22558  mdetrsca  22559  mdetunilem9  22576  mdetmul  22579  tx1cn  23565  cxpcn3  26726  imadifxp  32688  1stmbfm  34438  sxbrsigalem0  34449  cvmlift2lem1  35518  cvmlift2lem9  35527  poimirlem32  37903  dfno2  43784  trclexi  43976  cnvtrcl0  43982  volicoff  46353  volicofmpt  46355  issmflem  47085