Theorem unissd 4919

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

Syntax hints:   → wi 4   ⊆ wss 3949  ∪ cuni 4909

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-uni 4910

This theorem is referenced by:  unieq  4920  dffv2  6987  onfununi  8345  fiuni  9427  dfac2a  10128  incexc  15789  incexc2  15790  isacs1i  17607  isacs3lem  18501  acsmapd  18513  acsmap2d  18514  dprdres  19941  dprd2da  19955  eltg3i  22686  unitg  22692  tgss  22693  tgcmp  23127  cmpfi  23134  alexsubALTlem4  23776  ptcmplem3  23780  ustbas2  23952  uniioombllem3  25336  madess  27606  shsupunss  30864  locfinref  33117  cmpcref  33126  dya2iocucvr  33579  omssubadd  33595  carsggect  33613  carsgclctun  33616  cvmscld  34560  fnemeet1  35556  fnejoin1  35558  onsucsuccmpi  35633  heibor1  36983  heiborlem10  36993  hbt  42176  pwsal  45331  prsal  45334  intsaluni  45345  caragenuni  45527  caragendifcl  45530  cnfsmf  45756  smfsssmf  45759  smfpimbor1lem2  45815  toplatglb  47715  setrecsss  47835