Theorem unssi 3766

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

Syntax hints:   ∧ wa 384   ∪ cun 3553   ⊆ wss 3555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-in 3562  df-ss 3569

This theorem is referenced by:  dmrnssfld  5344  tc2  8562  pwxpndom2  9431  ltrelxr  10043  nn0ssre  11240  nn0ssz  11342  dfle2  11924  difreicc  12246  hashxrcl  13088  ramxrcl  15645  strlemor1OLD  15890  strleun  15893  cssincl  19951  leordtval2  20926  lecldbas  20933  comppfsc  21245  aalioulem2  23992  taylfval  24017  axlowdimlem10  25731  shunssji  28077  shsval3i  28096  shjshsi  28200  spanuni  28252  sshhococi  28254  esumcst  29906  hashf2  29927  sxbrsigalem3  30115  signswch  30418  bj-unrab  32569  bj-tagss  32615  poimirlem16  33057  poimirlem19  33060  poimirlem23  33064  poimirlem29  33070  poimirlem31  33072  poimirlem32  33073  mblfinlem3  33080  mblfinlem4  33081  hdmapevec  36607  rtrclex  37405  trclexi  37408  rtrclexi  37409  cnvrcl0  37413  cnvtrcl0  37414  comptiunov2i  37479  cotrclrcl  37515  cncfiooicclem1  39410  fourierdlem62  39692