Theorem unssi 4144

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

This proof depends on syntax axioms:   ∧ wa 401   ∪ cun 3904   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  pwunss  4582  dmrnssfld  5966  tc2  9716  djuunxp  9923  pwxpndom2  10667  ltrelxr  11287  nn0ssre  12525  nn0sscn  12526  nn0ssz  12631  dfle2  13190  difreicc  13529  hashxrcl  14413  ramxrcl  17101  strleun  17241  cssincl  21890  leordtval2  23421  lecldbas  23428  comppfsc  23742  aalioulem2  26549  taylfval  26575  addbdaylem  28263  addbday  28264  addsdilem3  28399  addsdilem4  28400  mulsasslem3  28411  oncutlt  28510  axlowdimlem10  29358  shunssji  31794  shsval3i  31813  shjshsi  31917  spanuni  31969  sshhococi  31971  esumcst  34519  hashf2  34540  sxbrsigalem3  34729  signswch  35015  tz9.1regs  35606  ttcuniun  37080  ttciunun  37081  ttcuni  37083  bj-unrab  37621  bj-tagss  37675  bj-imdirco  37893  poimirlem16  38346  poimirlem19  38349  poimirlem23  38353  poimirlem29  38359  poimirlem31  38361  poimirlem32  38362  mblfinlem3  38369  mblfinlem4  38370  hdmapevec  42669  rtrclex  44403  trclexi  44406  rtrclexi  44407  cnvrcl0  44411  cnvtrcl0  44412  comptiunov2i  44492  cotrclrcl  44528  cncfiooicclem1  46667  fourierdlem62  46942