Theorem unissd 4870

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

Syntax hints:   → wi 4   ⊆ wss 3898  ∪ cuni 4860

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-uni 4861

This theorem is referenced by:  unieq  4871  dffv2  6925  onfununi  8269  fiuni  9321  dfac2a  10030  incexc  15748  incexc2  15749  isacs1i  17567  isacs3lem  18452  acsmapd  18464  acsmap2d  18465  dprdres  19946  dprd2da  19960  eltg3i  22879  unitg  22885  tgss  22886  tgcmp  23319  cmpfi  23326  alexsubALTlem4  23968  ptcmplem3  23972  ustbas2  24143  uniioombllem3  25516  madess  27824  oldss  27826  shsupunss  31330  locfinref  33877  cmpcref  33886  dya2iocucvr  34320  omssubadd  34336  carsggect  34354  carsgclctun  34357  cvmscld  35340  fnemeet1  36433  fnejoin1  36435  onsucsuccmpi  36510  heibor1  37873  heiborlem10  37883  hbt  43250  pwsal  46440  prsal  46443  intsaluni  46454  caragenuni  46636  caragendifcl  46639  cnfsmf  46865  smfsssmf  46868  smfpimbor1lem2  46924  toplatglb  49128  setrecsss  49829