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 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵

This proof depends on syntax axioms:   ⊆ wss 3906  ∪ cuni 4874

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875

This theorem is used by:  uniin  4898  unidif  4910  unixpss  5799  riotassuni  7416  unifpw  9319  fiuni  9395  rankuni  9842  fin23lem29  10340  fin23lem30  10341  fin1a2lem12  10410  prdsds  17539  psss  18658  tgval2  23163  eltg4i  23167  ntrss2  23264  isopn3  23273  mretopd  23299  ordtbas  23399  cmpcov2  23597  tgcmp  23608  comppfsc  23740  alexsublem  24252  alexsubALTlem3  24257  alexsubALTlem4  24258  cldsubg  24319  bndth  25168  uniioombllem4  25796  uniioombllem5  25797  omssubadd  34755  cvmscld  35802  fnessref  36925  ttcuniun  37078  ttcuni  37081  inunissunidif  38078  mblfinlem3  38367  mblfinlem4  38368  ismblfin  38369  mbfresfi  38374  cover2  38424  salexct  47106  salgencntex  47115