Theorem unissi 4921

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

Syntax hints:   ⊆ wss 3963  ∪ cuni 4912

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913

This theorem is referenced by:  unidif  4947  unixpss  5823  riotassuni  7428  unifpw  9393  fiuni  9466  rankuni  9901  fin23lem29  10379  fin23lem30  10380  fin1a2lem12  10449  prdsds  17511  psss  18638  tgval2  22979  eltg4i  22983  ntrss2  23081  isopn3  23090  mretopd  23116  ordtbas  23216  cmpcov2  23414  tgcmp  23425  comppfsc  23556  alexsublem  24068  alexsubALTlem3  24073  alexsubALTlem4  24074  cldsubg  24135  bndth  25004  uniioombllem4  25635  uniioombllem5  25636  omssubadd  34282  cvmscld  35258  fnessref  36340  inunissunidif  37358  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  mbfresfi  37653  cover2  37702  salexct  46290  salgencntex  46299