Theorem unissi 4870

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

Syntax hints:   ⊆ wss 3899  ∪ cuni 4861

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-uni 4862

This theorem is referenced by:  unidif  4896  unixpss  5757  riotassuni  7353  unifpw  9253  fiuni  9329  rankuni  9773  fin23lem29  10249  fin23lem30  10250  fin1a2lem12  10319  prdsds  17382  psss  18501  tgval2  22898  eltg4i  22902  ntrss2  22999  isopn3  23008  mretopd  23034  ordtbas  23134  cmpcov2  23332  tgcmp  23343  comppfsc  23474  alexsublem  23986  alexsubALTlem3  23991  alexsubALTlem4  23992  cldsubg  24053  bndth  24911  uniioombllem4  25541  uniioombllem5  25542  omssubadd  34406  cvmscld  35416  fnessref  36500  inunissunidif  37519  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  mbfresfi  37806  cover2  37855  salexct  46520  salgencntex  46529