Theorem unissi 4917

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

Syntax hints:   ⊆ wss 3948  ∪ cuni 4908

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909

This theorem is referenced by:  unidif  4946  unixpss  5810  riotassuni  7409  unifpw  9361  fiuni  9429  rankuni  9864  fin23lem29  10342  fin23lem30  10343  fin1a2lem12  10412  prdsds  17417  psss  18543  tgval2  22779  eltg4i  22783  ntrss2  22881  isopn3  22890  mretopd  22916  ordtbas  23016  cmpcov2  23214  tgcmp  23225  comppfsc  23356  alexsublem  23868  alexsubALTlem3  23873  alexsubALTlem4  23874  cldsubg  23935  bndth  24804  uniioombllem4  25435  uniioombllem5  25436  omssubadd  33764  cvmscld  34729  fnessref  35708  inunissunidif  36722  mblfinlem3  36993  mblfinlem4  36994  ismblfin  36995  mbfresfi  37000  cover2  37049  salexct  45511  salgencntex  45520