Theorem unssi 4143

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  pwunss  4572  dmrnssfld  5923  tc2  9649  djuunxp  9833  pwxpndom2  10576  ltrelxr  11193  nn0ssre  12405  nn0sscn  12406  nn0ssz  12511  dfle2  13061  difreicc  13400  hashxrcl  14280  ramxrcl  16945  strleun  17084  cssincl  21643  leordtval2  23156  lecldbas  23163  comppfsc  23476  aalioulem2  26297  taylfval  26322  addbdaylem  28013  addbday  28014  addsdilem3  28149  addsdilem4  28150  mulsasslem3  28161  oncutlt  28260  axlowdimlem10  29024  shunssji  31444  shsval3i  31463  shjshsi  31567  spanuni  31619  sshhococi  31621  esumcst  34220  hashf2  34241  sxbrsigalem3  34429  signswch  34718  tz9.1regs  35290  bj-unrab  37127  bj-tagss  37181  bj-imdirco  37395  poimirlem16  37837  poimirlem19  37840  poimirlem23  37844  poimirlem29  37850  poimirlem31  37852  poimirlem32  37853  mblfinlem3  37860  mblfinlem4  37861  hdmapevec  42105  rtrclex  43868  trclexi  43871  rtrclexi  43872  cnvrcl0  43876  cnvtrcl0  43877  comptiunov2i  43957  cotrclrcl  43993  cncfiooicclem1  46147  fourierdlem62  46422