Theorem xpss1 5677

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   × cxp 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-opab 5174  df-xp 5664

This theorem is used by:  ssres2  6011  funssxp  6768  tposssxp  8285  tpostpos2  8302  unxpwdom2  9619  dfac12lem2  10262  unctb  10321  axdc3lem  10567  fpwwe2  10767  pwfseqlem5  10787  imasvscafn  17759  imasvscaf  17761  gasubg  19567  mamures  22767  mdetrlin  22972  mdetrsca  22973  mdetunilem9  22990  mdetmul  22993  tx1cn  23983  cxpcn3  27133  imadifxp  33293  1stmbfm  35003  sxbrsigalem0  35014  cvmlift2lem1  36275  cvmlift2lem9  36284  poimirlem32  38838  dfno2  44690  trclexi  44881  cnvtrcl0  44887  volicoff  47278  volicofmpt  47280  issmflem  48010