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

Theorem unssi 3438
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 441 . 2  |-  ( A 
C_  C  /\  B  C_  C )
4 unss 3437 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
53, 4mpbi 199 1  |-  ( A  u.  B )  C_  C
Colors of variables: wff set class
Syntax hints:    /\ wa 358    u. cun 3236    C_ wss 3238
This theorem is referenced by:  dmrnssfld  5041  tc2  7574  pwxpndom2  8434  ltrelxr  9033  nn0ssre  10118  nn0ssz  10195  dfle2  10633  difreicc  10920  hashxrcl  11527  ramxrcl  13272  strlemor1  13443  strleun  13446  cssincl  16805  leordtval2  17159  lecldbas  17166  aalioulem2  19928  taylfval  19953  konigsberg  21220  shunssji  22382  shsval3i  22401  shjshsi  22505  spanuni  22557  sshhococi  22559  esumcst  24041  hashf2  24060  sxbrsigalem3  24206  axlowdimlem10  25406  comppfsc  25899  hdmapevec  32087
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-un 3243  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator