Theorem unissd 4462

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

Syntax hints:   → wi 4   ⊆ wss 3574  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437

This theorem is referenced by:  dffv2  6271  onfununi  7438  fiuni  8334  dfac2a  8952  incexc  14569  incexc2  14570  isacs1i  16318  isacs3lem  17166  acsmapd  17178  acsmap2d  17179  dprdres  18427  dprd2da  18441  eltg3i  20765  unitg  20771  tgss  20772  tgcmp  21204  cmpfi  21211  alexsubALTlem4  21854  ptcmplem3  21858  ustbas2  22029  uniioombllem3  23353  shsupunss  28205  locfinref  29908  cmpcref  29917  dya2iocucvr  30346  omssubadd  30362  carsggect  30380  cvmscld  31255  fnemeet1  32361  fnejoin1  32363  onsucsuccmpi  32442  heibor1  33609  heiborlem10  33619  hbt  37700  caragenuni  40725  caragendifcl  40728  cnfsmf  40949  smfsssmf  40952  smfpimbor1lem2  41006