Theorem unssi 4132

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

Syntax hints:   ∧ wa 395   ∪ cun 3888   ⊆ wss 3890

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 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  pwunss  4560  dmrnssfld  5924  tc2  9655  djuunxp  9839  pwxpndom2  10582  ltrelxr  11200  nn0ssre  12435  nn0sscn  12436  nn0ssz  12541  dfle2  13092  difreicc  13431  hashxrcl  14313  ramxrcl  16982  strleun  17121  cssincl  21681  leordtval2  23190  lecldbas  23197  comppfsc  23510  aalioulem2  26313  taylfval  26338  addbdaylem  28026  addbday  28027  addsdilem3  28162  addsdilem4  28163  mulsasslem3  28174  oncutlt  28273  axlowdimlem10  29037  shunssji  31458  shsval3i  31477  shjshsi  31581  spanuni  31633  sshhococi  31635  esumcst  34226  hashf2  34247  sxbrsigalem3  34435  signswch  34724  tz9.1regs  35297  ttcuniun  36711  ttciunun  36712  ttcuni  36714  bj-unrab  37252  bj-tagss  37306  bj-imdirco  37523  poimirlem16  37974  poimirlem19  37977  poimirlem23  37981  poimirlem29  37987  poimirlem31  37989  poimirlem32  37990  mblfinlem3  37997  mblfinlem4  37998  hdmapevec  42298  rtrclex  44065  trclexi  44068  rtrclexi  44069  cnvrcl0  44073  cnvtrcl0  44074  comptiunov2i  44154  cotrclrcl  44190  cncfiooicclem1  46342  fourierdlem62  46617