Theorem unissd 4873

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

Syntax hints:   → wi 4   ⊆ wss 3901  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864

This theorem is referenced by:  unieq  4874  dffv2  6929  onfununi  8273  fiuni  9331  dfac2a  10040  incexc  15760  incexc2  15761  isacs1i  17580  isacs3lem  18465  acsmapd  18477  acsmap2d  18478  dprdres  19959  dprd2da  19973  eltg3i  22905  unitg  22911  tgss  22912  tgcmp  23345  cmpfi  23352  alexsubALTlem4  23994  ptcmplem3  23998  ustbas2  24169  uniioombllem3  25542  madess  27862  oldss  27866  shsupunss  31421  locfinref  33998  cmpcref  34007  dya2iocucvr  34441  omssubadd  34457  carsggect  34475  carsgclctun  34478  cvmscld  35467  fnemeet1  36560  fnejoin1  36562  onsucsuccmpi  36637  heibor1  38011  heiborlem10  38021  hbt  43372  pwsal  46559  prsal  46562  intsaluni  46573  caragenuni  46755  caragendifcl  46758  cnfsmf  46984  smfsssmf  46987  smfpimbor1lem2  47043  toplatglb  49246  setrecsss  49946