Theorem xpss1 5643

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

Syntax hints:   → wi 4   ⊆ wss 3901   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-opab 5161  df-xp 5630

This theorem is referenced by:  ssres2  5963  funssxp  6690  tposssxp  8172  tpostpos2  8189  unxpwdom2  9493  dfac12lem2  10055  unctb  10114  axdc3lem  10360  fpwwe2  10554  pwfseqlem5  10574  imasvscafn  17458  imasvscaf  17460  gasubg  19231  mamures  22341  mdetrlin  22546  mdetrsca  22547  mdetunilem9  22564  mdetmul  22567  tx1cn  23553  cxpcn3  26714  imadifxp  32676  1stmbfm  34417  sxbrsigalem0  34428  cvmlift2lem1  35496  cvmlift2lem9  35505  poimirlem32  37853  dfno2  43669  trclexi  43861  cnvtrcl0  43867  volicoff  46239  volicofmpt  46241  issmflem  46971