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

Theorem unssi 3482
Description: An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
unssi.1  |-  A  C_  C
unssi.2  |-  B  C_  C
Assertion
Ref Expression
unssi  |-  ( A  u.  B )  C_  C

Proof of Theorem unssi
StepHypRef Expression
1 unssi.1 . . 3  |-  A  C_  C
2 unssi.2 . . 3  |-  B  C_  C
31, 2pm3.2i 442 . 2  |-  ( A 
C_  C  /\  B  C_  C )
4 unss 3481 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
53, 4mpbi 200 1  |-  ( A  u.  B )  C_  C
Colors of variables: wff set class
Syntax hints:    /\ wa 359    u. cun 3278    C_ wss 3280
This theorem is referenced by:  dmrnssfld  5088  tc2  7637  pwxpndom2  8496  ltrelxr  9095  nn0ssre  10181  nn0ssz  10258  dfle2  10696  difreicc  10984  hashxrcl  11595  ramxrcl  13340  strlemor1  13511  strleun  13514  cssincl  16870  leordtval2  17230  lecldbas  17237  aalioulem2  20203  taylfval  20228  konigsberg  21662  shunssji  22824  shsval3i  22843  shjshsi  22947  spanuni  22999  sshhococi  23001  esumcst  24408  hashf2  24427  sxbrsigalem3  24575  axlowdimlem10  25794  mblfinlem2  26144  mblfinlem3  26145  comppfsc  26277  hdmapevec  32321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator