Theorem unissd 4860

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

Syntax hints:   → wi 4   ⊆ wss 3889  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  unieq  4861  dffv2  6935  onfununi  8281  fiuni  9341  dfac2a  10052  incexc  15802  incexc2  15803  isacs1i  17623  isacs3lem  18508  acsmapd  18520  acsmap2d  18521  dprdres  20005  dprd2da  20019  eltg3i  22926  unitg  22932  tgss  22933  tgcmp  23366  cmpfi  23373  alexsubALTlem4  24015  ptcmplem3  24019  ustbas2  24190  uniioombllem3  25552  madess  27858  oldss  27862  shsupunss  31417  locfinref  33985  cmpcref  33994  dya2iocucvr  34428  omssubadd  34444  carsggect  34462  carsgclctun  34465  cvmscld  35455  fnemeet1  36548  fnejoin1  36550  onsucsuccmpi  36625  heibor1  38131  heiborlem10  38141  hbt  43558  pwsal  46743  prsal  46746  intsaluni  46757  caragenuni  46939  caragendifcl  46942  cnfsmf  47168  smfsssmf  47171  smfpimbor1lem2  47227  toplatglb  49476  setrecsss  50176