Theorem unissd 4847

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

Syntax hints:   → wi 4   ⊆ wss 3935  ∪ cuni 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-uni 4838

This theorem is referenced by:  unieq  4848  dffv2  6755  onfununi  7977  fiuni  8891  dfac2a  9554  incexc  15191  incexc2  15192  isacs1i  16927  isacs3lem  17775  acsmapd  17787  acsmap2d  17788  dprdres  19149  dprd2da  19163  eltg3i  21568  unitg  21574  tgss  21575  tgcmp  22008  cmpfi  22015  alexsubALTlem4  22657  ptcmplem3  22661  ustbas2  22833  uniioombllem3  24185  shsupunss  29122  locfinref  31105  cmpcref  31114  dya2iocucvr  31542  omssubadd  31558  carsggect  31576  carsgclctun  31579  cvmscld  32520  fnemeet1  33714  fnejoin1  33716  onsucsuccmpi  33791  heibor1  35087  heiborlem10  35097  hbt  39728  pwsal  42599  prsal  42602  intsaluni  42611  caragenuni  42792  caragendifcl  42795  cnfsmf  43016  smfsssmf  43019  smfpimbor1lem2  43073  setrecsss  44802