Theorem unssi 4152

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

Syntax hints:   ∧ wa 400   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  pwunss  4585  dmrnssfld  5965  tc2  9709  djuunxp  9907  pwxpndom2  10650  ltrelxr  11270  nn0ssre  12508  nn0sscn  12509  nn0ssz  12614  dfle2  13172  difreicc  13511  hashxrcl  14393  ramxrcl  17077  strleun  17217  cssincl  21807  leordtval2  23338  lecldbas  23345  comppfsc  23658  aalioulem2  26463  taylfval  26488  addbdaylem  28176  addbday  28177  addsdilem3  28312  addsdilem4  28313  mulsasslem3  28324  oncutlt  28423  axlowdimlem10  29242  shunssji  31662  shsval3i  31681  shjshsi  31785  spanuni  31837  sshhococi  31839  esumcst  34398  hashf2  34419  sxbrsigalem3  34607  signswch  34893  tz9.1regs  35470  ttcuniun  36910  ttciunun  36911  ttcuni  36913  bj-unrab  37450  bj-tagss  37504  bj-imdirco  37722  poimirlem16  38175  poimirlem19  38178  poimirlem23  38182  poimirlem29  38188  poimirlem31  38190  poimirlem32  38191  mblfinlem3  38198  mblfinlem4  38199  hdmapevec  42499  rtrclex  44235  trclexi  44238  rtrclexi  44239  cnvrcl0  44243  cnvtrcl0  44244  comptiunov2i  44324  cotrclrcl  44360  cncfiooicclem1  46499  fourierdlem62  46774