Theorem unssi 4112

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

Syntax hints:   ∧ wa 399   ∪ cun 3879   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  pwunss  4517  dmrnssfld  5806  tc2  9168  djuunxp  9334  pwxpndom2  10076  ltrelxr  10691  nn0ssre  11889  nn0sscn  11890  nn0ssz  11991  dfle2  12528  difreicc  12862  hashxrcl  13714  ramxrcl  16343  strleun  16583  cssincl  20377  leordtval2  21817  lecldbas  21824  comppfsc  22137  aalioulem2  24929  taylfval  24954  axlowdimlem10  26745  shunssji  29152  shsval3i  29171  shjshsi  29275  spanuni  29327  sshhococi  29329  esumcst  31432  hashf2  31453  sxbrsigalem3  31640  signswch  31941  bj-unrab  34368  bj-tagss  34416  bj-imdirco  34605  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  mblfinlem3  35096  mblfinlem4  35097  hdmapevec  39131  rtrclex  40317  trclexi  40320  rtrclexi  40321  cnvrcl0  40325  cnvtrcl0  40326  comptiunov2i  40407  cotrclrcl  40443  cncfiooicclem1  42535  fourierdlem62  42810