Theorem unissi 4875

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

This proof depends on syntax axioms:   ⊆ wss 3896  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-uni 4867

This theorem is used by:  uniin  4890  unidif  4902  unixpss  5789  riotassuni  7421  unifpw  9351  fiuni  9427  rankuni  9886  fin23lem29  10426  fin23lem30  10427  fin1a2lem12  10496  prdsds  17644  psss  18763  tgval2  23283  eltg4i  23287  ntrss2  23384  isopn3  23393  mretopd  23419  ordtbas  23519  cmpcov2  23717  tgcmp  23728  comppfsc  23860  alexsublem  24372  alexsubALTlem3  24377  alexsubALTlem4  24378  cldsubg  24439  bndth  25288  uniioombllem4  25916  uniioombllem5  25917  omssubadd  34982  cvmscld  36128  fnessref  37241  ttcuniun  37394  ttcuni  37397  inunissunidif  38407  mblfinlem3  38686  mblfinlem4  38687  ismblfin  38688  mbfresfi  38693  cover2  38758  salexct  47452  salgencntex  47461