Theorem unissd 4846

Description: Subclass relationship for subclass union. Deduction form of uniss 4844. (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 4844	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3883  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  unieq  4847  dffv2  6845  onfununi  8143  fiuni  9117  dfac2a  9816  incexc  15477  incexc2  15478  isacs1i  17283  isacs3lem  18175  acsmapd  18187  acsmap2d  18188  dprdres  19546  dprd2da  19560  eltg3i  22019  unitg  22025  tgss  22026  tgcmp  22460  cmpfi  22467  alexsubALTlem4  23109  ptcmplem3  23113  ustbas2  23285  uniioombllem3  24654  shsupunss  29609  locfinref  31693  cmpcref  31702  dya2iocucvr  32151  omssubadd  32167  carsggect  32185  carsgclctun  32188  cvmscld  33135  madess  33986  fnemeet1  34482  fnejoin1  34484  onsucsuccmpi  34559  heibor1  35895  heiborlem10  35905  hbt  40871  pwsal  43746  prsal  43749  intsaluni  43758  caragenuni  43939  caragendifcl  43942  cnfsmf  44163  smfsssmf  44166  smfpimbor1lem2  44220  toplatglb  46175  setrecsss  46292