Theorem unissd 4850

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

Syntax hints:   → wi 4   ⊆ wss 3938  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  unieq  4851  dffv2  6758  onfununi  7980  fiuni  8894  dfac2a  9557  incexc  15194  incexc2  15195  isacs1i  16930  isacs3lem  17778  acsmapd  17790  acsmap2d  17791  dprdres  19152  dprd2da  19166  eltg3i  21571  unitg  21577  tgss  21578  tgcmp  22011  cmpfi  22018  alexsubALTlem4  22660  ptcmplem3  22664  ustbas2  22836  uniioombllem3  24188  shsupunss  29125  locfinref  31107  cmpcref  31116  dya2iocucvr  31544  omssubadd  31560  carsggect  31578  carsgclctun  31581  cvmscld  32522  fnemeet1  33716  fnejoin1  33718  onsucsuccmpi  33793  heibor1  35090  heiborlem10  35100  hbt  39737  pwsal  42607  prsal  42610  intsaluni  42619  caragenuni  42800  caragendifcl  42803  cnfsmf  43024  smfsssmf  43027  smfpimbor1lem2  43081  setrecsss  44810