Theorem xpss1 5696

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

Syntax hints:   → wi 4   ⊆ wss 3949   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683

This theorem is referenced by:  ssres2  6010  funssxp  6747  tposssxp  8215  tpostpos2  8232  unxpwdom2  9583  dfac12lem2  10139  unctb  10200  axdc3lem  10445  fpwwe2  10638  pwfseqlem5  10658  imasvscafn  17483  imasvscaf  17485  gasubg  19166  mamures  21892  mdetrlin  22104  mdetrsca  22105  mdetunilem9  22122  mdetmul  22125  tx1cn  23113  cxpcn3  26256  imadifxp  31832  1stmbfm  33259  sxbrsigalem0  33270  cvmlift2lem1  34293  cvmlift2lem9  34302  poimirlem32  36520  dfno2  42179  trclexi  42371  cnvtrcl0  42377  volicoff  44711  volicofmpt  44713  issmflem  45443