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

Theorem unss12 3742
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 3739 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 unss2 3741 . 2 (𝐶𝐷 → (𝐵𝐶) ⊆ (𝐵𝐷))
31, 2sylan9ss 3576 1 ((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ⊆ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  cun 3533  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-un 3540  df-in 3542  df-ss 3549
This theorem is referenced by:  pwssun  4930  fun  5961  undom  7906  finsschain  8129  trclun  13545  relexpfld  13579  mvdco  17630  dprd2da  18206  dmdprdsplit2lem  18209  lspun  18750  spanuni  27589  sshhococi  27591  mthmpps  30535  mblfinlem3  32417  dochdmj1  35496  mptrcllem  36738  clcnvlem  36748  dfrcl2  36784  relexpss1d  36815  corclrcl  36817  relexp0a  36826  corcltrcl  36849  frege131d  36874
  Copyright terms: Public domain W3C validator