Theorem xpss1 5161

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

Syntax hints:   → wi 4   ⊆ wss 3607   × cxp 5141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621  df-opab 4746  df-xp 5149

This theorem is referenced by:  ssres2  5460  funssxp  6099  tposssxp  7401  tpostpos2  7418  unxpwdom2  8534  dfac12lem2  9004  axdc3lem  9310  fpwwe2  9503  canthp1lem2  9513  pwfseqlem5  9523  wrdexg  13347  imasvscafn  16244  imasvscaf  16246  gasubg  17781  mamures  20244  mdetrlin  20456  mdetrsca  20457  mdetunilem9  20474  mdetmul  20477  tx1cn  21460  cxpcn3  24534  imadifxp  29540  1stmbfm  30450  sxbrsigalem0  30461  cvmlift2lem1  31410  cvmlift2lem9  31419  poimirlem32  33571  trclexi  38244  cnvtrcl0  38250  volicoff  40530  volicofmpt  40532  issmflem  41257