Theorem unissi 4881

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

This proof depends on syntax axioms:   ⊆ wss 3900  ∪ cuni 4872

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4873

This theorem is used by:  uniin  4896  unidif  4908  unixpss  5797  riotassuni  7448  unifpw  9382  fiuni  9457  rankuni  9916  fin23lem29  10458  fin23lem30  10459  fin1a2lem12  10528  prdsds  17685  psss  18804  tgval2  23329  eltg4i  23333  ntrss2  23430  isopn3  23439  mretopd  23465  ordtbas  23565  cmpcov2  23763  tgcmp  23774  comppfsc  23906  alexsublem  24418  alexsubALTlem3  24423  alexsubALTlem4  24424  cldsubg  24485  bndth  25334  uniioombllem4  25962  uniioombllem5  25963  omssubadd  35043  cvmscld  36246  fnessref  37360  ttcuniun  37513  ttcuni  37516  inunissunidif  38566  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  mbfresfi  38852  cover2  38917  salexct  47617  salgencntex  47626