Theorem xpss1 5151

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

Syntax hints:   → wi 4   ⊆ wss 3540   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044

This theorem is referenced by:  ssres2  5345  funssxp  5974  tposssxp  7243  tpostpos2  7260  unxpwdom2  8376  dfac12lem2  8849  axdc3lem  9155  fpwwe2  9344  canthp1lem2  9354  pwfseqlem5  9364  wrdexg  13170  imasvscafn  16020  imasvscaf  16022  gasubg  17558  mamures  20015  mdetrlin  20227  mdetrsca  20228  mdetunilem9  20245  mdetmul  20248  tx1cn  21222  cxpcn3  24289  imadifxp  28796  1stmbfm  29649  sxbrsigalem0  29660  cvmlift2lem1  30538  cvmlift2lem9  30547  poimirlem32  32611  trclexi  36946  cnvtrcl0  36952  volicoff  38888  volicofmpt  38890  issmflem  39613