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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  pwunss  4575  dmrnssfld  5958  tc2  9720  djuunxp  9927  pwxpndom2  10675  ltrelxr  11295  nn0ssre  12533  nn0sscn  12534  nn0ssz  12639  dfle2  13199  difreicc  13538  hashxrcl  14422  ramxrcl  17110  strleun  17250  cssincl  21902  leordtval2  23438  lecldbas  23445  comppfsc  23759  aalioulem2  26570  taylfval  26596  addbdaylem  28283  addbday  28284  addsdilem3  28419  addsdilem4  28420  mulsasslem3  28431  oncutlt  28530  axlowdimlem10  29409  shunssji  31851  shsval3i  31870  shjshsi  31974  spanuni  32026  sshhococi  32028  esumcst  34574  hashf2  34595  sxbrsigalem3  34784  signswch  35070  tz9.1regs  35661  ttcuniun  37130  ttciunun  37131  ttcuni  37133  bj-unrab  37671  bj-tagss  37725  bj-imdirco  37943  poimirlem16  38386  poimirlem19  38389  poimirlem23  38393  poimirlem29  38399  poimirlem31  38401  poimirlem32  38402  mblfinlem3  38409  mblfinlem4  38410  hdmapevec  42709  rtrclex  44458  trclexi  44461  rtrclexi  44462  cnvrcl0  44466  cnvtrcl0  44467  comptiunov2i  44547  cotrclrcl  44583  cncfiooicclem1  46722  fourierdlem62  46997