Theorem xpss1 5630

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

Syntax hints:   → wi 4   ⊆ wss 3897   × cxp 5609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-opab 5149  df-xp 5617

This theorem is referenced by:  ssres2  5948  funssxp  6674  tposssxp  8155  tpostpos2  8172  unxpwdom2  9469  dfac12lem2  10031  unctb  10090  axdc3lem  10336  fpwwe2  10529  pwfseqlem5  10549  imasvscafn  17436  imasvscaf  17438  gasubg  19209  mamures  22307  mdetrlin  22512  mdetrsca  22513  mdetunilem9  22530  mdetmul  22533  tx1cn  23519  cxpcn3  26680  imadifxp  32573  1stmbfm  34265  sxbrsigalem0  34276  cvmlift2lem1  35338  cvmlift2lem9  35347  poimirlem32  37692  dfno2  43461  trclexi  43653  cnvtrcl0  43659  volicoff  46033  volicofmpt  46035  issmflem  46765