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

Theorem unss12 3606
Description: Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.)
Assertion
Ref Expression
unss12  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  u.  C
)  C_  ( B  u.  D ) )

Proof of Theorem unss12
StepHypRef Expression
1 unss1 3603 . 2  |-  ( A 
C_  B  ->  ( A  u.  C )  C_  ( B  u.  C
) )
2 unss2 3605 . 2  |-  ( C 
C_  D  ->  ( B  u.  C )  C_  ( B  u.  D
) )
31, 2sylan9ss 3445 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  u.  C
)  C_  ( B  u.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    u. cun 3402    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409  df-in 3411  df-ss 3418
This theorem is referenced by:  pwssun  4740  fun  5746  undom  7660  finsschain  7881  trclun  13078  relexpfld  13112  mvdco  17086  dprd2da  17675  dmdprdsplit2lem  17678  lspun  18210  spanuni  27197  sshhococi  27199  mthmpps  30220  mblfinlem3  31979  dochdmj1  34958  mptrcllem  36220  clcnvlem  36230  dfrcl2  36266  relexpss1d  36297  corclrcl  36299  relexp0a  36308  corcltrcl  36331  frege131d  36356
  Copyright terms: Public domain W3C validator