Theorem unssd 3665

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	|- ( ph -> A C_ C )
unssd.2	|- ( ph -> B C_ C )

Assertion

Ref	Expression
unssd	|- ( ph -> ( A u. B ) C_ C )

Proof of Theorem unssd

Step	Hyp	Ref	Expression
1		unssd.1	. 2 |- ( ph -> A C_ C )
2		unssd.2	. 2 |- ( ph -> B C_ C )
3		unss 3663	. . 3 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
4	3	biimpi 194	. 2 |- ( ( A C_ C /\ B C_ C ) -> ( A u. B ) C_ C )
5	1, 2, 4	syl2anc 661	1 |- ( ph -> ( A u. B ) C_ C )

Syntax hints:   -> wi 4   /\ wa 369   u. cun 3459   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475

This theorem is referenced by:  tpssi  4181  sofld  5445  fr3nr  6600  suceloni  6633  ralxpmap  7470  marypha1lem  7895  wemapso2OLD  7980  wemapso2lem  7981  unwf  8231  rankunb  8271  ackbij1lem6  8608  ackbij1lem16  8618  ssfin4  8693  isfin1-3  8769  ttukeylem7  8898  fpwwe2lem13  9023  wuncval2  9128  inar1  9156  un0addcl  10835  un0mulcl  10836  fzosplit  11837  fzouzsplit  11839  hashf1lem1  12483  ccatrn  12585  saddisj  13992  prmreclem5  14315  4sqlem11  14350  4sqlem19  14358  vdwlem1  14376  vdwlem12  14387  ramub1lem1  14421  ramub1lem2  14422  mrieqvlemd  14903  mreexmrid  14917  mreexexlem2d  14919  mreexexlem3d  14920  mreexexlem4d  14921  acsfiindd  15681  tsrdir  15742  f1omvdco2  16347  symgsssg  16366  symggen  16369  lsmunss  16552  efgsfo  16631  gsumzaddlemOLD  16810  lsptpcl  17499  lspun  17507  lsmsp  17606  lspsolvlem  17662  lspsolv  17663  lsppratlem3  17669  lsppratlem4  17670  islbs3  17675  lbsextlem4  17681  aspval2  17870  evlseu  18059  clslp  19522  neitr  19554  ordtuni  19564  ordtbas2  19565  ordtbas  19566  ordtrest  19576  cmpcld  19775  comppfsc  19906  1stckgenlem  19927  1stckgen  19928  ptbasfi  19955  fbun  20214  trfil2  20261  isufil2  20282  ufileu  20293  filufint  20294  fmfnfm  20332  hausflim  20355  flimclslem  20358  fclsfnflim  20401  flimfnfcls  20402  alexsubALTlem3  20422  alexsubALTlem4  20423  tsmsgsum  20510  tsmsgsumOLD  20513  tsmsresOLD  20518  tsmsres  20519  tsmsxplem1  20528  ustund  20597  trust  20605  ustuqtop1  20617  prdsdsf  20743  prdsxmetlem  20744  prdsmet  20746  prdsbl  20867  prdsxmslem2  20905  restmetu  20963  icccmplem2  21201  rrxmval  21705  rrxmet  21708  rrxdstprj1  21709  ovolunlem1  21781  ovolunnul  21784  nulmbl2  21820  volun  21828  volcn  21888  itgsplitioo  22117  limcvallem  22148  limcdif  22153  ellimc2  22154  limcres  22163  limccnp  22168  limccnp2  22169  limcco  22170  dvreslem  22186  dvres2lem  22187  dvaddbr  22214  dvmulbr  22215  lhop2  22289  dvcnvrelem2  22292  elply2  22466  plyf  22468  elplyr  22471  elplyd  22472  ply1term  22474  ply0  22478  plyeq0lem  22480  plyeq0  22481  plyaddlem  22485  plymullem  22486  dgrlem  22499  coeidlem  22507  plyco  22511  plycj  22546  aannenlem2  22597  xrlimcnp  23170  perfectlem2  23377  shlej1  26150  shlub  26204  fcoinver  27332  ordtrestNEW  27776  eulerpartlemt  28183  erdszelem8  28515  mclsssvlem  28795  mclsax  28802  mclsind  28803  mthmpps  28815  mclsppslem  28816  relexpfld  28933  dftrpred3g  29291  ftc1anclem7  30071  ftc1anc  30073  topjoin  30158  prdsbnd  30264  rrnequiv  30306  elrfi  30601  cmpfiiin  30604  istopclsd  30607  mzpcompact2lem  30659  eldioph2lem2  30669  eldioph2  30670  rngunsnply  31098  idomsubgmo  31131  unima  31391  limciccioolb  31535  limcicciooub  31551  limcresiooub  31556  limcresioolb  31557  icccncfext  31597  fourierdlem20  31798  fourierdlem46  31824  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem51  31829  fourierdlem54  31832  fourierdlem64  31842  fourierdlem76  31854  fourierdlem101  31879  fourierdlem102  31880  fourierdlem103  31881  fourierdlem104  31882  fourierdlem114  31892  bnj1136  33786  bnj1452  33841  pclfinN  35364  dochdmj1  36857  djhspss  36873  djhunssN  36876  djhlsmcl  36881  dvh4dimlem  36910  dvhdimlem  36911  lclkrlem2c  36976  lclkrlem2v  36995  mapdh9a  37257  hdmapval0  37303  hdmapval3lemN  37307  hdmap10lem  37309