Theorem unssi 3932

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

Syntax hints:   ∧ wa 383   ∪ cun 3714   ⊆ wss 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730

This theorem is referenced by:  dmrnssfld  5540  tc2  8794  pwxpndom2  9700  ltrelxr  10312  nn0ssre  11509  nn0ssz  11611  dfle2  12194  difreicc  12518  hashxrcl  13361  ramxrcl  15944  strlemor1OLD  16192  strleun  16195  cssincl  20255  leordtval2  21239  lecldbas  21246  comppfsc  21558  aalioulem2  24308  taylfval  24333  axlowdimlem10  26052  shunssji  28559  shsval3i  28578  shjshsi  28682  spanuni  28734  sshhococi  28736  esumcst  30456  hashf2  30477  sxbrsigalem3  30665  signswch  30969  bj-unrab  33248  bj-tagss  33293  poimirlem16  33757  poimirlem19  33760  poimirlem23  33764  poimirlem29  33770  poimirlem31  33772  poimirlem32  33773  mblfinlem3  33780  mblfinlem4  33781  hdmapevec  37648  rtrclex  38445  trclexi  38448  rtrclexi  38449  cnvrcl0  38453  cnvtrcl0  38454  comptiunov2i  38519  cotrclrcl  38555  cncfiooicclem1  40628  fourierdlem62  40907