Theorem unssi 4131

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

Syntax hints:   ∧ wa 395   ∪ cun 3887   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  pwunss  4559  dmrnssfld  5929  tc2  9661  djuunxp  9845  pwxpndom2  10588  ltrelxr  11206  nn0ssre  12441  nn0sscn  12442  nn0ssz  12547  dfle2  13098  difreicc  13437  hashxrcl  14319  ramxrcl  16988  strleun  17127  cssincl  21668  leordtval2  23177  lecldbas  23184  comppfsc  23497  aalioulem2  26299  taylfval  26324  addbdaylem  28009  addbday  28010  addsdilem3  28145  addsdilem4  28146  mulsasslem3  28157  oncutlt  28256  axlowdimlem10  29020  shunssji  31440  shsval3i  31459  shjshsi  31563  spanuni  31615  sshhococi  31617  esumcst  34207  hashf2  34228  sxbrsigalem3  34416  signswch  34705  tz9.1regs  35278  ttcuniun  36692  ttciunun  36693  ttcuni  36695  bj-unrab  37233  bj-tagss  37287  bj-imdirco  37504  poimirlem16  37957  poimirlem19  37960  poimirlem23  37964  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  mblfinlem3  37980  mblfinlem4  37981  hdmapevec  42281  rtrclex  44044  trclexi  44047  rtrclexi  44048  cnvrcl0  44052  cnvtrcl0  44053  comptiunov2i  44133  cotrclrcl  44169  cncfiooicclem1  46321  fourierdlem62  46596