Theorem unssi 3931

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

Syntax hints:   ∧ wa 383   ∪ cun 3713   ⊆ wss 3715

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 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

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 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-in 3722  df-ss 3729

This theorem is referenced by:  dmrnssfld  5539  tc2  8793  pwxpndom2  9699  ltrelxr  10311  nn0ssre  11508  nn0ssz  11610  dfle2  12193  difreicc  12517  hashxrcl  13360  ramxrcl  15943  strlemor1OLD  16191  strleun  16194  cssincl  20254  leordtval2  21238  lecldbas  21245  comppfsc  21557  aalioulem2  24307  taylfval  24332  axlowdimlem10  26051  shunssji  28558  shsval3i  28577  shjshsi  28681  spanuni  28733  sshhococi  28735  esumcst  30455  hashf2  30476  sxbrsigalem3  30664  signswch  30968  bj-unrab  33247  bj-tagss  33292  poimirlem16  33756  poimirlem19  33759  poimirlem23  33763  poimirlem29  33769  poimirlem31  33771  poimirlem32  33772  mblfinlem3  33779  mblfinlem4  33780  hdmapevec  37647  rtrclex  38444  trclexi  38447  rtrclexi  38448  cnvrcl0  38452  cnvtrcl0  38453  comptiunov2i  38518  cotrclrcl  38554  cncfiooicclem1  40627  fourierdlem62  40906