Theorem unssd 3679

Description: A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
unssd.1
unssd.2

Assertion

Ref	Expression
unssd

Proof of Theorem unssd

Step	Hyp	Ref	Expression
1		unssd.1	. 2
2		unssd.2	. 2
3		unss 3677	. . 3
4	3	biimpi 194	. 2
5	1, 2, 4	syl2anc 661	1

Syntax hints:  ->wi 4  /\wa 369  u.cun 3473  C_wss 3475

This theorem is referenced by:  tpssi  4196  sofld  5460  fr3nr  6615  suceloni  6648  ralxpmap  7488  marypha1lem  7913  wemapso2OLD  7998  wemapso2lem  7999  unwf  8249  rankunb  8289  ackbij1lem6  8626  ackbij1lem16  8636  ssfin4  8711  isfin1-3  8787  ttukeylem7  8916  fpwwe2lem13  9041  wuncval2  9146  inar1  9174  un0addcl  10854  un0mulcl  10855  fzosplit  11858  fzouzsplit  11860  hashf1lem1  12504  ccatrn  12606  saddisj  14115  prmreclem5  14438  4sqlem11  14473  4sqlem19  14481  vdwlem1  14499  vdwlem12  14510  ramub1lem1  14544  ramub1lem2  14545  mrieqvlemd  15026  mreexmrid  15040  mreexexlem2d  15042  mreexexlem3d  15043  mreexexlem4d  15044  acsfiindd  15807  tsrdir  15868  f1omvdco2  16473  symgsssg  16492  symggen  16495  lsmunss  16678  efgsfo  16757  gsumzaddlemOLD  16936  lsptpcl  17625  lspun  17633  lsmsp  17732  lspsolvlem  17788  lspsolv  17789  lsppratlem3  17795  lsppratlem4  17796  islbs3  17801  lbsextlem4  17807  aspval2  17996  evlseu  18185  clslp  19649  neitr  19681  ordtuni  19691  ordtbas2  19692  ordtbas  19693  ordtrest  19703  cmpcld  19902  comppfsc  20033  1stckgenlem  20054  1stckgen  20055  ptbasfi  20082  fbun  20341  trfil2  20388  isufil2  20409  ufileu  20420  filufint  20421  fmfnfm  20459  hausflim  20482  flimclslem  20485  fclsfnflim  20528  flimfnfcls  20529  alexsubALTlem3  20549  alexsubALTlem4  20550  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  ustund  20724  trust  20732  ustuqtop1  20744  prdsdsf  20870  prdsxmetlem  20871  prdsmet  20873  prdsbl  20994  prdsxmslem2  21032  restmetu  21090  icccmplem2  21328  rrxmval  21832  rrxmet  21835  rrxdstprj1  21836  ovolunlem1  21908  ovolunnul  21911  nulmbl2  21947  volun  21955  volcn  22015  itgsplitioo  22244  limcvallem  22275  limcdif  22280  ellimc2  22281  limcres  22290  limccnp  22295  limccnp2  22296  limcco  22297  dvreslem  22313  dvres2lem  22314  dvaddbr  22341  dvmulbr  22342  lhop2  22416  dvcnvrelem2  22419  elply2  22593  plyf  22595  elplyr  22598  elplyd  22599  ply1term  22601  ply0  22605  plyeq0lem  22607  plyeq0  22608  plyaddlem  22612  plymullem  22613  dgrlem  22626  coeidlem  22634  plyco  22638  plycj  22674  aannenlem2  22725  xrlimcnp  23298  perfectlem2  23505  shlej1  26278  shlub  26332  fcoinver  27460  ordtrestNEW  27903  eulerpartlemt  28310  erdszelem8  28642  mclsssvlem  28922  mclsax  28929  mclsind  28930  mthmpps  28942  mclsppslem  28943  relexpfld  29060  dftrpred3g  29316  ftc1anclem7  30096  ftc1anc  30098  topjoin  30183  prdsbnd  30289  rrnequiv  30331  elrfi  30626  cmpfiiin  30629  istopclsd  30632  mzpcompact2lem  30684  eldioph2lem2  30694  eldioph2  30695  rngunsnply  31122  idomsubgmo  31155  unima  31441  mccllem  31605  limciccioolb  31627  limcicciooub  31643  limcresiooub  31648  limcresioolb  31649  icccncfext  31690  dvnprodlem2  31744  fourierdlem20  31909  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem54  31943  fourierdlem64  31953  fourierdlem76  31965  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003  bnj1136  34053  bnj1452  34108  pclfinN  35624  dochdmj1  37117  djhspss  37133  djhunssN  37136  djhlsmcl  37141  dvh4dimlem  37170  dvhdimlem  37171  lclkrlem2c  37236  lclkrlem2v  37255  mapdh9a  37517  hdmapval0  37563  hdmapval3lemN  37567  hdmap10lem  37569

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-or 370  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-un 3480  df-in 3482  df-ss 3489