Theorem unissi 4885

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

Syntax hints:   ⊆ wss 3913  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877

This theorem is referenced by:  uniin  4900  unidif  4912  unixpss  5798  riotassuni  7408  unifpw  9311  fiuni  9387  rankuni  9834  fin23lem29  10324  fin23lem30  10325  fin1a2lem12  10394  prdsds  17516  psss  18635  tgval2  23081  eltg4i  23085  ntrss2  23182  isopn3  23191  mretopd  23217  ordtbas  23317  cmpcov2  23515  tgcmp  23526  comppfsc  23657  alexsublem  24169  alexsubALTlem3  24174  alexsubALTlem4  24175  cldsubg  24236  bndth  25085  uniioombllem4  25713  uniioombllem5  25714  omssubadd  34634  cvmscld  35663  fnessref  36756  ttcuniun  36909  ttcuni  36912  inunissunidif  37908  mblfinlem3  38197  mblfinlem4  38198  ismblfin  38199  mbfresfi  38204  cover2  38253  salexct  46939  salgencntex  46948