Theorem unssi 4115

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 4114	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
5	3, 4	mpbi 229	1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶

Syntax hints:   ∧ wa 395   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  pwunss  4550  dmrnssfld  5868  tc2  9431  djuunxp  9610  pwxpndom2  10352  ltrelxr  10967  nn0ssre  12167  nn0sscn  12168  nn0ssz  12271  dfle2  12810  difreicc  13145  hashxrcl  14000  ramxrcl  16646  strleun  16786  cssincl  20805  leordtval2  22271  lecldbas  22278  comppfsc  22591  aalioulem2  25398  taylfval  25423  axlowdimlem10  27222  shunssji  29632  shsval3i  29651  shjshsi  29755  spanuni  29807  sshhococi  29809  esumcst  31931  hashf2  31952  sxbrsigalem3  32139  signswch  32440  bj-unrab  35041  bj-tagss  35097  bj-imdirco  35288  poimirlem16  35720  poimirlem19  35723  poimirlem23  35727  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  mblfinlem3  35743  mblfinlem4  35744  hdmapevec  39776  rtrclex  41114  trclexi  41117  rtrclexi  41118  cnvrcl0  41122  cnvtrcl0  41123  comptiunov2i  41203  cotrclrcl  41239  cncfiooicclem1  43324  fourierdlem62  43599