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

Theorem xpss1 5135
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 3581 . 2 𝐶𝐶
2 xpss12 5132 . 2 ((𝐴𝐵𝐶𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
31, 2mpan2 702 1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3534   × cxp 5021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-in 3541  df-ss 3548  df-opab 4633  df-xp 5029
This theorem is referenced by:  ssres2  5327  funssxp  5955  tposssxp  7215  tpostpos2  7232  unxpwdom2  8348  dfac12lem2  8821  axdc3lem  9127  fpwwe2  9316  canthp1lem2  9326  pwfseqlem5  9336  wrdexg  13111  imasvscafn  15961  imasvscaf  15963  gasubg  17499  mamures  19952  mdetrlin  20164  mdetrsca  20165  mdetunilem9  20182  mdetmul  20185  tx1cn  21159  cxpcn3  24201  imadifxp  28597  1stmbfm  29450  sxbrsigalem0  29461  cvmlift2lem1  30339  cvmlift2lem9  30348  poimirlem32  32409  trclexi  36744  cnvtrcl0  36750  volicoff  38687  volicofmpt  38689  issmflem  39412
  Copyright terms: Public domain W3C validator