Theorem unissd 4883

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

Syntax hints:   → wi 4   ⊆ wss 3906  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-uni 4874

This theorem is referenced by:  unieq  4884  dffv2  6978  onfununi  8329  fiuni  9389  dfac2a  10114  incexc  15893  incexc2  15894  isacs1i  17714  isacs3lem  18599  acsmapd  18611  acsmap2d  18612  dprdres  20101  dprd2da  20115  eltg3i  23099  unitg  23105  tgss  23106  tgcmp  23539  cmpfi  23546  alexsubALTlem4  24188  ptcmplem3  24192  ustbas2  24363  uniioombllem3  25725  madess  28040  oldss  28044  shsupunss  31679  locfinref  34212  cmpcref  34221  dya2iocucvr  34655  omssubadd  34671  carsggect  34689  carsgclctun  34692  cvmscld  35746  fnemeet1  36858  fnejoin1  36860  onsucsuccmpi  36935  heibor1  38442  heiborlem10  38452  hbt  43840  pwsal  47012  prsal  47015  intsaluni  47026  caragenuni  47208  caragendifcl  47211  cnfsmf  47437  smfsssmf  47440  smfpimbor1lem2  47496  toplatglb  49762  setrecsss  50462