Theorem unissd 4849

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

Syntax hints:   → wi 4   ⊆ wss 3887  ∪ cuni 4839

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  unieq  4850  dffv2  6863  onfununi  8172  fiuni  9187  dfac2a  9885  incexc  15549  incexc2  15550  isacs1i  17366  isacs3lem  18260  acsmapd  18272  acsmap2d  18273  dprdres  19631  dprd2da  19645  eltg3i  22111  unitg  22117  tgss  22118  tgcmp  22552  cmpfi  22559  alexsubALTlem4  23201  ptcmplem3  23205  ustbas2  23377  uniioombllem3  24749  shsupunss  29708  locfinref  31791  cmpcref  31800  dya2iocucvr  32251  omssubadd  32267  carsggect  32285  carsgclctun  32288  cvmscld  33235  madess  34059  fnemeet1  34555  fnejoin1  34557  onsucsuccmpi  34632  heibor1  35968  heiborlem10  35978  hbt  40955  pwsal  43856  prsal  43859  intsaluni  43868  caragenuni  44049  caragendifcl  44052  cnfsmf  44276  smfsssmf  44279  smfpimbor1lem2  44333  toplatglb  46287  setrecsss  46406