Theorem unissi 4845

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

Syntax hints:   ⊆ wss 3883  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  unidif  4872  unixpss  5709  riotassuni  7253  unifpw  9052  fiuni  9117  rankuni  9552  fin23lem29  10028  fin23lem30  10029  fin1a2lem12  10098  prdsds  17092  psss  18213  tgval2  22014  eltg4i  22018  ntrss2  22116  isopn3  22125  mretopd  22151  ordtbas  22251  cmpcov2  22449  tgcmp  22460  comppfsc  22591  alexsublem  23103  alexsubALTlem3  23108  alexsubALTlem4  23109  cldsubg  23170  bndth  24027  uniioombllem4  24655  uniioombllem5  24656  omssubadd  32167  cvmscld  33135  fnessref  34473  inunissunidif  35473  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  mbfresfi  35750  cover2  35799  salexct  43763  salgencntex  43772