Theorem unissi 4876

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

This proof depends on syntax axioms:   ⊆ wss 3899  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868

This theorem is used by:  uniin  4891  unidif  4903  unixpss  5788  riotassuni  7415  unifpw  9337  fiuni  9413  rankuni  9872  fin23lem29  10412  fin23lem30  10413  fin1a2lem12  10482  prdsds  17628  psss  18747  tgval2  23267  eltg4i  23271  ntrss2  23368  isopn3  23377  mretopd  23403  ordtbas  23503  cmpcov2  23701  tgcmp  23712  comppfsc  23844  alexsublem  24356  alexsubALTlem3  24361  alexsubALTlem4  24362  cldsubg  24423  bndth  25272  uniioombllem4  25900  uniioombllem5  25901  omssubadd  34925  cvmscld  36017  fnessref  37125  ttcuniun  37278  ttcuni  37281  inunissunidif  38278  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  mbfresfi  38564  cover2  38629  salexct  47313  salgencntex  47322