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 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  unieq  4878  dffv2  6974  onfununi  8331  fiuni  9401  dfac2a  10135  incexc  15929  incexc2  15930  isacs1i  17748  isacs3lem  18633  acsmapd  18645  acsmap2d  18646  dprdres  20160  dprd2da  20174  eltg3i  23189  unitg  23195  tgss  23196  tgcmp  23629  cmpfi  23636  alexsubALTlem4  24279  ptcmplem3  24283  ustbas2  24454  uniioombllem3  25816  madess  28134  oldss  28138  shsupunss  31830  locfinref  34354  cmpcref  34363  dya2iocucvr  34798  omssubadd  34814  carsggect  34832  carsgclctun  34835  cvmscld  35855  fnemeet1  36988  fnejoin1  36990  onsucsuccmpi  37065  heibor1  38563  heiborlem10  38573  hbt  43974  pwsal  47146  prsal  47149  intsaluni  47160  caragenuni  47342  caragendifcl  47345  cnfsmf  47571  smfsssmf  47574  smfpimbor1lem2  47630  toplatglb  49930  setrecsss  50630