Theorem xpss1 5678

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

Syntax hints:   → wi 4   ⊆ wss 3913   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-opab 5175  df-xp 5665

This theorem is referenced by:  ssres2  6001  funssxp  6732  tposssxp  8222  tpostpos2  8239  unxpwdom2  9546  dfac12lem2  10124  unctb  10183  axdc3lem  10430  fpwwe2  10624  pwfseqlem5  10644  imasvscafn  17587  imasvscaf  17589  gasubg  19368  mamures  22519  mdetrlin  22724  mdetrsca  22725  mdetunilem9  22742  mdetmul  22745  tx1cn  23731  cxpcn3  26875  imadifxp  32883  1stmbfm  34591  sxbrsigalem0  34602  cvmlift2lem1  35689  cvmlift2lem9  35698  poimirlem32  38186  dfno2  44039  trclexi  44231  cnvtrcl0  44237  volicoff  46594  volicofmpt  46596  issmflem  47326