Theorem unissi 4874

Description: Subclass relationship for subclass union. Inference form of uniss 4873. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unissi.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
unissi	⊢ ∪ 𝐴 ⊆ ∪ 𝐵

Proof of Theorem unissi

Step	Hyp	Ref	Expression
1		unissi.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		uniss 4873	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵

Syntax hints:   ⊆ wss 3904  ∪ cuni 4865

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-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4866

This theorem is referenced by:  uniin  4889  unidif  4901  unixpss  5783  riotassuni  7393  unifpw  9298  fiuni  9374  rankuni  9821  fin23lem29  10298  fin23lem30  10299  fin1a2lem12  10368  prdsds  17493  psss  18612  tgval2  23013  eltg4i  23017  ntrss2  23114  isopn3  23123  mretopd  23149  ordtbas  23249  cmpcov2  23447  tgcmp  23458  comppfsc  23589  alexsublem  24101  alexsubALTlem3  24106  alexsubALTlem4  24107  cldsubg  24168  bndth  25017  uniioombllem4  25645  uniioombllem5  25646  omssubadd  34594  cvmscld  35620  fnessref  36714  ttcuniun  36867  ttcuni  36870  inunissunidif  37866  mblfinlem3  38155  mblfinlem4  38156  ismblfin  38157  mbfresfi  38162  cover2  38211  salexct  46905  salgencntex  46914