Theorem unssi 4157

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

Syntax hints:   ∧ wa 395   ∪ cun 3915   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934

This theorem is referenced by:  pwunss  4584  dmrnssfld  5940  tc2  9702  djuunxp  9881  pwxpndom2  10625  ltrelxr  11242  nn0ssre  12453  nn0sscn  12454  nn0ssz  12559  dfle2  13114  difreicc  13452  hashxrcl  14329  ramxrcl  16995  strleun  17134  cssincl  21604  leordtval2  23106  lecldbas  23113  comppfsc  23426  aalioulem2  26248  taylfval  26273  addsbdaylem  27930  addsbday  27931  addsdilem3  28063  addsdilem4  28064  mulsasslem3  28075  onscutlt  28172  axlowdimlem10  28885  shunssji  31305  shsval3i  31324  shjshsi  31428  spanuni  31480  sshhococi  31482  esumcst  34060  hashf2  34081  sxbrsigalem3  34270  signswch  34559  bj-unrab  36921  bj-tagss  36975  bj-imdirco  37185  poimirlem16  37637  poimirlem19  37640  poimirlem23  37644  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  mblfinlem3  37660  mblfinlem4  37661  hdmapevec  41836  rtrclex  43613  trclexi  43616  rtrclexi  43617  cnvrcl0  43621  cnvtrcl0  43622  comptiunov2i  43702  cotrclrcl  43738  cncfiooicclem1  45898  fourierdlem62  46173