Theorem unissi 4883

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

Syntax hints:   ⊆ wss 3917  ∪ cuni 4874

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  unidif  4909  unixpss  5776  riotassuni  7387  unifpw  9313  fiuni  9386  rankuni  9823  fin23lem29  10301  fin23lem30  10302  fin1a2lem12  10371  prdsds  17434  psss  18546  tgval2  22850  eltg4i  22854  ntrss2  22951  isopn3  22960  mretopd  22986  ordtbas  23086  cmpcov2  23284  tgcmp  23295  comppfsc  23426  alexsublem  23938  alexsubALTlem3  23943  alexsubALTlem4  23944  cldsubg  24005  bndth  24864  uniioombllem4  25494  uniioombllem5  25495  omssubadd  34298  cvmscld  35267  fnessref  36352  inunissunidif  37370  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  mbfresfi  37667  cover2  37716  salexct  46339  salgencntex  46348