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 231	1 ⊢ (𝐴 ∪ 𝐵) ⊆ 𝐶

Syntax hints:   ∧ wa 396   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900

This theorem is referenced by:  pwunss  4547  dmrnssfld  5916  tc2  9652  djuunxp  9836  pwxpndom2  10579  ltrelxr  11197  nn0ssre  12432  nn0sscn  12433  nn0ssz  12538  dfle2  13089  difreicc  13428  hashxrcl  14310  ramxrcl  16979  strleun  17118  cssincl  21663  leordtval2  23195  lecldbas  23202  comppfsc  23515  aalioulem2  26317  taylfval  26342  addbdaylem  28027  addbday  28028  addsdilem3  28163  addsdilem4  28164  mulsasslem3  28175  oncutlt  28274  axlowdimlem10  29038  shunssji  31458  shsval3i  31477  shjshsi  31581  spanuni  31633  sshhococi  31635  esumcst  34247  hashf2  34268  sxbrsigalem3  34456  signswch  34745  tz9.1regs  35315  ttcuniun  36738  ttciunun  36739  ttcuni  36741  bj-unrab  37279  bj-tagss  37333  bj-imdirco  37550  poimirlem16  38003  poimirlem19  38006  poimirlem23  38010  poimirlem29  38016  poimirlem31  38018  poimirlem32  38019  mblfinlem3  38026  mblfinlem4  38027  hdmapevec  42327  rtrclex  44061  trclexi  44064  rtrclexi  44065  cnvrcl0  44069  cnvtrcl0  44070  comptiunov2i  44150  cotrclrcl  44186  cncfiooicclem1  46336  fourierdlem62  46611