Theorem unissd 4570

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

Syntax hints:   → wi 4   ⊆ wss 3680  ∪ cuni 4544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-in 3687  df-ss 3694  df-uni 4545

This theorem is referenced by:  dffv2  6385  onfununi  7558  fiuni  8450  dfac2a  9065  incexc  14689  incexc2  14690  isacs1i  16440  isacs3lem  17288  acsmapd  17300  acsmap2d  17301  dprdres  18548  dprd2da  18562  eltg3i  20888  unitg  20894  tgss  20895  tgcmp  21327  cmpfi  21334  alexsubALTlem4  21976  ptcmplem3  21980  ustbas2  22151  uniioombllem3  23474  shsupunss  28435  locfinref  30138  cmpcref  30147  dya2iocucvr  30576  omssubadd  30592  carsggect  30610  cvmscld  31483  fnemeet1  32588  fnejoin1  32590  onsucsuccmpi  32669  heibor1  33841  heiborlem10  33851  hbt  38119  caragenuni  41148  caragendifcl  41151  cnfsmf  41372  smfsssmf  41375  smfpimbor1lem2  41429  setrecsss  42874