Theorem unissi 4859

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

Syntax hints:   ⊆ wss 3889  ∪ cuni 4850

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  unidif  4885  unixpss  5766  riotassuni  7364  unifpw  9265  fiuni  9341  rankuni  9787  fin23lem29  10263  fin23lem30  10264  fin1a2lem12  10333  prdsds  17427  psss  18546  tgval2  22921  eltg4i  22925  ntrss2  23022  isopn3  23031  mretopd  23057  ordtbas  23157  cmpcov2  23355  tgcmp  23366  comppfsc  23497  alexsublem  24009  alexsubALTlem3  24014  alexsubALTlem4  24015  cldsubg  24076  bndth  24925  uniioombllem4  25553  uniioombllem5  25554  omssubadd  34444  cvmscld  35455  fnessref  36539  ttcuniun  36692  ttcuni  36695  inunissunidif  37691  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  mbfresfi  37987  cover2  38036  salexct  46762  salgencntex  46771