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

Theorem unssi 3647
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 456 . 2  |-  ( A 
C_  C  /\  B  C_  C )
4 unss 3646 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
53, 4mpbi 211 1  |-  ( A  u.  B )  C_  C
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    u. cun 3440    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-in 3449  df-ss 3456
This theorem is referenced by:  dmrnssfld  5113  tc2  8225  pwxpndom2  9089  ltrelxr  9694  nn0ssre  10873  nn0ssz  10958  dfle2  11446  difreicc  11762  hashxrcl  12536  ramxrcl  14938  strlemor1  15179  strleun  15182  cssincl  19182  leordtval2  20159  lecldbas  20166  comppfsc  20478  aalioulem2  23154  taylfval  23179  axlowdimlem10  24827  konigsberg  25560  shunssji  26857  shsval3i  26876  shjshsi  26980  spanuni  27032  sshhococi  27034  esumcst  28723  hashf2  28744  sxbrsigalem3  28933  signswch  29238  bj-unrab  31279  bj-tagss  31323  poimirlem16  31660  poimirlem19  31663  poimirlem23  31667  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  mblfinlem3  31683  mblfinlem4  31684  hdmapevec  35115  comptiunov2i  35937  cotrclrcl  35973  cncfiooicclem1  37343  fourierdlem62  37600
  Copyright terms: Public domain W3C validator