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

Syntax hints:   ∧ wa 395   ∪ cun 3949   ⊆ wss 3951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968

This theorem is referenced by:  pwunss  4618  dmrnssfld  5984  tc2  9782  djuunxp  9961  pwxpndom2  10705  ltrelxr  11322  nn0ssre  12530  nn0sscn  12531  nn0ssz  12636  dfle2  13189  difreicc  13524  hashxrcl  14396  ramxrcl  17055  strleun  17194  cssincl  21706  leordtval2  23220  lecldbas  23227  comppfsc  23540  aalioulem2  26375  taylfval  26400  addsbdaylem  28049  addsbday  28050  addsdilem3  28179  addsdilem4  28180  mulsasslem3  28191  pw2bday  28418  axlowdimlem10  28966  shunssji  31388  shsval3i  31407  shjshsi  31511  spanuni  31563  sshhococi  31565  esumcst  34064  hashf2  34085  sxbrsigalem3  34274  signswch  34576  bj-unrab  36927  bj-tagss  36981  bj-imdirco  37191  poimirlem16  37643  poimirlem19  37646  poimirlem23  37650  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  mblfinlem3  37666  mblfinlem4  37667  hdmapevec  41837  rtrclex  43630  trclexi  43633  rtrclexi  43634  cnvrcl0  43638  cnvtrcl0  43639  comptiunov2i  43719  cotrclrcl  43755  cncfiooicclem1  45908  fourierdlem62  46183