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

Theorem unssi 4158
Description: An inference showing the union of two subclasses is a subclass. (Contributed by Raph Levien, 10-Dec-2002.)
Hypotheses
Ref Expression
unssi.1 𝐴𝐶
unssi.2 𝐵𝐶
Assertion
Ref Expression
unssi (𝐴𝐵) ⊆ 𝐶

Proof of Theorem unssi
StepHypRef Expression
1 unssi.1 . . 3 𝐴𝐶
2 unssi.2 . . 3 𝐵𝐶
31, 2pm3.2i 471 . 2 (𝐴𝐶𝐵𝐶)
4 unss 4157 . 2 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
53, 4mpbi 231 1 (𝐴𝐵) ⊆ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wa 396  cun 3931  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949
This theorem is referenced by:  pwunss  5446  dmrnssfld  5834  tc2  9172  djuunxp  9338  pwxpndom2  10075  ltrelxr  10690  nn0ssre  11889  nn0sscn  11890  nn0ssz  11991  dfle2  12528  difreicc  12858  hashxrcl  13706  ramxrcl  16341  strleun  16579  cssincl  20760  leordtval2  21748  lecldbas  21755  comppfsc  22068  aalioulem2  24849  taylfval  24874  axlowdimlem10  26664  shunssji  29073  shsval3i  29092  shjshsi  29196  spanuni  29248  sshhococi  29250  esumcst  31221  hashf2  31242  sxbrsigalem3  31429  signswch  31730  bj-unrab  34141  bj-tagss  34189  poimirlem16  34789  poimirlem19  34792  poimirlem23  34796  poimirlem29  34802  poimirlem31  34804  poimirlem32  34805  mblfinlem3  34812  mblfinlem4  34813  hdmapevec  38851  rtrclex  39855  trclexi  39858  rtrclexi  39859  cnvrcl0  39863  cnvtrcl0  39864  comptiunov2i  39929  cotrclrcl  39965  cncfiooicclem1  42052  fourierdlem62  42330
  Copyright terms: Public domain W3C validator