Theorem unssi 4192

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

This proof depends on syntax axioms:   ∧ wa 401   ⊆ wss 3900   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  pwunss  4579  dmrnssfld  5968  tc2  9778  djuunxp  10039  pwxpndom2  10789  ltrelxr  11409  nn0ssre  12650  nn0sscn  12651  nn0ssz  12756  dfle2  13316  difreicc  13655  hashxrcl  14542  ramxrcl  17239  strleun  17379  cssincl  22049  leordtval2  23585  lecldbas  23592  comppfsc  23906  aalioulem2  26717  taylfval  26743  addbdaylem  28460  addbday  28461  addsdilem3  28596  addsdilem4  28597  mulsasslem3  28608  oncutlt  28707  axlowdimlem10  29586  shunssji  32028  shsval3i  32047  shjshsi  32151  spanuni  32203  sshhococi  32205  esumcst  34806  hashf2  34827  sxbrsigalem3  35015  signswch  35301  tz9.1regs  35943  ttcuniun  37513  ttciunun  37514  ttcuni  37516  bj-unrab  38054  bj-tagss  38108  bj-imdirco  38379  poimirlem16  38822  poimirlem19  38825  poimirlem23  38829  poimirlem29  38835  poimirlem31  38837  poimirlem32  38838  mblfinlem3  38845  mblfinlem4  38846  hdmapevec  43158  rtrclex  44878  trclexi  44881  rtrclexi  44882  cnvrcl0  44886  cnvtrcl0  44887  comptiunov2i  44967  cotrclrcl  45003  cncfiooicclem1  47176  fourierdlem62  47451  parhomssun  51078  parhomss2  51087  parhomss  51088