Theorem unssi 4185

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

Syntax hints:   ∧ wa 396   ∪ cun 3946   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  pwunss  4620  dmrnssfld  5969  tc2  9736  djuunxp  9915  pwxpndom2  10659  ltrelxr  11274  nn0ssre  12475  nn0sscn  12476  nn0ssz  12580  dfle2  13125  difreicc  13460  hashxrcl  14316  ramxrcl  16949  strleun  17089  cssincl  21240  leordtval2  22715  lecldbas  22722  comppfsc  23035  aalioulem2  25845  taylfval  25870  addsdilem3  27605  addsdilem4  27606  mulsasslem3  27617  axlowdimlem10  28206  shunssji  30617  shsval3i  30636  shjshsi  30740  spanuni  30792  sshhococi  30794  esumcst  33056  hashf2  33077  sxbrsigalem3  33266  signswch  33567  bj-unrab  35801  bj-tagss  35856  bj-imdirco  36066  poimirlem16  36499  poimirlem19  36502  poimirlem23  36506  poimirlem29  36512  poimirlem31  36514  poimirlem32  36515  mblfinlem3  36522  mblfinlem4  36523  hdmapevec  40701  rtrclex  42358  trclexi  42361  rtrclexi  42362  cnvrcl0  42366  cnvtrcl0  42367  comptiunov2i  42447  cotrclrcl  42483  cncfiooicclem1  44599  fourierdlem62  44874