Theorem unissd 4815

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

Syntax hints:   → wi 4   ⊆ wss 3853  ∪ cuni 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-uni 4806

This theorem is referenced by:  unieq  4816  dffv2  6784  onfununi  8056  fiuni  9022  dfac2a  9708  incexc  15364  incexc2  15365  isacs1i  17114  isacs3lem  18002  acsmapd  18014  acsmap2d  18015  dprdres  19369  dprd2da  19383  eltg3i  21812  unitg  21818  tgss  21819  tgcmp  22252  cmpfi  22259  alexsubALTlem4  22901  ptcmplem3  22905  ustbas2  23077  uniioombllem3  24436  shsupunss  29381  locfinref  31459  cmpcref  31468  dya2iocucvr  31917  omssubadd  31933  carsggect  31951  carsgclctun  31954  cvmscld  32902  madess  33745  fnemeet1  34241  fnejoin1  34243  onsucsuccmpi  34318  heibor1  35654  heiborlem10  35664  hbt  40599  pwsal  43474  prsal  43477  intsaluni  43486  caragenuni  43667  caragendifcl  43670  cnfsmf  43891  smfsssmf  43894  smfpimbor1lem2  43948  toplatglb  45903  setrecsss  46020