Theorem xpss1 5650

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

Syntax hints:   → wi 4   ⊆ wss 3889   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-opab 5148  df-xp 5637

This theorem is referenced by:  ssres2  5969  funssxp  6696  tposssxp  8180  tpostpos2  8197  unxpwdom2  9503  dfac12lem2  10067  unctb  10126  axdc3lem  10372  fpwwe2  10566  pwfseqlem5  10586  imasvscafn  17501  imasvscaf  17503  gasubg  19277  mamures  22362  mdetrlin  22567  mdetrsca  22568  mdetunilem9  22585  mdetmul  22588  tx1cn  23574  cxpcn3  26712  imadifxp  32671  1stmbfm  34404  sxbrsigalem0  34415  cvmlift2lem1  35484  cvmlift2lem9  35493  poimirlem32  37973  dfno2  43855  trclexi  44047  cnvtrcl0  44053  volicoff  46423  volicofmpt  46425  issmflem  47155