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

Theorem unss12 4198
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 4195 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 unss2 4197 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 4009 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  cun 3961  wss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980
This theorem is referenced by:  pwssun  5580  fun  6771  f1un  6869  undomOLD  9099  finsschain  9397  trclun  15050  relexpfld  15085  mulgfval  19100  mvdco  19478  dprd2da  20077  dmdprdsplit2lem  20080  lspun  21003  mulsproplem13  28169  mulsproplem14  28170  spanuni  31573  sshhococi  31575  mthmpps  35567  pibt2  37400  mblfinlem3  37646  dochdmj1  41373  mptrcllem  43603  clcnvlem  43613  dfrcl2  43664  relexpss1d  43695  corclrcl  43697  relexp0a  43706  corcltrcl  43729  frege131d  43754
  Copyright terms: Public domain W3C validator