Theorem unissi 4854

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

Syntax hints:   ⊆ wss 3935  ∪ cuni 4831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-uni 4832

This theorem is referenced by:  unidif  4864  unixpss  5677  riotassuni  7148  unifpw  8821  fiuni  8886  rankuni  9286  fin23lem29  9757  fin23lem30  9758  fin1a2lem12  9827  prdsds  16731  psss  17818  tgval2  21558  eltg4i  21562  ntrss2  21659  isopn3  21668  mretopd  21694  ordtbas  21794  cmpcov2  21992  tgcmp  22003  comppfsc  22134  alexsublem  22646  alexsubALTlem3  22651  alexsubALTlem4  22652  cldsubg  22713  bndth  23556  uniioombllem4  24181  uniioombllem5  24182  omssubadd  31553  cvmscld  32515  fnessref  33700  inunissunidif  34650  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  mbfresfi  34932  cover2  34983  salexct  42611  salgencntex  42620