Theorem unissi 4683

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

Syntax hints:   ⊆ wss 3798  ∪ cuni 4658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812  df-uni 4659

This theorem is referenced by:  unidif  4693  unixpss  5468  riotassuni  6903  unifpw  8538  fiuni  8603  rankuni  9003  fin23lem29  9478  fin23lem30  9479  fin1a2lem12  9548  prdsds  16477  psss  17567  tgval2  21131  eltg4i  21135  ntrss2  21232  isopn3  21241  mretopd  21267  ordtbas  21367  cmpcov2  21564  tgcmp  21575  comppfsc  21706  alexsublem  22218  alexsubALTlem3  22223  alexsubALTlem4  22224  cldsubg  22284  bndth  23127  uniioombllem4  23752  uniioombllem5  23753  omssubadd  30907  cvmscld  31801  fnessref  32890  mblfinlem3  33992  mblfinlem4  33993  ismblfin  33994  mbfresfi  33999  cover2  34051  salexct  41343  salgencntex  41352