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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868

This theorem is used by:  uniin  4891  unidif  4903  unixpss  5788  riotassuni  7417  unifpw  9344  fiuni  9420  rankuni  9879  fin23lem29  10419  fin23lem30  10420  fin1a2lem12  10489  prdsds  17635  psss  18754  tgval2  23274  eltg4i  23278  ntrss2  23375  isopn3  23384  mretopd  23410  ordtbas  23510  cmpcov2  23708  tgcmp  23719  comppfsc  23851  alexsublem  24363  alexsubALTlem3  24368  alexsubALTlem4  24369  cldsubg  24430  bndth  25279  uniioombllem4  25907  uniioombllem5  25908  omssubadd  34932  cvmscld  36038  fnessref  37145  ttcuniun  37298  ttcuni  37301  inunissunidif  38299  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  mbfresfi  38585  cover2  38650  salexct  47344  salgencntex  47353