Theorem unissi 4872

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

Syntax hints:   ⊆ wss 3901  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864

This theorem is referenced by:  unidif  4898  unixpss  5759  riotassuni  7355  unifpw  9255  fiuni  9331  rankuni  9775  fin23lem29  10251  fin23lem30  10252  fin1a2lem12  10321  prdsds  17384  psss  18503  tgval2  22900  eltg4i  22904  ntrss2  23001  isopn3  23010  mretopd  23036  ordtbas  23136  cmpcov2  23334  tgcmp  23345  comppfsc  23476  alexsublem  23988  alexsubALTlem3  23993  alexsubALTlem4  23994  cldsubg  24055  bndth  24913  uniioombllem4  25543  uniioombllem5  25544  omssubadd  34457  cvmscld  35467  fnessref  36551  inunissunidif  37580  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  mbfresfi  37867  cover2  37916  salexct  46578  salgencntex  46587