Theorem unssi 4142

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

Step	Hyp	Ref	Expression
1		unssi.1	. . 3 ⊢ 𝐴 ⊆ 𝐶
2		unssi.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	1, 2	pm3.2i 470	. 2 ⊢ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)
4		unss 4141	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
5	3, 4	mpbi 230	1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶

Syntax hints:   ∧ wa 395   ∪ cun 3897   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  pwunss  4569  dmrnssfld  5920  tc2  9640  djuunxp  9824  pwxpndom2  10566  ltrelxr  11183  nn0ssre  12395  nn0sscn  12396  nn0ssz  12501  dfle2  13056  difreicc  13394  hashxrcl  14274  ramxrcl  16939  strleun  17078  cssincl  21635  leordtval2  23137  lecldbas  23144  comppfsc  23457  aalioulem2  26278  taylfval  26303  addsbdaylem  27969  addsbday  27970  addsdilem3  28102  addsdilem4  28103  mulsasslem3  28114  onscutlt  28211  axlowdimlem10  28940  shunssji  31360  shsval3i  31379  shjshsi  31483  spanuni  31535  sshhococi  31537  esumcst  34087  hashf2  34108  sxbrsigalem3  34296  signswch  34585  tz9.1regs  35141  bj-unrab  36981  bj-tagss  37035  bj-imdirco  37245  poimirlem16  37686  poimirlem19  37689  poimirlem23  37693  poimirlem29  37699  poimirlem31  37701  poimirlem32  37702  mblfinlem3  37709  mblfinlem4  37710  hdmapevec  41944  rtrclex  43724  trclexi  43727  rtrclexi  43728  cnvrcl0  43732  cnvtrcl0  43733  comptiunov2i  43813  cotrclrcl  43849  cncfiooicclem1  46005  fourierdlem62  46280