Theorem unissd 4876

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  unieq  4877  dffv2  6981  onfununi  8353  fiuni  9424  dfac2a  10212  incexc  16012  incexc2  16013  isacs1i  17837  isacs3lem  18722  acsmapd  18734  acsmap2d  18735  dprdres  20250  dprd2da  20264  eltg3i  23285  unitg  23291  tgss  23292  tgcmp  23725  cmpfi  23732  alexsubALTlem4  24375  ptcmplem3  24379  ustbas2  24550  uniioombllem3  25912  madess  28258  oldss  28262  shsupunss  31954  locfinref  34520  cmpcref  34529  dya2iocucvr  34963  omssubadd  34979  carsggect  34997  carsgclctun  35000  cvmscld  36125  fnemeet1  37247  fnejoin1  37249  onsucsuccmpi  37324  heibor1  38838  heiborlem10  38848  hbt  44226  pwsal  47419  prsal  47422  intsaluni  47433  caragenuni  47615  caragendifcl  47618  cnfsmf  47844  smfsssmf  47847  smfpimbor1lem2  47903  toplatglb  50209  setrecsss  50963