Theorem unissd 4860

Description: Subclass relationship for subclass union. Deduction form of uniss 4858. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
unissd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
unissd	⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)

Proof of Theorem unissd

Step	Hyp	Ref	Expression
1		unissd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		uniss 4858	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3897  ∪ cuni 4850

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3904  df-ss 3914  df-uni 4851

This theorem is referenced by:  unieq  4861  dffv2  6902  onfununi  8219  fiuni  9257  dfac2a  9958  incexc  15621  incexc2  15622  isacs1i  17436  isacs3lem  18330  acsmapd  18342  acsmap2d  18343  dprdres  19699  dprd2da  19713  eltg3i  22183  unitg  22189  tgss  22190  tgcmp  22624  cmpfi  22631  alexsubALTlem4  23273  ptcmplem3  23277  ustbas2  23449  uniioombllem3  24821  shsupunss  29817  locfinref  31897  cmpcref  31906  dya2iocucvr  32357  omssubadd  32373  carsggect  32391  carsgclctun  32394  cvmscld  33340  madess  34117  fnemeet1  34613  fnejoin1  34615  onsucsuccmpi  34690  heibor1  36024  heiborlem10  36034  hbt  41159  pwsal  44093  prsal  44096  intsaluni  44105  caragenuni  44287  caragendifcl  44290  cnfsmf  44516  smfsssmf  44519  smfpimbor1lem2  44575  toplatglb  46539  setrecsss  46658