Theorem xpss1 5577

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

Syntax hints:   → wi 4   ⊆ wss 3939   × cxp 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-in 3946  df-ss 3955  df-opab 5132  df-xp 5564

This theorem is referenced by:  ssres2  5884  funssxp  6538  tposssxp  7899  tpostpos2  7916  unxpwdom2  9055  dfac12lem2  9573  unctb  9630  axdc3lem  9875  fpwwe2  10068  pwfseqlem5  10088  wrdexgOLD  13875  imasvscafn  16813  imasvscaf  16815  gasubg  18435  mamures  21004  mdetrlin  21214  mdetrsca  21215  mdetunilem9  21232  mdetmul  21235  tx1cn  22220  cxpcn3  25332  imadifxp  30354  1stmbfm  31522  sxbrsigalem0  31533  cvmlift2lem1  32553  cvmlift2lem9  32562  poimirlem32  34928  trclexi  39986  cnvtrcl0  39992  volicoff  42287  volicofmpt  42289  issmflem  43011