Theorem unissi 4897

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

Syntax hints:   ⊆ wss 3931  ∪ cuni 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889

This theorem is referenced by:  unidif  4923  unixpss  5794  riotassuni  7407  unifpw  9372  fiuni  9445  rankuni  9882  fin23lem29  10360  fin23lem30  10361  fin1a2lem12  10430  prdsds  17483  psss  18595  tgval2  22899  eltg4i  22903  ntrss2  23000  isopn3  23009  mretopd  23035  ordtbas  23135  cmpcov2  23333  tgcmp  23344  comppfsc  23475  alexsublem  23987  alexsubALTlem3  23992  alexsubALTlem4  23993  cldsubg  24054  bndth  24913  uniioombllem4  25544  uniioombllem5  25545  omssubadd  34337  cvmscld  35300  fnessref  36380  inunissunidif  37398  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  mbfresfi  37695  cover2  37744  salexct  46330  salgencntex  46339