Theorem unissd 4887

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908  ∪ cuni 4877

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-uni 4878

This theorem is used by:  unieq  4888  dffv2  6983  onfununi  8337  fiuni  9398  dfac2a  10132  incexc  15917  incexc2  15918  isacs1i  17738  isacs3lem  18623  acsmapd  18635  acsmap2d  18636  dprdres  20131  dprd2da  20145  eltg3i  23155  unitg  23161  tgss  23162  tgcmp  23595  cmpfi  23602  alexsubALTlem4  24244  ptcmplem3  24248  ustbas2  24419  uniioombllem3  25781  madess  28096  oldss  28100  shsupunss  31735  locfinref  34262  cmpcref  34271  dya2iocucvr  34706  omssubadd  34722  carsggect  34740  carsgclctun  34743  cvmscld  35786  fnemeet1  36918  fnejoin1  36920  onsucsuccmpi  36995  heibor1  38502  heiborlem10  38512  hbt  43898  pwsal  47070  prsal  47073  intsaluni  47084  caragenuni  47266  caragendifcl  47269  cnfsmf  47495  smfsssmf  47498  smfpimbor1lem2  47554  toplatglb  49820  setrecsss  50520