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 ⊢ ∪ 𝐴 ⊆ ∪ 𝐵

Syntax hints:   ⊆ wss 3905  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873

This theorem is referenced by:  uniin  4896  unidif  4908  unixpss  5797  riotassuni  7407  unifpw  9308  fiuni  9384  rankuni  9831  fin23lem29  10320  fin23lem30  10321  fin1a2lem12  10390  prdsds  17512  psss  18631  tgval2  23113  eltg4i  23117  ntrss2  23214  isopn3  23223  mretopd  23249  ordtbas  23349  cmpcov2  23547  tgcmp  23558  comppfsc  23689  alexsublem  24201  alexsubALTlem3  24206  alexsubALTlem4  24207  cldsubg  24268  bndth  25117  uniioombllem4  25745  uniioombllem5  25746  omssubadd  34690  cvmscld  35765  fnessref  36868  ttcuniun  37021  ttcuni  37024  inunissunidif  38021  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  mbfresfi  38317  cover2  38366  salexct  47048  salgencntex  47057