Theorem unissd 4877

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ∪ cuni 4867

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868

This theorem is used by:  unieq  4878  dffv2  6972  onfununi  8333  fiuni  9404  dfac2a  10189  incexc  15986  incexc2  15987  isacs1i  17811  isacs3lem  18696  acsmapd  18708  acsmap2d  18709  dprdres  20224  dprd2da  20238  eltg3i  23259  unitg  23265  tgss  23266  tgcmp  23699  cmpfi  23706  alexsubALTlem4  24349  ptcmplem3  24353  ustbas2  24524  uniioombllem3  25886  madess  28234  oldss  28238  shsupunss  31930  locfinref  34455  cmpcref  34464  dya2iocucvr  34899  omssubadd  34915  carsggect  34933  carsgclctun  34936  cvmscld  36007  fnemeet1  37124  fnejoin1  37126  onsucsuccmpi  37201  heibor1  38712  heiborlem10  38722  hbt  44090  pwsal  47269  prsal  47272  intsaluni  47283  caragenuni  47465  caragendifcl  47468  cnfsmf  47694  smfsssmf  47697  smfpimbor1lem2  47753  toplatglb  50053  setrecsss  50738