Theorem unssi 4129

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

Syntax hints:   ∧ wa 396   ∪ cun 3894   ⊆ wss 3896

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3442  df-un 3901  df-in 3903  df-ss 3913

This theorem is referenced by:  pwunss  4562  dmrnssfld  5898  tc2  9577  djuunxp  9756  pwxpndom2  10500  ltrelxr  11115  nn0ssre  12316  nn0sscn  12317  nn0ssz  12420  dfle2  12960  difreicc  13295  hashxrcl  14150  ramxrcl  16792  strleun  16932  cssincl  20973  leordtval2  22443  lecldbas  22450  comppfsc  22763  aalioulem2  25573  taylfval  25598  axlowdimlem10  27452  shunssji  29863  shsval3i  29882  shjshsi  29986  spanuni  30038  sshhococi  30040  esumcst  32167  hashf2  32188  sxbrsigalem3  32375  signswch  32676  bj-unrab  35183  bj-tagss  35238  bj-imdirco  35438  poimirlem16  35870  poimirlem19  35873  poimirlem23  35877  poimirlem29  35883  poimirlem31  35885  poimirlem32  35886  mblfinlem3  35893  mblfinlem4  35894  hdmapevec  40075  rtrclex  41464  trclexi  41467  rtrclexi  41468  cnvrcl0  41472  cnvtrcl0  41473  comptiunov2i  41553  cotrclrcl  41589  cncfiooicclem1  43689  fourierdlem62  43964