Theorem unissd 4861

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

Syntax hints:   → wi 4   ⊆ wss 3890  ∪ cuni 4851

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 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unieq  4862  dffv2  6929  onfununi  8274  fiuni  9334  dfac2a  10043  incexc  15793  incexc2  15794  isacs1i  17614  isacs3lem  18499  acsmapd  18511  acsmap2d  18512  dprdres  19996  dprd2da  20010  eltg3i  22936  unitg  22942  tgss  22943  tgcmp  23376  cmpfi  23383  alexsubALTlem4  24025  ptcmplem3  24029  ustbas2  24200  uniioombllem3  25562  madess  27872  oldss  27876  shsupunss  31432  locfinref  34001  cmpcref  34010  dya2iocucvr  34444  omssubadd  34460  carsggect  34478  carsgclctun  34481  cvmscld  35471  fnemeet1  36564  fnejoin1  36566  onsucsuccmpi  36641  heibor1  38145  heiborlem10  38155  hbt  43576  pwsal  46761  prsal  46764  intsaluni  46775  caragenuni  46957  caragendifcl  46960  cnfsmf  47186  smfsssmf  47189  smfpimbor1lem2  47245  toplatglb  49488  setrecsss  50188