Theorem unissd 4941

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

Syntax hints:   → wi 4   ⊆ wss 3976  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932

This theorem is referenced by:  unieq  4942  dffv2  7017  onfununi  8397  fiuni  9497  dfac2a  10199  incexc  15885  incexc2  15886  isacs1i  17715  isacs3lem  18612  acsmapd  18624  acsmap2d  18625  dprdres  20072  dprd2da  20086  eltg3i  22989  unitg  22995  tgss  22996  tgcmp  23430  cmpfi  23437  alexsubALTlem4  24079  ptcmplem3  24083  ustbas2  24255  uniioombllem3  25639  madess  27933  shsupunss  31378  locfinref  33787  cmpcref  33796  dya2iocucvr  34249  omssubadd  34265  carsggect  34283  carsgclctun  34286  cvmscld  35241  fnemeet1  36332  fnejoin1  36334  onsucsuccmpi  36409  heibor1  37770  heiborlem10  37780  hbt  43087  pwsal  46236  prsal  46239  intsaluni  46250  caragenuni  46432  caragendifcl  46435  cnfsmf  46661  smfsssmf  46664  smfpimbor1lem2  46720  toplatglb  48673  setrecsss  48793