Theorem xpss1 5657

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

Syntax hints:   → wi 4   ⊆ wss 3914   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-opab 5170  df-xp 5644

This theorem is referenced by:  ssres2  5975  funssxp  6716  tposssxp  8209  tpostpos2  8226  unxpwdom2  9541  dfac12lem2  10098  unctb  10157  axdc3lem  10403  fpwwe2  10596  pwfseqlem5  10616  imasvscafn  17500  imasvscaf  17502  gasubg  19234  mamures  22284  mdetrlin  22489  mdetrsca  22490  mdetunilem9  22507  mdetmul  22510  tx1cn  23496  cxpcn3  26658  imadifxp  32530  1stmbfm  34251  sxbrsigalem0  34262  cvmlift2lem1  35289  cvmlift2lem9  35298  poimirlem32  37646  dfno2  43417  trclexi  43609  cnvtrcl0  43615  volicoff  45993  volicofmpt  45995  issmflem  46725