Theorem unissd 4871

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

Syntax hints:   → wi 4   ⊆ wss 3905  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-uni 4862

This theorem is referenced by:  unieq  4872  dffv2  6922  onfununi  8271  fiuni  9337  dfac2a  10043  incexc  15762  incexc2  15763  isacs1i  17581  isacs3lem  18466  acsmapd  18478  acsmap2d  18479  dprdres  19927  dprd2da  19941  eltg3i  22864  unitg  22870  tgss  22871  tgcmp  23304  cmpfi  23311  alexsubALTlem4  23953  ptcmplem3  23957  ustbas2  24129  uniioombllem3  25502  madess  27808  oldss  27810  shsupunss  31308  locfinref  33810  cmpcref  33819  dya2iocucvr  34254  omssubadd  34270  carsggect  34288  carsgclctun  34291  cvmscld  35248  fnemeet1  36342  fnejoin1  36344  onsucsuccmpi  36419  heibor1  37792  heiborlem10  37802  hbt  43106  pwsal  46300  prsal  46303  intsaluni  46314  caragenuni  46496  caragendifcl  46499  cnfsmf  46725  smfsssmf  46728  smfpimbor1lem2  46784  toplatglb  48989  setrecsss  49690