Theorem unissd 4880

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  unieq  4881  dffv2  6977  onfununi  8334  fiuni  9402  dfac2a  10136  incexc  15930  incexc2  15931  isacs1i  17751  isacs3lem  18636  acsmapd  18648  acsmap2d  18649  dprdres  20163  dprd2da  20177  eltg3i  23192  unitg  23198  tgss  23199  tgcmp  23632  cmpfi  23639  alexsubALTlem4  24282  ptcmplem3  24286  ustbas2  24457  uniioombllem3  25819  madess  28139  oldss  28143  shsupunss  31835  locfinref  34359  cmpcref  34368  dya2iocucvr  34803  omssubadd  34819  carsggect  34837  carsgclctun  34840  cvmscld  35860  fnemeet1  36993  fnejoin1  36995  onsucsuccmpi  37070  heibor1  38568  heiborlem10  38578  hbt  43979  pwsal  47151  prsal  47154  intsaluni  47165  caragenuni  47347  caragendifcl  47350  cnfsmf  47576  smfsssmf  47579  smfpimbor1lem2  47635  toplatglb  49935  setrecsss  50635