Theorem unissd 4893

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

Syntax hints:   → wi 4   ⊆ wss 3926  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  unieq  4894  dffv2  6974  onfununi  8355  fiuni  9440  dfac2a  10144  incexc  15853  incexc2  15854  isacs1i  17669  isacs3lem  18552  acsmapd  18564  acsmap2d  18565  dprdres  20011  dprd2da  20025  eltg3i  22899  unitg  22905  tgss  22906  tgcmp  23339  cmpfi  23346  alexsubALTlem4  23988  ptcmplem3  23992  ustbas2  24164  uniioombllem3  25538  madess  27840  shsupunss  31327  locfinref  33872  cmpcref  33881  dya2iocucvr  34316  omssubadd  34332  carsggect  34350  carsgclctun  34353  cvmscld  35295  fnemeet1  36384  fnejoin1  36386  onsucsuccmpi  36461  heibor1  37834  heiborlem10  37844  hbt  43154  pwsal  46344  prsal  46347  intsaluni  46358  caragenuni  46540  caragendifcl  46543  cnfsmf  46769  smfsssmf  46772  smfpimbor1lem2  46828  toplatglb  48975  setrecsss  49565