Theorem xpss1 5643

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

Syntax hints:   → wi 4   ⊆ wss 3890   × cxp 5622

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 3907  df-opab 5149  df-xp 5630

This theorem is referenced by:  ssres2  5963  funssxp  6690  tposssxp  8173  tpostpos2  8190  unxpwdom2  9496  dfac12lem2  10058  unctb  10117  axdc3lem  10363  fpwwe2  10557  pwfseqlem5  10577  imasvscafn  17492  imasvscaf  17494  gasubg  19268  mamures  22372  mdetrlin  22577  mdetrsca  22578  mdetunilem9  22595  mdetmul  22598  tx1cn  23584  cxpcn3  26725  imadifxp  32686  1stmbfm  34420  sxbrsigalem0  34431  cvmlift2lem1  35500  cvmlift2lem9  35509  poimirlem32  37987  dfno2  43873  trclexi  44065  cnvtrcl0  44071  volicoff  46441  volicofmpt  46443  issmflem  47173