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

Theorem unssi 3998
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 458 . 2 (𝐴𝐶𝐵𝐶)
4 unss 3997 . 2 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
53, 4mpbi 221 1 (𝐴𝐵) ⊆ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wa 384  cun 3778  wss 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-un 3785  df-in 3787  df-ss 3794
This theorem is referenced by:  dmrnssfld  5599  tc2  8875  djuunxp  9040  pwxpndom2  9782  ltrelxr  10394  nn0ssre  11583  nn0ssz  11684  dfle2  12216  difreicc  12547  hashxrcl  13386  ramxrcl  15958  strlemor1OLD  16200  strleun  16203  cssincl  20263  leordtval2  21251  lecldbas  21258  comppfsc  21570  aalioulem2  24325  taylfval  24350  axlowdimlem10  26068  shunssji  28579  shsval3i  28598  shjshsi  28702  spanuni  28754  sshhococi  28756  esumcst  30473  hashf2  30494  sxbrsigalem3  30682  signswch  30986  bj-unrab  33252  bj-tagss  33297  poimirlem16  33757  poimirlem19  33760  poimirlem23  33764  poimirlem29  33770  poimirlem31  33772  poimirlem32  33773  mblfinlem3  33780  mblfinlem4  33781  hdmapevec  37634  rtrclex  38442  trclexi  38445  rtrclexi  38446  cnvrcl0  38450  cnvtrcl0  38451  comptiunov2i  38516  cotrclrcl  38552  cncfiooicclem1  40604  fourierdlem62  40882
  Copyright terms: Public domain W3C validator