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

Theorem xpss1 5151
 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 3587 . 2 𝐶𝐶
2 xpss12 5148 . 2 ((𝐴𝐵𝐶𝐶) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
31, 2mpan2 703 1 (𝐴𝐵 → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐶))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator