Theorem unssi 4214

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

Syntax hints:   ∧ wa 395   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  pwunss  4640  dmrnssfld  5996  tc2  9811  djuunxp  9990  pwxpndom2  10734  ltrelxr  11351  nn0ssre  12557  nn0sscn  12558  nn0ssz  12662  dfle2  13209  difreicc  13544  hashxrcl  14406  ramxrcl  17064  strleun  17204  cssincl  21729  leordtval2  23241  lecldbas  23248  comppfsc  23561  aalioulem2  26393  taylfval  26418  addsbdaylem  28067  addsbday  28068  addsdilem3  28197  addsdilem4  28198  mulsasslem3  28209  pw2bday  28436  axlowdimlem10  28984  shunssji  31401  shsval3i  31420  shjshsi  31524  spanuni  31576  sshhococi  31578  esumcst  34027  hashf2  34048  sxbrsigalem3  34237  signswch  34538  bj-unrab  36892  bj-tagss  36946  bj-imdirco  37156  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  mblfinlem3  37619  mblfinlem4  37620  hdmapevec  41792  rtrclex  43579  trclexi  43582  rtrclexi  43583  cnvrcl0  43587  cnvtrcl0  43588  comptiunov2i  43668  cotrclrcl  43704  cncfiooicclem1  45814  fourierdlem62  46089