Theorem xpss1 5683

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908   × cxp 5662

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-opab 5177  df-xp 5670

This theorem is used by:  ssres2  6006  funssxp  6738  tposssxp  8228  tpostpos2  8245  unxpwdom2  9552  dfac12lem2  10139  unctb  10198  axdc3lem  10444  fpwwe2  10638  pwfseqlem5  10658  imasvscafn  17601  imasvscaf  17603  gasubg  19382  mamures  22569  mdetrlin  22774  mdetrsca  22775  mdetunilem9  22792  mdetmul  22795  tx1cn  23781  cxpcn3  26928  imadifxp  32961  1stmbfm  34663  sxbrsigalem0  34674  cvmlift2lem1  35806  cvmlift2lem9  35815  poimirlem32  38335  dfno2  44186  trclexi  44378  cnvtrcl0  44384  volicoff  46741  volicofmpt  46743  issmflem  47473