Theorem unssi 4138

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914

This theorem is referenced by:  pwunss  4565  dmrnssfld  5912  tc2  9630  djuunxp  9814  pwxpndom2  10556  ltrelxr  11173  nn0ssre  12385  nn0sscn  12386  nn0ssz  12491  dfle2  13046  difreicc  13384  hashxrcl  14264  ramxrcl  16929  strleun  17068  cssincl  21625  leordtval2  23127  lecldbas  23134  comppfsc  23447  aalioulem2  26268  taylfval  26293  addsbdaylem  27959  addsbday  27960  addsdilem3  28092  addsdilem4  28093  mulsasslem3  28104  onscutlt  28201  axlowdimlem10  28929  shunssji  31349  shsval3i  31368  shjshsi  31472  spanuni  31524  sshhococi  31526  esumcst  34076  hashf2  34097  sxbrsigalem3  34285  signswch  34574  tz9.1regs  35130  bj-unrab  36970  bj-tagss  37024  bj-imdirco  37234  poimirlem16  37686  poimirlem19  37689  poimirlem23  37693  poimirlem29  37699  poimirlem31  37701  poimirlem32  37702  mblfinlem3  37709  mblfinlem4  37710  hdmapevec  41944  rtrclex  43720  trclexi  43723  rtrclexi  43724  cnvrcl0  43728  cnvtrcl0  43729  comptiunov2i  43809  cotrclrcl  43845  cncfiooicclem1  46001  fourierdlem62  46276