Theorem unissi 4863

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

Syntax hints:   ⊆ wss 3897  ∪ cuni 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4855

This theorem is referenced by:  unidif  4888  unixpss  5745  riotassuni  7338  unifpw  9234  fiuni  9307  rankuni  9751  fin23lem29  10227  fin23lem30  10228  fin1a2lem12  10297  prdsds  17363  psss  18481  tgval2  22866  eltg4i  22870  ntrss2  22967  isopn3  22976  mretopd  23002  ordtbas  23102  cmpcov2  23300  tgcmp  23311  comppfsc  23442  alexsublem  23954  alexsubALTlem3  23959  alexsubALTlem4  23960  cldsubg  24021  bndth  24879  uniioombllem4  25509  uniioombllem5  25510  omssubadd  34305  cvmscld  35309  fnessref  36391  inunissunidif  37409  mblfinlem3  37699  mblfinlem4  37700  ismblfin  37701  mbfresfi  37706  cover2  37755  salexct  46372  salgencntex  46381