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

Theorem unssi 3932
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 470 . 2 (𝐴𝐶𝐵𝐶)
4 unss 3931 . 2 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
53, 4mpbi 220 1 (𝐴𝐵) ⊆ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wa 383  cun 3714  wss 3716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730
This theorem is referenced by:  dmrnssfld  5540  tc2  8794  pwxpndom2  9700  ltrelxr  10312  nn0ssre  11509  nn0ssz  11611  dfle2  12194  difreicc  12518  hashxrcl  13361  ramxrcl  15944  strlemor1OLD  16192  strleun  16195  cssincl  20255  leordtval2  21239  lecldbas  21246  comppfsc  21558  aalioulem2  24308  taylfval  24333  axlowdimlem10  26052  shunssji  28559  shsval3i  28578  shjshsi  28682  spanuni  28734  sshhococi  28736  esumcst  30456  hashf2  30477  sxbrsigalem3  30665  signswch  30969  bj-unrab  33248  bj-tagss  33293  poimirlem16  33757  poimirlem19  33760  poimirlem23  33764  poimirlem29  33770  poimirlem31  33772  poimirlem32  33773  mblfinlem3  33780  mblfinlem4  33781  hdmapevec  37648  rtrclex  38445  trclexi  38448  rtrclexi  38449  cnvrcl0  38453  cnvtrcl0  38454  comptiunov2i  38519  cotrclrcl  38555  cncfiooicclem1  40628  fourierdlem62  40907
  Copyright terms: Public domain W3C validator