Theorem unssi 4142

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920

This theorem is referenced by:  pwunss  4569  dmrnssfld  5915  tc2  9638  djuunxp  9817  pwxpndom2  10559  ltrelxr  11176  nn0ssre  12388  nn0sscn  12389  nn0ssz  12494  dfle2  13049  difreicc  13387  hashxrcl  14264  ramxrcl  16929  strleun  17068  cssincl  21595  leordtval2  23097  lecldbas  23104  comppfsc  23417  aalioulem2  26239  taylfval  26264  addsbdaylem  27928  addsbday  27929  addsdilem3  28061  addsdilem4  28062  mulsasslem3  28073  onscutlt  28170  axlowdimlem10  28896  shunssji  31313  shsval3i  31332  shjshsi  31436  spanuni  31488  sshhococi  31490  esumcst  34036  hashf2  34057  sxbrsigalem3  34246  signswch  34535  tz9.1regs  35073  bj-unrab  36910  bj-tagss  36964  bj-imdirco  37174  poimirlem16  37626  poimirlem19  37629  poimirlem23  37633  poimirlem29  37639  poimirlem31  37641  poimirlem32  37642  mblfinlem3  37649  mblfinlem4  37650  hdmapevec  41824  rtrclex  43600  trclexi  43603  rtrclexi  43604  cnvrcl0  43608  cnvtrcl0  43609  comptiunov2i  43689  cotrclrcl  43725  cncfiooicclem1  45884  fourierdlem62  46159