Theorem unssi 4186

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

Syntax hints:   ∧ wa 397   ∪ cun 3947   ⊆ wss 3949

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  pwunss  4621  dmrnssfld  5970  tc2  9737  djuunxp  9916  pwxpndom2  10660  ltrelxr  11275  nn0ssre  12476  nn0sscn  12477  nn0ssz  12581  dfle2  13126  difreicc  13461  hashxrcl  14317  ramxrcl  16950  strleun  17090  cssincl  21241  leordtval2  22716  lecldbas  22723  comppfsc  23036  aalioulem2  25846  taylfval  25871  addsdilem3  27608  addsdilem4  27609  mulsasslem3  27620  axlowdimlem10  28209  shunssji  30622  shsval3i  30641  shjshsi  30745  spanuni  30797  sshhococi  30799  esumcst  33061  hashf2  33082  sxbrsigalem3  33271  signswch  33572  bj-unrab  35806  bj-tagss  35861  bj-imdirco  36071  poimirlem16  36504  poimirlem19  36507  poimirlem23  36511  poimirlem29  36517  poimirlem31  36519  poimirlem32  36520  mblfinlem3  36527  mblfinlem4  36528  hdmapevec  40706  rtrclex  42368  trclexi  42371  rtrclexi  42372  cnvrcl0  42376  cnvtrcl0  42377  comptiunov2i  42457  cotrclrcl  42493  cncfiooicclem1  44609  fourierdlem62  44884