Theorem xpss1 5331

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

Syntax hints:   → wi 4   ⊆ wss 3769   × cxp 5310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-in 3776  df-ss 3783  df-opab 4906  df-xp 5318

This theorem is referenced by:  ssres2  5635  funssxp  6276  tposssxp  7594  tpostpos2  7611  unxpwdom2  8735  dfac12lem2  9254  axdc3lem  9560  fpwwe2  9753  canthp1lem2  9763  pwfseqlem5  9773  wrdexg  13544  imasvscafn  16512  imasvscaf  16514  gasubg  18047  mamures  20521  mdetrlin  20734  mdetrsca  20735  mdetunilem9  20752  mdetmul  20755  tx1cn  21741  cxpcn3  24833  imadifxp  29931  1stmbfm  30838  sxbrsigalem0  30849  cvmlift2lem1  31801  cvmlift2lem9  31810  poimirlem32  33930  trclexi  38710  cnvtrcl0  38716  volicoff  40955  volicofmpt  40957  issmflem  41682