Theorem unssi 4045

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

Syntax hints:   ∧ wa 387   ∪ cun 3823   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-un 3830  df-in 3832  df-ss 3839

This theorem is referenced by:  dmrnssfld  5676  tc2  8970  djuunxp  9136  pwxpndom2  9877  ltrelxr  10494  nn0ssre  11704  nn0sscn  11705  nn0ssz  11809  dfle2  12350  difreicc  12679  hashxrcl  13526  ramxrcl  16199  strleun  16437  cssincl  20524  leordtval2  21514  lecldbas  21521  comppfsc  21834  aalioulem2  24615  taylfval  24640  axlowdimlem10  26430  shunssji  28917  shsval3i  28936  shjshsi  29040  spanuni  29092  sshhococi  29094  esumcst  30923  hashf2  30944  sxbrsigalem3  31132  signswch  31438  bj-unrab  33679  bj-tagss  33745  poimirlem16  34297  poimirlem19  34300  poimirlem23  34304  poimirlem29  34310  poimirlem31  34312  poimirlem32  34313  mblfinlem3  34320  mblfinlem4  34321  hdmapevec  38364  rtrclex  39285  trclexi  39288  rtrclexi  39289  cnvrcl0  39293  cnvtrcl0  39294  comptiunov2i  39359  cotrclrcl  39395  cncfiooicclem1  41552  fourierdlem62  41830