Theorem unissi 4916

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

Syntax hints:   ⊆ wss 3951  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unidif  4942  unixpss  5820  riotassuni  7428  unifpw  9395  fiuni  9468  rankuni  9903  fin23lem29  10381  fin23lem30  10382  fin1a2lem12  10451  prdsds  17509  psss  18625  tgval2  22963  eltg4i  22967  ntrss2  23065  isopn3  23074  mretopd  23100  ordtbas  23200  cmpcov2  23398  tgcmp  23409  comppfsc  23540  alexsublem  24052  alexsubALTlem3  24057  alexsubALTlem4  24058  cldsubg  24119  bndth  24990  uniioombllem4  25621  uniioombllem5  25622  omssubadd  34302  cvmscld  35278  fnessref  36358  inunissunidif  37376  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  mbfresfi  37673  cover2  37722  salexct  46349  salgencntex  46358