Theorem unissd 4730

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

Syntax hints:   → wi 4   ⊆ wss 3825  ∪ cuni 4706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-in 3832  df-ss 3839  df-uni 4707

This theorem is referenced by:  dffv2  6578  onfununi  7775  fiuni  8679  dfac2a  9341  incexc  15042  incexc2  15043  isacs1i  16776  isacs3lem  17624  acsmapd  17636  acsmap2d  17637  dprdres  18890  dprd2da  18904  eltg3i  21263  unitg  21269  tgss  21270  tgcmp  21703  cmpfi  21710  alexsubALTlem4  22352  ptcmplem3  22356  ustbas2  22527  uniioombllem3  23879  shsupunss  28894  locfinref  30706  cmpcref  30715  dya2iocucvr  31144  omssubadd  31160  carsggect  31178  cvmscld  32065  fnemeet1  33175  fnejoin1  33177  onsucsuccmpi  33251  heibor1  34478  heiborlem10  34488  hbt  39071  prsal  41980  caragenuni  42170  caragendifcl  42173  cnfsmf  42394  smfsssmf  42397  smfpimbor1lem2  42451  setrecsss  44110