Theorem unssi 4191

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

This proof depends on syntax axioms:   ∧ wa 401   ⊆ wss 3899   ∪ cun 4151

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-un 4153

This theorem is used by:  pwunss  4578  dmrnssfld  5960  tc2  9751  djuunxp  10012  pwxpndom2  10760  ltrelxr  11380  nn0ssre  12620  nn0sscn  12621  nn0ssz  12726  dfle2  13286  difreicc  13625  hashxrcl  14511  ramxrcl  17207  strleun  17347  cssincl  22006  leordtval2  23542  lecldbas  23549  comppfsc  23863  aalioulem2  26672  taylfval  26698  addbdaylem  28415  addbday  28416  addsdilem3  28551  addsdilem4  28552  mulsasslem3  28563  oncutlt  28662  axlowdimlem10  29541  shunssji  31983  shsval3i  32002  shjshsi  32106  spanuni  32158  sshhococi  32160  esumcst  34748  hashf2  34769  sxbrsigalem3  34957  signswch  35243  tz9.1regs  35873  ttcuniun  37425  ttciunun  37426  ttcuni  37428  bj-unrab  37966  bj-tagss  38020  bj-imdirco  38251  poimirlem16  38694  poimirlem19  38697  poimirlem23  38701  poimirlem29  38707  poimirlem31  38709  poimirlem32  38710  mblfinlem3  38717  mblfinlem4  38718  hdmapevec  43032  rtrclex  44757  trclexi  44760  rtrclexi  44761  cnvrcl0  44765  cnvtrcl0  44766  comptiunov2i  44846  cotrclrcl  44882  cncfiooicclem1  47042  fourierdlem62  47317  parhomssun  50886  parhomss2  50895  parhomss  50896