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

Theorem unss1 3594
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 3412 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21orim1d 857 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  \/  x  e.  C
)  ->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3565 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3565 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43imtr4g 278 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A  u.  C )  ->  x  e.  ( B  u.  C ) ) )
65ssrdv 3424 1  |-  ( A 
C_  B  ->  ( A  u.  C )  C_  ( B  u.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 375    e. wcel 1904    u. cun 3388    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-in 3397  df-ss 3404
This theorem is referenced by:  unss2  3596  unss12  3597  eldifpw  6622  tposss  6992  dftpos4  7010  hashbclem  12656  incexclem  13971  mreexexlem2d  15629  catcoppccl  16081  neitr  20273  restntr  20275  leordtval2  20305  cmpcld  20494  uniioombllem3  22622  limcres  22920  plyss  23232  shlej1  27094  ss2mcls  30278  orderseqlem  30561  bj-rrhatsscchat  31748  pclfinclN  33586
  Copyright terms: Public domain W3C validator