Theorem xpss1 5678

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

Syntax hints:   → wi 4   ⊆ wss 3931   × cxp 5657

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ss 3948  df-opab 5187  df-xp 5665

This theorem is referenced by:  ssres2  5996  funssxp  6739  tposssxp  8234  tpostpos2  8251  unxpwdom2  9607  dfac12lem2  10164  unctb  10223  axdc3lem  10469  fpwwe2  10662  pwfseqlem5  10682  imasvscafn  17556  imasvscaf  17558  gasubg  19290  mamures  22340  mdetrlin  22545  mdetrsca  22546  mdetunilem9  22563  mdetmul  22566  tx1cn  23552  cxpcn3  26715  imadifxp  32587  1stmbfm  34297  sxbrsigalem0  34308  cvmlift2lem1  35329  cvmlift2lem9  35338  poimirlem32  37681  dfno2  43419  trclexi  43611  cnvtrcl0  43617  volicoff  45991  volicofmpt  45993  issmflem  46723