Theorem unissi 4880

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

Syntax hints:   ⊆ wss 3914  ∪ cuni 4871

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unidif  4906  unixpss  5773  riotassuni  7384  unifpw  9306  fiuni  9379  rankuni  9816  fin23lem29  10294  fin23lem30  10295  fin1a2lem12  10364  prdsds  17427  psss  18539  tgval2  22843  eltg4i  22847  ntrss2  22944  isopn3  22953  mretopd  22979  ordtbas  23079  cmpcov2  23277  tgcmp  23288  comppfsc  23419  alexsublem  23931  alexsubALTlem3  23936  alexsubALTlem4  23937  cldsubg  23998  bndth  24857  uniioombllem4  25487  uniioombllem5  25488  omssubadd  34291  cvmscld  35260  fnessref  36345  inunissunidif  37363  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  mbfresfi  37660  cover2  37709  salexct  46332  salgencntex  46341