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

Theorem unss12 4112
 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 4109 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 unss2 4111 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3931 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3882   ⊆ wss 3884 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901 This theorem is referenced by:  pwssun  5424  fun  6518  undom  8592  finsschain  8819  trclun  14369  relexpfld  14403  mulgfval  18221  mvdco  18568  dprd2da  19160  dmdprdsplit2lem  19163  lspun  19755  spanuni  29330  sshhococi  29332  mthmpps  32937  pibt2  34829  mblfinlem3  35089  dochdmj1  38679  mptrcllem  40300  clcnvlem  40310  dfrcl2  40362  relexpss1d  40393  corclrcl  40395  relexp0a  40404  corcltrcl  40427  frege131d  40452
 Copyright terms: Public domain W3C validator