Theorem unssi 4144

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

Syntax hints:   ∧ wa 400   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922

This theorem is referenced by:  pwunss  4580  dmrnssfld  5964  tc2  9705  djuunxp  9903  pwxpndom2  10645  ltrelxr  11265  nn0ssre  12503  nn0sscn  12504  nn0ssz  12609  dfle2  13167  difreicc  13506  hashxrcl  14389  ramxrcl  17072  strleun  17212  cssincl  21838  leordtval2  23369  lecldbas  23376  comppfsc  23689  aalioulem2  26496  taylfval  26522  addbdaylem  28210  addbday  28211  addsdilem3  28346  addsdilem4  28347  mulsasslem3  28358  oncutlt  28457  axlowdimlem10  29301  shunssji  31721  shsval3i  31740  shjshsi  31844  spanuni  31896  sshhococi  31898  esumcst  34453  hashf2  34474  sxbrsigalem3  34662  signswch  34948  tz9.1regs  35547  ttcuniun  37041  ttciunun  37042  ttcuni  37044  bj-unrab  37582  bj-tagss  37636  bj-imdirco  37854  poimirlem16  38307  poimirlem19  38310  poimirlem23  38314  poimirlem29  38320  poimirlem31  38322  poimirlem32  38323  mblfinlem3  38330  mblfinlem4  38331  hdmapevec  42629  rtrclex  44363  trclexi  44366  rtrclexi  44367  cnvrcl0  44371  cnvtrcl0  44372  comptiunov2i  44452  cotrclrcl  44488  cncfiooicclem1  46627  fourierdlem62  46902