Theorem unssd 3621

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 3619	. . 3 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
4	3	biimpi 199	. 2 |- ( ( A C_ C /\ B C_ C ) -> ( A u. B ) C_ C )
5	1, 2, 4	syl2anc 671	1 |- ( ph -> ( A u. B ) C_ C )

Syntax hints:   -> wi 4   /\ wa 375   u. cun 3413   C_ wss 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-in 3422  df-ss 3429

This theorem is referenced by:  tpssi  4150  sofld  5302  fr3nr  6632  suceloni  6666  ralxpmap  7546  marypha1lem  7972  wemapso2lem  8092  unwf  8306  rankunb  8346  ackbij1lem6  8680  ackbij1lem16  8690  ssfin4  8765  isfin1-3  8841  ttukeylem7  8970  fpwwe2lem13  9092  wuncval2  9197  inar1  9225  un0addcl  10931  un0mulcl  10932  fzosplit  11981  fzouzsplit  11983  hashf1lem1  12650  ccatrn  12768  trclfvlb3  13123  trclun  13126  relexpfld  13160  saddisj  14487  lcmfunsnlem2lem1  14659  lcmfunsnlem2lem2  14660  lcmfunsnlem2  14661  lcmfun  14666  prmreclem5  14912  4sqlem11  14947  4sqlem19  14961  vdwlem1  14979  vdwlem12  14990  ramub1lem1  15032  ramub1lem2  15033  mrieqvlemd  15583  mreexmrid  15597  mreexexlem2d  15599  mreexexlem3d  15600  mreexexlem4d  15601  acsfiindd  16471  tsrdir  16532  f1omvdco2  17137  symgsssg  17156  symggen  17159  lsmunss  17358  efgsfo  17437  lsptpcl  18250  lspun  18258  lsmsp  18357  lspsolvlem  18413  lspsolv  18414  lsppratlem3  18420  lsppratlem4  18421  islbs3  18426  lbsextlem4  18432  aspval2  18619  evlseu  18787  clslp  20212  neitr  20244  ordtuni  20254  ordtbas2  20255  ordtbas  20256  ordtrest  20266  cmpcld  20465  comppfsc  20595  1stckgenlem  20616  1stckgen  20617  ptbasfi  20644  fbun  20903  trfil2  20950  isufil2  20971  ufileu  20982  filufint  20983  fmfnfm  21021  hausflim  21044  flimclslem  21047  fclsfnflim  21090  flimfnfcls  21091  alexsubALTlem3  21112  alexsubALTlem4  21113  tsmsgsum  21201  tsmsres  21206  tsmsxplem1  21215  ustund  21284  trust  21292  ustuqtop1  21304  prdsdsf  21430  prdsxmetlem  21431  prdsmet  21433  prdsbl  21554  prdsxmslem2  21592  restmetu  21633  icccmplem2  21889  rrxmval  22407  rrxmet  22410  rrxdstprj1  22411  ovolunlem1  22498  ovolunnul  22501  nulmbl2  22538  volun  22546  volcn  22612  itgsplitioo  22843  limcvallem  22874  limcdif  22879  ellimc2  22880  limcres  22889  limccnp  22894  limccnp2  22895  limcco  22896  dvreslem  22912  dvres2lem  22913  dvaddbr  22940  dvmulbr  22941  lhop2  23015  dvcnvrelem2  23018  elply2  23198  plyf  23200  elplyr  23203  elplyd  23204  ply1term  23206  ply0  23210  plyeq0lem  23212  plyeq0  23213  plyaddlem  23217  plymullem  23218  dgrlem  23231  coeidlem  23239  plyco  23243  plycj  23279  aannenlem2  23333  xrlimcnp  23942  perfectlem2  24206  shlej1  27061  shlub  27115  disjiunel  28254  fcoinver  28262  ordtrestNEW  28775  carsggect  29198  eulerpartlemt  29252  bnj1136  29854  bnj1452  29909  erdszelem8  29969  mclsssvlem  30248  mclsax  30255  mclsind  30256  mthmpps  30268  mclsppslem  30269  dftrpred3g  30522  topjoin  31069  poimirlem32  32016  ftc1anclem7  32067  ftc1anc  32069  prdsbnd  32169  rrnequiv  32211  pclfinN  33509  dochdmj1  35002  djhspss  35018  djhunssN  35021  djhlsmcl  35026  dvh4dimlem  35055  dvhdimlem  35056  lclkrlem2c  35121  lclkrlem2v  35140  mapdh9a  35402  hdmapval0  35448  hdmapval3lemN  35452  hdmap10lem  35454  elrfi  35580  cmpfiiin  35583  istopclsd  35586  mzpcompact2lem  35637  eldioph2lem2  35647  eldioph2  35648  rngunsnply  36083  idomsubgmo  36116  dfrcl2  36310  iunrelexp0  36338  relexp0a  36352  brtrclfv2  36363  frege77d  36382  frege109d  36393  frege131d  36400  unima  37466  mccllem  37714  limciccioolb  37738  limcicciooub  37754  limcresiooub  37760  limcresioolb  37761  icccncfext  37802  dvnprodlem2  37859  fourierdlem20  38026  fourierdlem46  38053  fourierdlem48  38055  fourierdlem49  38056  fourierdlem50  38057  fourierdlem51  38058  fourierdlem54  38061  fourierdlem64  38071  fourierdlem76  38083  fourierdlem101  38108  fourierdlem102  38109  fourierdlem103  38110  fourierdlem104  38111  fourierdlem114  38121  sge0resplit  38285  sge0xaddlem1  38312  ismeannd  38342  caragenuncl  38371  omeunle  38374  isomenndlem  38388  hoidmvlelem2  38455  hoidmvlelem3  38456  hoidmvlelem4  38457  perfectALTVlem2  38881