MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpss1 Structured version   Visualization version   GIF version

Theorem xpss1 5650
Description: Subset relation for Cartesian product. (Contributed by Jeff Hankins, 30-Aug-2009.)
Assertion
Ref Expression
xpss1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))

Proof of Theorem xpss1
StepHypRef Expression
1 ssid 3964 . 2 𝐶𝐶
2 xpss12 5646 . 2 ((𝐴𝐵𝐶𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
31, 2mpan2 689 1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3908   × 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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-ss 3925  df-opab 5166  df-xp 5637
This theorem is referenced by:  ssres2  5963  funssxp  6694  tposssxp  8153  tpostpos2  8170  unxpwdom2  9482  dfac12lem2  10038  unctb  10099  axdc3lem  10344  fpwwe2  10537  pwfseqlem5  10557  imasvscafn  17379  imasvscaf  17381  gasubg  19041  mamures  21691  mdetrlin  21903  mdetrsca  21904  mdetunilem9  21921  mdetmul  21924  tx1cn  22912  cxpcn3  26053  imadifxp  31348  1stmbfm  32672  sxbrsigalem0  32683  cvmlift2lem1  33708  cvmlift2lem9  33717  poimirlem32  36048  dfno2  41611  trclexi  41803  cnvtrcl0  41809  volicoff  44137  volicofmpt  44139  issmflem  44869
  Copyright terms: Public domain W3C validator