Theorem unssi 4150

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

Syntax hints:   ∧ wa 395   ∪ cun 3909   ⊆ wss 3911

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 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  pwunss  4577  dmrnssfld  5926  tc2  9671  djuunxp  9850  pwxpndom2  10594  ltrelxr  11211  nn0ssre  12422  nn0sscn  12423  nn0ssz  12528  dfle2  13083  difreicc  13421  hashxrcl  14298  ramxrcl  16964  strleun  17103  cssincl  21630  leordtval2  23132  lecldbas  23139  comppfsc  23452  aalioulem2  26274  taylfval  26299  addsbdaylem  27963  addsbday  27964  addsdilem3  28096  addsdilem4  28097  mulsasslem3  28108  onscutlt  28205  axlowdimlem10  28931  shunssji  31348  shsval3i  31367  shjshsi  31471  spanuni  31523  sshhococi  31525  esumcst  34046  hashf2  34067  sxbrsigalem3  34256  signswch  34545  bj-unrab  36907  bj-tagss  36961  bj-imdirco  37171  poimirlem16  37623  poimirlem19  37626  poimirlem23  37630  poimirlem29  37636  poimirlem31  37638  poimirlem32  37639  mblfinlem3  37646  mblfinlem4  37647  hdmapevec  41822  rtrclex  43599  trclexi  43602  rtrclexi  43603  cnvrcl0  43607  cnvtrcl0  43608  comptiunov2i  43688  cotrclrcl  43724  cncfiooicclem1  45884  fourierdlem62  46159