Theorem unssi 4141

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

Syntax hints:   ∧ wa 395   ∪ cun 3897   ⊆ wss 3899

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  pwunss  4570  dmrnssfld  5921  tc2  9647  djuunxp  9831  pwxpndom2  10574  ltrelxr  11191  nn0ssre  12403  nn0sscn  12404  nn0ssz  12509  dfle2  13059  difreicc  13398  hashxrcl  14278  ramxrcl  16943  strleun  17082  cssincl  21641  leordtval2  23154  lecldbas  23161  comppfsc  23474  aalioulem2  26295  taylfval  26320  addsbdaylem  27986  addsbday  27987  addsdilem3  28122  addsdilem4  28123  mulsasslem3  28134  onscutlt  28232  axlowdimlem10  28973  shunssji  31393  shsval3i  31412  shjshsi  31516  spanuni  31568  sshhococi  31570  esumcst  34169  hashf2  34190  sxbrsigalem3  34378  signswch  34667  tz9.1regs  35239  bj-unrab  37070  bj-tagss  37124  bj-imdirco  37334  poimirlem16  37776  poimirlem19  37779  poimirlem23  37783  poimirlem29  37789  poimirlem31  37791  poimirlem32  37792  mblfinlem3  37799  mblfinlem4  37800  hdmapevec  42034  rtrclex  43800  trclexi  43803  rtrclexi  43804  cnvrcl0  43808  cnvtrcl0  43809  comptiunov2i  43889  cotrclrcl  43925  cncfiooicclem1  46079  fourierdlem62  46354