Theorem unissi 4879

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

Syntax hints:   ⊆ wss 3913  ∪ cuni 4870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871

This theorem is referenced by:  unidif  4908  unixpss  5771  riotassuni  7359  unifpw  9306  fiuni  9373  rankuni  9808  fin23lem29  10286  fin23lem30  10287  fin1a2lem12  10356  prdsds  17360  psss  18483  tgval2  22343  eltg4i  22347  ntrss2  22445  isopn3  22454  mretopd  22480  ordtbas  22580  cmpcov2  22778  tgcmp  22789  comppfsc  22920  alexsublem  23432  alexsubALTlem3  23437  alexsubALTlem4  23438  cldsubg  23499  bndth  24358  uniioombllem4  24987  uniioombllem5  24988  omssubadd  32989  cvmscld  33954  fnessref  34905  inunissunidif  35919  mblfinlem3  36190  mblfinlem4  36191  ismblfin  36192  mbfresfi  36197  cover2  36246  salexct  44695  salgencntex  44704