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

Theorem unss1 3636
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 3461 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21orim1d 835 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  \/  x  e.  C
)  ->  ( x  e.  B  \/  x  e.  C ) ) )
3 elun 3608 . . 3  |-  ( x  e.  ( A  u.  C )  <->  ( x  e.  A  \/  x  e.  C ) )
4 elun 3608 . . 3  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
52, 3, 43imtr4g 270 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A  u.  C )  ->  x  e.  ( B  u.  C ) ) )
65ssrdv 3473 1  |-  ( A 
C_  B  ->  ( A  u.  C )  C_  ( B  u.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    e. wcel 1758    u. cun 3437    C_ wss 3439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444  df-in 3446  df-ss 3453
This theorem is referenced by:  unss2  3638  unss12  3639  eldifpw  6501  tposss  6859  dftpos4  6877  hashbclem  12326  incexclem  13420  mreexexlem2d  14705  catcoppccl  15098  neitr  18919  restntr  18921  leordtval2  18951  cmpcld  19140  uniioombllem3  21201  limcres  21497  plyss  21803  shlej1  24935  orderseqlem  27877  bj-rrhatsscchat  32917  pclfinclN  33952
  Copyright terms: Public domain W3C validator