Theorem unissi 4874

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

Syntax hints:   ⊆ wss 3903  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unidif  4900  unixpss  5767  riotassuni  7365  unifpw  9267  fiuni  9343  rankuni  9787  fin23lem29  10263  fin23lem30  10264  fin1a2lem12  10333  prdsds  17396  psss  18515  tgval2  22912  eltg4i  22916  ntrss2  23013  isopn3  23022  mretopd  23048  ordtbas  23148  cmpcov2  23346  tgcmp  23357  comppfsc  23488  alexsublem  24000  alexsubALTlem3  24005  alexsubALTlem4  24006  cldsubg  24067  bndth  24925  uniioombllem4  25555  uniioombllem5  25556  omssubadd  34478  cvmscld  35489  fnessref  36573  inunissunidif  37630  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  mbfresfi  37917  cover2  37966  salexct  46692  salgencntex  46701