Theorem unssi 4120

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

Syntax hints:   ∧ wa 396   ∪ cun 3886   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905

This theorem is referenced by:  pwunss  4554  dmrnssfld  5882  tc2  9509  djuunxp  9688  pwxpndom2  10430  ltrelxr  11045  nn0ssre  12246  nn0sscn  12247  nn0ssz  12350  dfle2  12890  difreicc  13225  hashxrcl  14081  ramxrcl  16727  strleun  16867  cssincl  20902  leordtval2  22372  lecldbas  22379  comppfsc  22692  aalioulem2  25502  taylfval  25527  axlowdimlem10  27328  shunssji  29740  shsval3i  29759  shjshsi  29863  spanuni  29915  sshhococi  29917  esumcst  32040  hashf2  32061  sxbrsigalem3  32248  signswch  32549  bj-unrab  35123  bj-tagss  35179  bj-imdirco  35370  poimirlem16  35802  poimirlem19  35805  poimirlem23  35809  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  mblfinlem3  35825  mblfinlem4  35826  hdmapevec  39856  rtrclex  41232  trclexi  41235  rtrclexi  41236  cnvrcl0  41240  cnvtrcl0  41241  comptiunov2i  41321  cotrclrcl  41357  cncfiooicclem1  43441  fourierdlem62  43716