Theorem unissi 4918

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

Syntax hints:   ⊆ wss 3949  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  unidif  4947  unixpss  5811  riotassuni  7406  unifpw  9355  fiuni  9423  rankuni  9858  fin23lem29  10336  fin23lem30  10337  fin1a2lem12  10406  prdsds  17410  psss  18533  tgval2  22459  eltg4i  22463  ntrss2  22561  isopn3  22570  mretopd  22596  ordtbas  22696  cmpcov2  22894  tgcmp  22905  comppfsc  23036  alexsublem  23548  alexsubALTlem3  23553  alexsubALTlem4  23554  cldsubg  23615  bndth  24474  uniioombllem4  25103  uniioombllem5  25104  omssubadd  33330  cvmscld  34295  fnessref  35290  inunissunidif  36304  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  mbfresfi  36582  cover2  36631  salexct  45098  salgencntex  45107