Theorem unssd 3483

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

Syntax hints:   -> wi 4   /\ wa 359   u. cun 3278   C_ wss 3280

This theorem is referenced by:  tpssi  3925  fr3nr  4719  suceloni  4752  sofld  5277  marypha1lem  7396  wemapso2  7477  unwf  7692  rankunb  7732  ackbij1lem6  8061  ackbij1lem16  8071  ssfin4  8146  isfin1-3  8222  ttukeylem7  8351  fpwwe2lem13  8473  wuncval2  8578  inar1  8606  un0addcl  10209  un0mulcl  10210  fzosplit  11121  fzouzsplit  11123  hashf1lem1  11659  saddisj  12932  prmreclem5  13243  4sqlem11  13278  4sqlem19  13286  vdwlem1  13304  vdwlem12  13315  ramub1lem1  13349  ramub1lem2  13350  mrieqvlemd  13809  mreexmrid  13823  mreexexlem2d  13825  mreexexlem3d  13826  mreexexlem4d  13827  acsfiindd  14558  tsrdir  14638  lsmunss  15247  efgsfo  15326  gsumzaddlem  15481  lsptpcl  16010  lspun  16018  lsmsp  16113  lspsolvlem  16169  lspsolv  16170  lsppratlem3  16176  lsppratlem4  16177  islbs3  16182  lbsextlem4  16188  aspval2  16360  clslp  17166  neitr  17198  ordtuni  17208  ordtbas2  17209  ordtbas  17210  ordtrest  17220  cmpcld  17419  1stckgenlem  17538  1stckgen  17539  ptbasfi  17566  fbun  17825  trfil2  17872  isufil2  17893  ufileu  17904  filufint  17905  fmfnfm  17943  hausflim  17966  flimclslem  17969  fclsfnflim  18012  flimfnfcls  18013  alexsubALTlem3  18033  alexsubALTlem4  18034  tsmsgsum  18121  tsmsres  18126  tsmsxplem1  18135  ustund  18204  trust  18212  ustuqtop1  18224  prdsdsf  18350  prdsxmetlem  18351  prdsmet  18353  prdsbl  18474  prdsxmslem2  18512  restmetu  18570  icccmplem2  18807  ovolunlem1  19346  ovolunnul  19349  nulmbl2  19384  volun  19392  volcn  19451  itgsplitioo  19682  limcvallem  19711  limcdif  19716  ellimc2  19717  limcres  19726  limccnp  19731  limccnp2  19732  limcco  19733  dvreslem  19749  dvres2lem  19750  dvaddbr  19777  dvmulbr  19778  lhop2  19852  dvcnvrelem2  19855  evlseu  19890  elply2  20068  plyf  20070  elplyr  20073  elplyd  20074  ply1term  20076  ply0  20080  plyeq0lem  20082  plyeq0  20083  plyaddlem  20087  plymullem  20088  dgrlem  20101  coeidlem  20109  plyco  20113  plycj  20148  aannenlem2  20199  xrlimcnp  20760  perfectlem2  20967  shlej1  22815  shlub  22869  erdszelem8  24837  relexpfld  25090  dftrpred3g  25450  comppfsc  26277  topjoin  26284  prdsbnd  26392  rrnequiv  26434  ralxpmap  26632  elrfi  26638  cmpfiiin  26641  istopclsd  26644  mzpcompact2lem  26698  eldioph2lem2  26709  eldioph2  26710  rngunsnply  27246  f1omvdco2  27259  symgsssg  27276  symggen  27279  idomsubgmo  27382  bnj1136  29072  bnj1452  29127  pclfinN  30382  dochdmj1  31873  djhspss  31889  djhunssN  31892  djhlsmcl  31897  dvh4dimlem  31926  dvhdimlem  31927  lclkrlem2c  31992  lclkrlem2v  32011  mapdh9a  32273  hdmapval0  32319  hdmapval3lemN  32323  hdmap10lem  32325

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294