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

Theorem unss1 3503
Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
unss1  |-  ( A 
C_  B  ->  ( A  u.  C )  C_  ( B  u.  C
) )

Proof of Theorem unss1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ssel 3329 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21orim1d 813 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  \/  x  e.  C
)  ->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3475 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3475 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43imtr4g 262 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A  u.  C )  ->  x  e.  ( B  u.  C ) ) )
65ssrdv 3341 1  |-  ( A 
C_  B  ->  ( A  u.  C )  C_  ( B  u.  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    e. wcel 1725    u. cun 3305    C_ wss 3307
This theorem is referenced by:  unss2  3505  unss12  3506  eldifpw  4741  tposss  6466  dftpos4  6484  hashbclem  11684  incexclem  12599  mreexexlem2d  13853  catcoppccl  14246  neitr  17227  restntr  17229  leordtval2  17259  cmpcld  17448  uniioombllem3  19460  limcres  19756  plyss  20101  shlej1  22845  orderseqlem  25502  pclfinclN  30478
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-un 3312  df-in 3314  df-ss 3321
  Copyright terms: Public domain W3C validator