Theorem unissi 4809

Description: Subclass relationship for subclass union. Inference form of uniss 4808. (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 4808	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵

Syntax hints:   ⊆ wss 3881  ∪ cuni 4800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  unidif  4834  unixpss  5647  riotassuni  7133  unifpw  8811  fiuni  8876  rankuni  9276  fin23lem29  9752  fin23lem30  9753  fin1a2lem12  9822  prdsds  16729  psss  17816  tgval2  21561  eltg4i  21565  ntrss2  21662  isopn3  21671  mretopd  21697  ordtbas  21797  cmpcov2  21995  tgcmp  22006  comppfsc  22137  alexsublem  22649  alexsubALTlem3  22654  alexsubALTlem4  22655  cldsubg  22716  bndth  23563  uniioombllem4  24190  uniioombllem5  24191  omssubadd  31668  cvmscld  32633  fnessref  33818  inunissunidif  34792  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  mbfresfi  35103  cover2  35152  salexct  42974  salgencntex  42983