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

Theorem unssi 3536
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 455 . 2  |-  ( A 
C_  C  /\  B  C_  C )
4 unss 3535 . 2  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
53, 4mpbi 208 1  |-  ( A  u.  B )  C_  C
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    u. cun 3331    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338  df-in 3340  df-ss 3347
This theorem is referenced by:  dmrnssfld  5103  tc2  7967  pwxpndom2  8837  ltrelxr  9443  nn0ssre  10588  nn0ssz  10672  dfle2  11129  difreicc  11422  hashxrcl  12132  ramxrcl  14083  strlemor1  14270  strleun  14273  cssincl  18118  leordtval2  18821  lecldbas  18828  aalioulem2  21804  taylfval  21829  axlowdimlem10  23202  konigsberg  23613  shunssji  24777  shsval3i  24796  shjshsi  24900  spanuni  24952  sshhococi  24954  esumcst  26519  hashf2  26538  sxbrsigalem3  26692  signswch  26967  mblfinlem3  28435  mblfinlem4  28436  comppfsc  28584  bj-unrab  32434  bj-tagss  32478  hdmapevec  35488
  Copyright terms: Public domain W3C validator