Theorem unissd 4881

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

Syntax hints:   → wi 4   ⊆ wss 3914  ∪ cuni 4871

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 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unieq  4882  dffv2  6956  onfununi  8310  fiuni  9379  dfac2a  10083  incexc  15803  incexc2  15804  isacs1i  17618  isacs3lem  18501  acsmapd  18513  acsmap2d  18514  dprdres  19960  dprd2da  19974  eltg3i  22848  unitg  22854  tgss  22855  tgcmp  23288  cmpfi  23295  alexsubALTlem4  23937  ptcmplem3  23941  ustbas2  24113  uniioombllem3  25486  madess  27788  shsupunss  31275  locfinref  33831  cmpcref  33840  dya2iocucvr  34275  omssubadd  34291  carsggect  34309  carsgclctun  34312  cvmscld  35260  fnemeet1  36354  fnejoin1  36356  onsucsuccmpi  36431  heibor1  37804  heiborlem10  37814  hbt  43119  pwsal  46313  prsal  46316  intsaluni  46327  caragenuni  46509  caragendifcl  46512  cnfsmf  46738  smfsssmf  46741  smfpimbor1lem2  46797  toplatglb  48989  setrecsss  49690