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

Theorem xpss1 5573
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 3993 . 2 𝐶𝐶
2 xpss12 5569 . 2 ((𝐴𝐵𝐶𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
31, 2mpan2 687 1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3940   × cxp 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-in 3947  df-ss 3956  df-opab 5126  df-xp 5560
This theorem is referenced by:  ssres2  5880  funssxp  6532  tposssxp  7887  tpostpos2  7904  unxpwdom2  9041  dfac12lem2  9559  unctb  9616  axdc3lem  9861  fpwwe2  10054  pwfseqlem5  10074  wrdexgOLD  13862  imasvscafn  16800  imasvscaf  16802  gasubg  18362  mamures  20917  mdetrlin  21127  mdetrsca  21128  mdetunilem9  21145  mdetmul  21148  tx1cn  22133  cxpcn3  25242  imadifxp  30266  1stmbfm  31404  sxbrsigalem0  31415  cvmlift2lem1  32433  cvmlift2lem9  32442  poimirlem32  34791  trclexi  39845  cnvtrcl0  39851  volicoff  42146  volicofmpt  42148  issmflem  42870
  Copyright terms: Public domain W3C validator