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  34030  hashf2  34051  sxbrsigalem3  34240  signswch  34529  tz9.1regs  35067  bj-unrab  36904  bj-tagss  36958  bj-imdirco  37168  poimirlem16  37620  poimirlem19  37623  poimirlem23  37627  poimirlem29  37633  poimirlem31  37635  poimirlem32  37636  mblfinlem3  37643  mblfinlem4  37644  hdmapevec  41818  rtrclex  43594  trclexi  43597  rtrclexi  43598  cnvrcl0  43602  cnvtrcl0  43603  comptiunov2i  43683  cotrclrcl  43719  cncfiooicclem1  45878  fourierdlem62  46153