Theorem unissd 4855

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

Syntax hints:   → wi 4   ⊆ wss 3890  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-uni 4846

This theorem is referenced by:  unieq  4856  dffv2  6929  onfununi  8278  fiuni  9338  dfac2a  10050  incexc  15800  incexc2  15801  isacs1i  17621  isacs3lem  18506  acsmapd  18518  acsmap2d  18519  dprdres  20003  dprd2da  20017  eltg3i  22951  unitg  22957  tgss  22958  tgcmp  23391  cmpfi  23398  alexsubALTlem4  24040  ptcmplem3  24044  ustbas2  24215  uniioombllem3  25577  madess  27883  oldss  27887  shsupunss  31442  locfinref  34032  cmpcref  34041  dya2iocucvr  34475  omssubadd  34491  carsggect  34509  carsgclctun  34512  cvmscld  35508  fnemeet1  36601  fnejoin1  36603  onsucsuccmpi  36678  heibor1  38184  heiborlem10  38194  hbt  43582  pwsal  46765  prsal  46768  intsaluni  46779  caragenuni  46961  caragendifcl  46964  cnfsmf  47190  smfsssmf  47193  smfpimbor1lem2  47249  toplatglb  49498  setrecsss  50198