Theorem xpss1 5670

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   × cxp 5649

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-opab 5168  df-xp 5657

This theorem is used by:  ssres2  5995  funssxp  6736  tposssxp  8240  tpostpos2  8257  unxpwdom2  9575  dfac12lem2  10216  unctb  10275  axdc3lem  10521  fpwwe2  10721  pwfseqlem5  10741  imasvscafn  17702  imasvscaf  17704  gasubg  19509  mamures  22705  mdetrlin  22910  mdetrsca  22911  mdetunilem9  22928  mdetmul  22931  tx1cn  23921  cxpcn3  27069  imadifxp  33188  1stmbfm  34885  sxbrsigalem0  34896  cvmlift2lem1  36046  cvmlift2lem9  36055  poimirlem32  38550  dfno2  44413  trclexi  44605  cnvtrcl0  44611  volicoff  46974  volicofmpt  46976  issmflem  47706