Theorem unssi 4201

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

Syntax hints:   ∧ wa 395   ∪ cun 3961   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  pwunss  4623  dmrnssfld  5987  tc2  9780  djuunxp  9959  pwxpndom2  10703  ltrelxr  11320  nn0ssre  12528  nn0sscn  12529  nn0ssz  12634  dfle2  13186  difreicc  13521  hashxrcl  14393  ramxrcl  17051  strleun  17191  cssincl  21724  leordtval2  23236  lecldbas  23243  comppfsc  23556  aalioulem2  26390  taylfval  26415  addsbdaylem  28064  addsbday  28065  addsdilem3  28194  addsdilem4  28195  mulsasslem3  28206  pw2bday  28433  axlowdimlem10  28981  shunssji  31398  shsval3i  31417  shjshsi  31521  spanuni  31573  sshhococi  31575  esumcst  34044  hashf2  34065  sxbrsigalem3  34254  signswch  34555  bj-unrab  36909  bj-tagss  36963  bj-imdirco  37173  poimirlem16  37623  poimirlem19  37626  poimirlem23  37630  poimirlem29  37636  poimirlem31  37638  poimirlem32  37639  mblfinlem3  37646  mblfinlem4  37647  hdmapevec  41818  rtrclex  43607  trclexi  43610  rtrclexi  43611  cnvrcl0  43615  cnvtrcl0  43616  comptiunov2i  43696  cotrclrcl  43732  cncfiooicclem1  45849  fourierdlem62  46124