Theorem unissd 4917

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

Syntax hints:   → wi 4   ⊆ wss 3951  ∪ cuni 4907

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unieq  4918  dffv2  7004  onfununi  8381  fiuni  9468  dfac2a  10170  incexc  15873  incexc2  15874  isacs1i  17700  isacs3lem  18587  acsmapd  18599  acsmap2d  18600  dprdres  20048  dprd2da  20062  eltg3i  22968  unitg  22974  tgss  22975  tgcmp  23409  cmpfi  23416  alexsubALTlem4  24058  ptcmplem3  24062  ustbas2  24234  uniioombllem3  25620  madess  27915  shsupunss  31365  locfinref  33840  cmpcref  33849  dya2iocucvr  34286  omssubadd  34302  carsggect  34320  carsgclctun  34323  cvmscld  35278  fnemeet1  36367  fnejoin1  36369  onsucsuccmpi  36444  heibor1  37817  heiborlem10  37827  hbt  43142  pwsal  46330  prsal  46333  intsaluni  46344  caragenuni  46526  caragendifcl  46529  cnfsmf  46755  smfsssmf  46758  smfpimbor1lem2  46814  toplatglb  48890  setrecsss  49220