Theorem unissd 4875

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

Syntax hints:   → wi 4   ⊆ wss 3903  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unieq  4876  dffv2  6937  onfununi  8283  fiuni  9343  dfac2a  10052  incexc  15772  incexc2  15773  isacs1i  17592  isacs3lem  18477  acsmapd  18489  acsmap2d  18490  dprdres  19971  dprd2da  19985  eltg3i  22917  unitg  22923  tgss  22924  tgcmp  23357  cmpfi  23364  alexsubALTlem4  24006  ptcmplem3  24010  ustbas2  24181  uniioombllem3  25554  madess  27874  oldss  27878  shsupunss  31433  locfinref  34018  cmpcref  34027  dya2iocucvr  34461  omssubadd  34477  carsggect  34495  carsgclctun  34498  cvmscld  35486  fnemeet1  36579  fnejoin1  36581  onsucsuccmpi  36656  heibor1  38058  heiborlem10  38068  hbt  43484  pwsal  46670  prsal  46673  intsaluni  46684  caragenuni  46866  caragendifcl  46869  cnfsmf  47095  smfsssmf  47098  smfpimbor1lem2  47154  toplatglb  49357  setrecsss  50057