Theorem xpss1 5642

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

Syntax hints:   → wi 4   ⊆ wss 3905   × cxp 5621

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 3922  df-opab 5158  df-xp 5629

This theorem is referenced by:  ssres2  5959  funssxp  6684  tposssxp  8170  tpostpos2  8187  unxpwdom2  9499  dfac12lem2  10058  unctb  10117  axdc3lem  10363  fpwwe2  10556  pwfseqlem5  10576  imasvscafn  17460  imasvscaf  17462  gasubg  19200  mamures  22301  mdetrlin  22506  mdetrsca  22507  mdetunilem9  22524  mdetmul  22527  tx1cn  23513  cxpcn3  26675  imadifxp  32564  1stmbfm  34247  sxbrsigalem0  34258  cvmlift2lem1  35294  cvmlift2lem9  35303  poimirlem32  37651  dfno2  43421  trclexi  43613  cnvtrcl0  43619  volicoff  45996  volicofmpt  45998  issmflem  46728