Theorem unissd 4884

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

Syntax hints:   → wi 4   ⊆ wss 3917  ∪ cuni 4874

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  unieq  4885  dffv2  6959  onfununi  8313  fiuni  9386  dfac2a  10090  incexc  15810  incexc2  15811  isacs1i  17625  isacs3lem  18508  acsmapd  18520  acsmap2d  18521  dprdres  19967  dprd2da  19981  eltg3i  22855  unitg  22861  tgss  22862  tgcmp  23295  cmpfi  23302  alexsubALTlem4  23944  ptcmplem3  23948  ustbas2  24120  uniioombllem3  25493  madess  27795  shsupunss  31282  locfinref  33838  cmpcref  33847  dya2iocucvr  34282  omssubadd  34298  carsggect  34316  carsgclctun  34319  cvmscld  35267  fnemeet1  36361  fnejoin1  36363  onsucsuccmpi  36438  heibor1  37811  heiborlem10  37821  hbt  43126  pwsal  46320  prsal  46323  intsaluni  46334  caragenuni  46516  caragendifcl  46519  cnfsmf  46745  smfsssmf  46748  smfpimbor1lem2  46804  toplatglb  48993  setrecsss  49694