Theorem unissd 4273

Description: Subclass relationship for subclass union. Deduction form of uniss 4270. (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 4270	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  C_wss 3475  U.cuni 4249

This theorem is referenced by:  dffv2  5946  onfununi  7031  fiuni  7908  dfac2a  8531  incexc  13649  incexc2  13650  isacs1i  15054  isacs3lem  15796  acsmapd  15808  acsmap2d  15809  dprdres  17075  dprd2da  17091  eltg3i  19462  unitg  19468  unitgOLD  19469  tgss  19470  tgcmp  19901  cmpfi  19908  alexsubALTlem4  20550  ptcmplem3  20554  ustbas2  20728  uniioombllem3  21994  shsupunss  26264  locfinref  27844  cmpcref  27853  dya2iocucvr  28255  cvmscld  28718  nofulllem3  29464  onsucsuccmpi  29908  fnemeet1  30184  fnejoin1  30186  heibor1  30306  heiborlem10  30316  hbt  31079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250