Theorem unissd 4872

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

Syntax hints:   → wi 4   ⊆ wss 3902  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-uni 4863

This theorem is referenced by:  unieq  4873  dffv2  6956  onfununi  8305  fiuni  9367  dfac2a  10079  incexc  15857  incexc2  15858  isacs1i  17679  isacs3lem  18564  acsmapd  18576  acsmap2d  18577  dprdres  20060  dprd2da  20074  eltg3i  23008  unitg  23014  tgss  23015  tgcmp  23448  cmpfi  23455  alexsubALTlem4  24097  ptcmplem3  24101  ustbas2  24272  uniioombllem3  25634  madess  27946  oldss  27950  shsupunss  31505  locfinref  34098  cmpcref  34107  dya2iocucvr  34541  omssubadd  34557  carsggect  34575  carsgclctun  34578  cvmscld  35583  fnemeet1  36686  fnejoin1  36688  onsucsuccmpi  36763  heibor1  38269  heiborlem10  38279  hbt  43667  pwsal  46849  prsal  46852  intsaluni  46863  caragenuni  47045  caragendifcl  47048  cnfsmf  47274  smfsssmf  47277  smfpimbor1lem2  47333  toplatglb  49582  setrecsss  50282