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

Theorem unss12 4140
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 4137 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 unss2 4139 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3955 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  cun 3906  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-un 3913  df-in 3915  df-ss 3925
This theorem is referenced by:  pwssun  5526  fun  6701  f1un  6801  undomOLD  8962  finsschain  9261  trclun  14853  relexpfld  14888  mulgfval  18827  mvdco  19180  dprd2da  19774  dmdprdsplit2lem  19777  lspun  20395  spanuni  30331  sshhococi  30333  mthmpps  34004  pibt2  35820  mblfinlem3  36049  dochdmj1  39785  mptrcllem  41790  clcnvlem  41800  dfrcl2  41851  relexpss1d  41882  corclrcl  41884  relexp0a  41893  corcltrcl  41916  frege131d  41941
  Copyright terms: Public domain W3C validator