Theorem unssi 4196

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

Syntax hints:   ∧ wa 394   ∪ cun 3957   ⊆ wss 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-un 3964  df-ss 3976

This theorem is referenced by:  pwunss  4628  dmrnssfld  5981  tc2  9792  djuunxp  9971  pwxpndom2  10715  ltrelxr  11332  nn0ssre  12538  nn0sscn  12539  nn0ssz  12643  dfle2  13190  difreicc  13525  hashxrcl  14386  ramxrcl  17040  strleun  17180  cssincl  21706  leordtval2  23230  lecldbas  23237  comppfsc  23550  aalioulem2  26384  taylfval  26409  addsdilem3  28177  addsdilem4  28178  mulsasslem3  28189  axlowdimlem10  28908  shunssji  31325  shsval3i  31344  shjshsi  31448  spanuni  31500  sshhococi  31502  esumcst  33934  hashf2  33955  sxbrsigalem3  34144  signswch  34445  bj-unrab  36680  bj-tagss  36734  bj-imdirco  36944  poimirlem16  37384  poimirlem19  37387  poimirlem23  37391  poimirlem29  37397  poimirlem31  37399  poimirlem32  37400  mblfinlem3  37407  mblfinlem4  37408  hdmapevec  41581  rtrclex  43355  trclexi  43358  rtrclexi  43359  cnvrcl0  43363  cnvtrcl0  43364  comptiunov2i  43444  cotrclrcl  43480  cncfiooicclem1  45584  fourierdlem62  45859