Theorem xpss1 5570

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

Syntax hints:   → wi 4   ⊆ wss 3866   × cxp 5549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-opab 5116  df-xp 5557

This theorem is referenced by:  ssres2  5879  funssxp  6574  tposssxp  7972  tpostpos2  7989  unxpwdom2  9204  dfac12lem2  9758  unctb  9819  axdc3lem  10064  fpwwe2  10257  pwfseqlem5  10277  imasvscafn  17042  imasvscaf  17044  gasubg  18696  mamures  21289  mdetrlin  21499  mdetrsca  21500  mdetunilem9  21517  mdetmul  21520  tx1cn  22506  cxpcn3  25634  imadifxp  30659  1stmbfm  31939  sxbrsigalem0  31950  cvmlift2lem1  32977  cvmlift2lem9  32986  poimirlem32  35546  trclexi  40904  cnvtrcl0  40910  volicoff  43211  volicofmpt  43213  issmflem  43935