Theorem unissd 4922

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

Syntax hints:   → wi 4   ⊆ wss 3963  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913

This theorem is referenced by:  unieq  4923  dffv2  7004  onfununi  8380  fiuni  9466  dfac2a  10168  incexc  15870  incexc2  15871  isacs1i  17702  isacs3lem  18600  acsmapd  18612  acsmap2d  18613  dprdres  20063  dprd2da  20077  eltg3i  22984  unitg  22990  tgss  22991  tgcmp  23425  cmpfi  23432  alexsubALTlem4  24074  ptcmplem3  24078  ustbas2  24250  uniioombllem3  25634  madess  27930  shsupunss  31375  locfinref  33802  cmpcref  33811  dya2iocucvr  34266  omssubadd  34282  carsggect  34300  carsgclctun  34303  cvmscld  35258  fnemeet1  36349  fnejoin1  36351  onsucsuccmpi  36426  heibor1  37797  heiborlem10  37807  hbt  43119  pwsal  46271  prsal  46274  intsaluni  46285  caragenuni  46467  caragendifcl  46470  cnfsmf  46696  smfsssmf  46699  smfpimbor1lem2  46755  toplatglb  48790  setrecsss  48932