Theorem xpss1 5650

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

Syntax hints:   → wi 4   ⊆ wss 3911   × cxp 5629

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 3928  df-opab 5165  df-xp 5637

This theorem is referenced by:  ssres2  5964  funssxp  6698  tposssxp  8186  tpostpos2  8203  unxpwdom2  9517  dfac12lem2  10074  unctb  10133  axdc3lem  10379  fpwwe2  10572  pwfseqlem5  10592  imasvscafn  17476  imasvscaf  17478  gasubg  19210  mamures  22260  mdetrlin  22465  mdetrsca  22466  mdetunilem9  22483  mdetmul  22486  tx1cn  23472  cxpcn3  26634  imadifxp  32503  1stmbfm  34224  sxbrsigalem0  34235  cvmlift2lem1  35262  cvmlift2lem9  35271  poimirlem32  37619  dfno2  43390  trclexi  43582  cnvtrcl0  43588  volicoff  45966  volicofmpt  45968  issmflem  46698