Theorem unissi 4847

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

Syntax hints:   ⊆ wss 3883  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839

This theorem is referenced by:  unidif  4873  unixpss  5753  riotassuni  7353  unifpw  9255  fiuni  9331  rankuni  9778  fin23lem29  10254  fin23lem30  10255  fin1a2lem12  10324  prdsds  17418  psss  18537  tgval2  22939  eltg4i  22943  ntrss2  23040  isopn3  23049  mretopd  23075  ordtbas  23175  cmpcov2  23373  tgcmp  23384  comppfsc  23515  alexsublem  24027  alexsubALTlem3  24032  alexsubALTlem4  24033  cldsubg  24094  bndth  24943  uniioombllem4  25571  uniioombllem5  25572  omssubadd  34484  cvmscld  35501  fnessref  36585  ttcuniun  36738  ttcuni  36741  inunissunidif  37737  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  mbfresfi  38033  cover2  38082  salexct  46777  salgencntex  46786