Theorem unssd 3673

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 3671	. . 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 3467   C_ wss 3469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-in 3476  df-ss 3483

This theorem is referenced by:  tpssi  4186  sofld  5446  fr3nr  6586  suceloni  6619  ralxpmap  7458  marypha1lem  7882  wemapso2OLD  7966  wemapso2lem  7967  unwf  8217  rankunb  8257  ackbij1lem6  8594  ackbij1lem16  8604  ssfin4  8679  isfin1-3  8755  ttukeylem7  8884  fpwwe2lem13  9009  wuncval2  9114  inar1  9142  un0addcl  10818  un0mulcl  10819  fzosplit  11815  fzouzsplit  11817  hashf1lem1  12457  saddisj  13963  prmreclem5  14286  4sqlem11  14321  4sqlem19  14329  vdwlem1  14347  vdwlem12  14358  ramub1lem1  14392  ramub1lem2  14393  mrieqvlemd  14873  mreexmrid  14887  mreexexlem2d  14889  mreexexlem3d  14890  mreexexlem4d  14891  acsfiindd  15653  tsrdir  15714  f1omvdco2  16262  symgsssg  16281  symggen  16284  lsmunss  16467  efgsfo  16546  gsumzaddlemOLD  16720  lsptpcl  17401  lspun  17409  lsmsp  17508  lspsolvlem  17564  lspsolv  17565  lsppratlem3  17571  lsppratlem4  17572  islbs3  17577  lbsextlem4  17583  aspval2  17760  evlseu  17949  clslp  19408  neitr  19440  ordtuni  19450  ordtbas2  19451  ordtbas  19452  ordtrest  19462  cmpcld  19661  1stckgenlem  19782  1stckgen  19783  ptbasfi  19810  fbun  20069  trfil2  20116  isufil2  20137  ufileu  20148  filufint  20149  fmfnfm  20187  hausflim  20210  flimclslem  20213  fclsfnflim  20256  flimfnfcls  20257  alexsubALTlem3  20277  alexsubALTlem4  20278  tsmsgsum  20365  tsmsgsumOLD  20368  tsmsresOLD  20373  tsmsres  20374  tsmsxplem1  20383  ustund  20452  trust  20460  ustuqtop1  20472  prdsdsf  20598  prdsxmetlem  20599  prdsmet  20601  prdsbl  20722  prdsxmslem2  20760  restmetu  20818  icccmplem2  21056  rrxmval  21560  rrxmet  21563  rrxdstprj1  21564  ovolunlem1  21636  ovolunnul  21639  nulmbl2  21675  volun  21683  volcn  21743  itgsplitioo  21972  limcvallem  22003  limcdif  22008  ellimc2  22009  limcres  22018  limccnp  22023  limccnp2  22024  limcco  22025  dvreslem  22041  dvres2lem  22042  dvaddbr  22069  dvmulbr  22070  lhop2  22144  dvcnvrelem2  22147  elply2  22321  plyf  22323  elplyr  22326  elplyd  22327  ply1term  22329  ply0  22333  plyeq0lem  22335  plyeq0  22336  plyaddlem  22340  plymullem  22341  dgrlem  22354  coeidlem  22362  plyco  22366  plycj  22401  aannenlem2  22452  xrlimcnp  23019  perfectlem2  23226  shlej1  25940  shlub  25994  ordtrestNEW  27525  eulerpartlemt  27936  erdszelem8  28268  relexpfld  28521  dftrpred3g  28879  ftc1anclem7  29660  ftc1anc  29662  comppfsc  29766  topjoin  29773  prdsbnd  29879  rrnequiv  29921  elrfi  30217  cmpfiiin  30220  istopclsd  30223  mzpcompact2lem  30275  eldioph2lem2  30285  eldioph2  30286  rngunsnply  30716  idomsubgmo  30749  unima  30974  limcresiooub  31139  limcresioolb  31140  icccncfext  31181  fourierdlem20  31382  fourierdlem46  31408  fourierdlem48  31410  fourierdlem49  31411  fourierdlem50  31412  fourierdlem51  31413  fourierdlem54  31416  fourierdlem64  31426  fourierdlem76  31438  fourierdlem102  31464  fourierdlem103  31465  fourierdlem104  31466  fourierdlem114  31476  bnj1136  33007  bnj1452  33062  pclfinN  34571  dochdmj1  36062  djhspss  36078  djhunssN  36081  djhlsmcl  36086  dvh4dimlem  36115  dvhdimlem  36116  lclkrlem2c  36181  lclkrlem2v  36200  mapdh9a  36462  hdmapval0  36508  hdmapval3lemN  36512  hdmap10lem  36514