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

Theorem unss12 4187
Description: Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
Assertion
Ref Expression
unss12 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))

Proof of Theorem unss12
StepHypRef Expression
1 unss1 4184 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 unss2 4186 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3996 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  cun 3948  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-ss 3967
This theorem is referenced by:  pwssun  5574  fun  6769  f1un  6867  undomOLD  9101  finsschain  9400  trclun  15054  relexpfld  15089  mulgfval  19088  mvdco  19464  dprd2da  20063  dmdprdsplit2lem  20066  lspun  20986  mulsproplem13  28155  mulsproplem14  28156  spanuni  31564  sshhococi  31566  mthmpps  35588  pibt2  37419  mblfinlem3  37667  dochdmj1  41393  mptrcllem  43631  clcnvlem  43641  dfrcl2  43692  relexpss1d  43723  corclrcl  43725  relexp0a  43734  corcltrcl  43757  frege131d  43782
  Copyright terms: Public domain W3C validator