Theorem unssi 4154

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

Syntax hints:   ∧ wa 395   ∪ cun 3912   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  pwunss  4581  dmrnssfld  5937  tc2  9695  djuunxp  9874  pwxpndom2  10618  ltrelxr  11235  nn0ssre  12446  nn0sscn  12447  nn0ssz  12552  dfle2  13107  difreicc  13445  hashxrcl  14322  ramxrcl  16988  strleun  17127  cssincl  21597  leordtval2  23099  lecldbas  23106  comppfsc  23419  aalioulem2  26241  taylfval  26266  addsbdaylem  27923  addsbday  27924  addsdilem3  28056  addsdilem4  28057  mulsasslem3  28068  onscutlt  28165  axlowdimlem10  28878  shunssji  31298  shsval3i  31317  shjshsi  31421  spanuni  31473  sshhococi  31475  esumcst  34053  hashf2  34074  sxbrsigalem3  34263  signswch  34552  bj-unrab  36914  bj-tagss  36968  bj-imdirco  37178  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  mblfinlem3  37653  mblfinlem4  37654  hdmapevec  41829  rtrclex  43606  trclexi  43609  rtrclexi  43610  cnvrcl0  43614  cnvtrcl0  43615  comptiunov2i  43695  cotrclrcl  43731  cncfiooicclem1  45891  fourierdlem62  46166