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

Theorem unssi 4147
 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 474 . 2 (𝐴𝐶𝐵𝐶)
4 unss 4146 . 2 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
53, 4mpbi 233 1 (𝐴𝐵) ⊆ 𝐶
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   ∪ cun 3917   ⊆ wss 3919 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936 This theorem is referenced by:  pwunss  4542  dmrnssfld  5830  tc2  9183  djuunxp  9349  pwxpndom2  10087  ltrelxr  10702  nn0ssre  11900  nn0sscn  11901  nn0ssz  12002  dfle2  12539  difreicc  12873  hashxrcl  13725  ramxrcl  16353  strleun  16593  cssincl  20386  leordtval2  21826  lecldbas  21833  comppfsc  22146  aalioulem2  24938  taylfval  24963  axlowdimlem10  26754  shunssji  29161  shsval3i  29180  shjshsi  29284  spanuni  29336  sshhococi  29338  esumcst  31407  hashf2  31428  sxbrsigalem3  31615  signswch  31916  bj-unrab  34340  bj-tagss  34388  bj-imdirco  34577  poimirlem16  35045  poimirlem19  35048  poimirlem23  35052  poimirlem29  35058  poimirlem31  35060  poimirlem32  35061  mblfinlem3  35068  mblfinlem4  35069  hdmapevec  39103  rtrclex  40261  trclexi  40264  rtrclexi  40265  cnvrcl0  40269  cnvtrcl0  40270  comptiunov2i  40351  cotrclrcl  40387  cncfiooicclem1  42488  fourierdlem62  42763
 Copyright terms: Public domain W3C validator