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

Theorem unssi 3350
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 3349 . 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 3150    C_ wss 3152
This theorem is referenced by:  dmrnssfld  4938  tc2  7427  pwxpndom2  8287  ltrelxr  8886  nn0ssre  9969  nn0ssz  10044  dfle2  10481  difreicc  10767  hashxrcl  11351  ramxrcl  13064  strlemor1  13235  strleun  13238  cssincl  16588  leordtval2  16942  lecldbas  16949  aalioulem2  19713  taylfval  19738  shunssji  21948  shsval3i  21967  shjshsi  22071  spanuni  22123  sshhococi  22125  esumcst  23436  hashf2  23452  konigsberg  23911  axlowdimlem10  24579  smbkle  26043  comppfsc  26307  hdmapevec  32028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator