Theorem unssi 4143

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

Syntax hints:   ∧ wa 399   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921

This theorem is referenced by:  pwunss  4573  dmrnssfld  5950  tc2  9695  djuunxp  9879  pwxpndom2  10623  ltrelxr  11243  nn0ssre  12485  nn0sscn  12486  nn0ssz  12591  dfle2  13149  difreicc  13488  hashxrcl  14370  ramxrcl  17053  strleun  17193  cssincl  21740  leordtval2  23272  lecldbas  23279  comppfsc  23592  aalioulem2  26397  taylfval  26422  addbdaylem  28110  addbday  28111  addsdilem3  28246  addsdilem4  28247  mulsasslem3  28258  oncutlt  28357  axlowdimlem10  29152  shunssji  31572  shsval3i  31591  shjshsi  31695  spanuni  31747  sshhococi  31749  esumcst  34360  hashf2  34381  sxbrsigalem3  34569  signswch  34855  tz9.1regs  35430  ttcuniun  36870  ttciunun  36871  ttcuni  36873  bj-unrab  37411  bj-tagss  37465  bj-imdirco  37682  poimirlem16  38135  poimirlem19  38138  poimirlem23  38142  poimirlem29  38148  poimirlem31  38150  poimirlem32  38151  mblfinlem3  38158  mblfinlem4  38159  hdmapevec  42459  rtrclex  44193  trclexi  44196  rtrclexi  44197  cnvrcl0  44201  cnvtrcl0  44202  comptiunov2i  44282  cotrclrcl  44318  cncfiooicclem1  46467  fourierdlem62  46742