Theorem unssi 4145

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

Syntax hints:   ∧ wa 395   ∪ cun 3901   ⊆ wss 3903

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  pwunss  4574  dmrnssfld  5931  tc2  9661  djuunxp  9845  pwxpndom2  10588  ltrelxr  11205  nn0ssre  12417  nn0sscn  12418  nn0ssz  12523  dfle2  13073  difreicc  13412  hashxrcl  14292  ramxrcl  16957  strleun  17096  cssincl  21655  leordtval2  23168  lecldbas  23175  comppfsc  23488  aalioulem2  26309  taylfval  26334  addbdaylem  28025  addbday  28026  addsdilem3  28161  addsdilem4  28162  mulsasslem3  28173  oncutlt  28272  axlowdimlem10  29036  shunssji  31457  shsval3i  31476  shjshsi  31580  spanuni  31632  sshhococi  31634  esumcst  34241  hashf2  34262  sxbrsigalem3  34450  signswch  34739  tz9.1regs  35312  bj-unrab  37174  bj-tagss  37228  bj-imdirco  37445  poimirlem16  37887  poimirlem19  37890  poimirlem23  37894  poimirlem29  37900  poimirlem31  37902  poimirlem32  37903  mblfinlem3  37910  mblfinlem4  37911  hdmapevec  42211  rtrclex  43973  trclexi  43976  rtrclexi  43977  cnvrcl0  43981  cnvtrcl0  43982  comptiunov2i  44062  cotrclrcl  44098  cncfiooicclem1  46251  fourierdlem62  46526