Theorem unissd 4919

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

Syntax hints:   → wi 4   ⊆ wss 3949  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  unieq  4920  dffv2  6987  onfununi  8341  fiuni  9423  dfac2a  10124  incexc  15783  incexc2  15784  isacs1i  17601  isacs3lem  18495  acsmapd  18507  acsmap2d  18508  dprdres  19898  dprd2da  19912  eltg3i  22464  unitg  22470  tgss  22471  tgcmp  22905  cmpfi  22912  alexsubALTlem4  23554  ptcmplem3  23558  ustbas2  23730  uniioombllem3  25102  madess  27372  shsupunss  30630  locfinref  32852  cmpcref  32861  dya2iocucvr  33314  omssubadd  33330  carsggect  33348  carsgclctun  33351  cvmscld  34295  fnemeet1  35299  fnejoin1  35301  onsucsuccmpi  35376  heibor1  36726  heiborlem10  36736  hbt  41920  pwsal  45079  prsal  45082  intsaluni  45093  caragenuni  45275  caragendifcl  45278  cnfsmf  45504  smfsssmf  45507  smfpimbor1lem2  45563  toplatglb  47674  setrecsss  47794