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

Theorem xpss1 5218
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 3616 . 2 𝐶𝐶
2 xpss12 5215 . 2 ((𝐴𝐵𝐶𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
31, 2mpan2 706 1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3567   × cxp 5102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-in 3574  df-ss 3581  df-opab 4704  df-xp 5110
This theorem is referenced by:  ssres2  5413  funssxp  6048  tposssxp  7341  tpostpos2  7358  unxpwdom2  8478  dfac12lem2  8951  axdc3lem  9257  fpwwe2  9450  canthp1lem2  9460  pwfseqlem5  9470  wrdexg  13298  imasvscafn  16178  imasvscaf  16180  gasubg  17716  mamures  20177  mdetrlin  20389  mdetrsca  20390  mdetunilem9  20407  mdetmul  20410  tx1cn  21393  cxpcn3  24470  imadifxp  29386  1stmbfm  30296  sxbrsigalem0  30307  cvmlift2lem1  31258  cvmlift2lem9  31267  poimirlem32  33412  trclexi  37746  cnvtrcl0  37752  volicoff  39975  volicofmpt  39977  issmflem  40699
  Copyright terms: Public domain W3C validator