Theorem unssi 3750

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

Syntax hints:   ∧ wa 383   ∪ cun 3538   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  dmrnssfld  5305  tc2  8501  pwxpndom2  9366  ltrelxr  9978  nn0ssre  11173  nn0ssz  11275  dfle2  11856  difreicc  12175  hashxrcl  13010  ramxrcl  15559  strlemor1  15796  strleun  15799  cssincl  19851  leordtval2  20826  lecldbas  20833  comppfsc  21145  aalioulem2  23892  taylfval  23917  axlowdimlem10  25631  konigsberg  26514  shunssji  27612  shsval3i  27631  shjshsi  27735  spanuni  27787  sshhococi  27789  esumcst  29452  hashf2  29473  sxbrsigalem3  29661  signswch  29964  bj-unrab  32114  bj-tagss  32161  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  mblfinlem3  32618  mblfinlem4  32619  hdmapevec  36145  rtrclex  36943  trclexi  36946  rtrclexi  36947  cnvrcl0  36951  cnvtrcl0  36952  comptiunov2i  37017  cotrclrcl  37053  cncfiooicclem1  38779  fourierdlem62  39061