Theorem unissi 4876

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

This proof depends on syntax axioms:   ⊆ wss 3899  ∪ cuni 4867

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  uniin  4891  unidif  4903  unixpss  5791  riotassuni  7410  unifpw  9322  fiuni  9398  rankuni  9845  fin23lem29  10343  fin23lem30  10344  fin1a2lem12  10413  prdsds  17549  psss  18668  tgval2  23181  eltg4i  23185  ntrss2  23282  isopn3  23291  mretopd  23317  ordtbas  23417  cmpcov2  23615  tgcmp  23626  comppfsc  23758  alexsublem  24270  alexsubALTlem3  24275  alexsubALTlem4  24276  cldsubg  24337  bndth  25186  uniioombllem4  25814  uniioombllem5  25815  omssubadd  34811  cvmscld  35852  fnessref  36976  ttcuniun  37129  ttcuni  37132  inunissunidif  38129  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  mbfresfi  38415  cover2  38465  salexct  47162  salgencntex  47171