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  4582  dmrnssfld  5962  tc2  9705  djuunxp  9903  pwxpndom2  10646  ltrelxr  11266  nn0ssre  12504  nn0sscn  12505  nn0ssz  12610  dfle2  13168  difreicc  13507  hashxrcl  14389  ramxrcl  17073  strleun  17213  cssincl  21803  leordtval2  23334  lecldbas  23341  comppfsc  23654  aalioulem2  26459  taylfval  26484  addbdaylem  28172  addbday  28173  addsdilem3  28308  addsdilem4  28309  mulsasslem3  28320  oncutlt  28419  axlowdimlem10  29238  shunssji  31658  shsval3i  31677  shjshsi  31781  spanuni  31833  sshhococi  31835  esumcst  34394  hashf2  34415  sxbrsigalem3  34603  signswch  34889  tz9.1regs  35466  ttcuniun  36906  ttciunun  36907  ttcuni  36909  bj-unrab  37446  bj-tagss  37500  bj-imdirco  37717  poimirlem16  38170  poimirlem19  38173  poimirlem23  38177  poimirlem29  38183  poimirlem31  38185  poimirlem32  38186  mblfinlem3  38193  mblfinlem4  38194  hdmapevec  42494  rtrclex  44228  trclexi  44231  rtrclexi  44232  cnvrcl0  44236  cnvtrcl0  44237  comptiunov2i  44317  cotrclrcl  44353  cncfiooicclem1  46492  fourierdlem62  46767