Theorem unissd 4877

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

Syntax hints:   → wi 4   ⊆ wss 3907  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4868

This theorem is referenced by:  unieq  4878  dffv2  6966  onfununi  8316  fiuni  9376  dfac2a  10101  incexc  15879  incexc2  15880  isacs1i  17701  isacs3lem  18586  acsmapd  18598  acsmap2d  18599  dprdres  20088  dprd2da  20102  eltg3i  23075  unitg  23081  tgss  23082  tgcmp  23515  cmpfi  23522  alexsubALTlem4  24164  ptcmplem3  24168  ustbas2  24339  uniioombllem3  25701  madess  28013  oldss  28017  shsupunss  31603  locfinref  34143  cmpcref  34152  dya2iocucvr  34586  omssubadd  34602  carsggect  34620  carsgclctun  34623  cvmscld  35631  fnemeet1  36734  fnejoin1  36736  onsucsuccmpi  36811  heibor1  38316  heiborlem10  38326  hbt  43714  pwsal  46888  prsal  46891  intsaluni  46902  caragenuni  47084  caragendifcl  47087  cnfsmf  47313  smfsssmf  47316  smfpimbor1lem2  47372  toplatglb  49631  setrecsss  50331