Theorem unssi 4163

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

Syntax hints:   ∧ wa 398   ∪ cun 3936   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954

This theorem is referenced by:  pwunss  4561  dmrnssfld  5843  tc2  9186  djuunxp  9352  pwxpndom2  10089  ltrelxr  10704  nn0ssre  11904  nn0sscn  11905  nn0ssz  12006  dfle2  12543  difreicc  12873  hashxrcl  13721  ramxrcl  16355  strleun  16593  cssincl  20834  leordtval2  21822  lecldbas  21829  comppfsc  22142  aalioulem2  24924  taylfval  24949  axlowdimlem10  26739  shunssji  29148  shsval3i  29167  shjshsi  29271  spanuni  29323  sshhococi  29325  esumcst  31324  hashf2  31345  sxbrsigalem3  31532  signswch  31833  bj-unrab  34246  bj-tagss  34294  poimirlem16  34910  poimirlem19  34913  poimirlem23  34917  poimirlem29  34923  poimirlem31  34925  poimirlem32  34926  mblfinlem3  34933  mblfinlem4  34934  hdmapevec  38973  rtrclex  39984  trclexi  39987  rtrclexi  39988  cnvrcl0  39992  cnvtrcl0  39993  comptiunov2i  40058  cotrclrcl  40094  cncfiooicclem1  42183  fourierdlem62  42460