Theorem unissi 4865

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

Syntax hints:   ⊆ wss 3897  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  unidif  4891  unixpss  5749  riotassuni  7343  unifpw  9239  fiuni  9312  rankuni  9756  fin23lem29  10232  fin23lem30  10233  fin1a2lem12  10302  prdsds  17368  psss  18486  tgval2  22871  eltg4i  22875  ntrss2  22972  isopn3  22981  mretopd  23007  ordtbas  23107  cmpcov2  23305  tgcmp  23316  comppfsc  23447  alexsublem  23959  alexsubALTlem3  23964  alexsubALTlem4  23965  cldsubg  24026  bndth  24884  uniioombllem4  25514  uniioombllem5  25515  omssubadd  34313  cvmscld  35317  fnessref  36401  inunissunidif  37419  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  mbfresfi  37705  cover2  37754  salexct  46431  salgencntex  46440