Theorem unssi 4137

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

This proof depends on syntax axioms:   ∧ wa 401   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  pwunss  4575  dmrnssfld  5956  tc2  9741  djuunxp  10002  pwxpndom2  10750  ltrelxr  11370  nn0ssre  12610  nn0sscn  12611  nn0ssz  12716  dfle2  13276  difreicc  13615  hashxrcl  14501  ramxrcl  17195  strleun  17335  cssincl  21994  leordtval2  23530  lecldbas  23537  comppfsc  23851  aalioulem2  26660  taylfval  26686  addbdaylem  28403  addbday  28404  addsdilem3  28539  addsdilem4  28540  mulsasslem3  28551  oncutlt  28650  axlowdimlem10  29529  shunssji  31971  shsval3i  31990  shjshsi  32094  spanuni  32146  sshhococi  32148  esumcst  34695  hashf2  34716  sxbrsigalem3  34904  signswch  35190  tz9.1regs  35802  ttcuniun  37298  ttciunun  37299  ttcuni  37301  bj-unrab  37839  bj-tagss  37893  bj-imdirco  38111  poimirlem16  38554  poimirlem19  38557  poimirlem23  38561  poimirlem29  38567  poimirlem31  38569  poimirlem32  38570  mblfinlem3  38577  mblfinlem4  38578  hdmapevec  42892  rtrclex  44616  trclexi  44619  rtrclexi  44620  cnvrcl0  44624  cnvtrcl0  44625  comptiunov2i  44705  cotrclrcl  44741  cncfiooicclem1  46902  fourierdlem62  47177