Theorem unissd 4880

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ∪ cuni 4870

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  unieq  4881  dffv2  7006  onfununi  8380  fiuni  9450  dfac2a  10238  incexc  16038  incexc2  16039  isacs1i  17863  isacs3lem  18748  acsmapd  18760  acsmap2d  18761  dprdres  20277  dprd2da  20291  eltg3i  23312  unitg  23318  tgss  23319  tgcmp  23752  cmpfi  23759  alexsubALTlem4  24402  ptcmplem3  24406  ustbas2  24577  uniioombllem3  25939  madess  28285  oldss  28289  shsupunss  31981  locfinref  34556  cmpcref  34565  dya2iocucvr  34999  omssubadd  35015  carsggect  35033  carsgclctun  35036  cvmscld  36218  fnemeet1  37345  fnejoin1  37347  onsucsuccmpi  37422  heibor1  38947  heiborlem10  38957  hbt  44335  pwsal  47540  prsal  47543  intsaluni  47554  caragenuni  47736  caragendifcl  47739  cnfsmf  47965  smfsssmf  47968  smfpimbor1lem2  48024  toplatglb  50330  setrecsss  51084