Theorem unssd 3520

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 3518	. . 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 654	1 |- ( ph -> ( A u. B ) C_ C )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330

This theorem is referenced by:  tpssi  4027  sofld  5274  fr3nr  6380  suceloni  6413  ralxpmap  7250  marypha1lem  7671  wemapso2OLD  7754  wemapso2lem  7755  unwf  8005  rankunb  8045  ackbij1lem6  8382  ackbij1lem16  8392  ssfin4  8467  isfin1-3  8543  ttukeylem7  8672  fpwwe2lem13  8797  wuncval2  8902  inar1  8930  un0addcl  10601  un0mulcl  10602  fzosplit  11566  fzouzsplit  11568  hashf1lem1  12192  saddisj  13644  prmreclem5  13964  4sqlem11  13999  4sqlem19  14007  vdwlem1  14025  vdwlem12  14036  ramub1lem1  14070  ramub1lem2  14071  mrieqvlemd  14550  mreexmrid  14564  mreexexlem2d  14566  mreexexlem3d  14567  mreexexlem4d  14568  acsfiindd  15330  tsrdir  15391  f1omvdco2  15934  symgsssg  15953  symggen  15956  lsmunss  16137  efgsfo  16216  gsumzaddlemOLD  16390  lsptpcl  16982  lspun  16990  lsmsp  17089  lspsolvlem  17145  lspsolv  17146  lsppratlem3  17152  lsppratlem4  17153  islbs3  17158  lbsextlem4  17164  aspval2  17339  clslp  18594  neitr  18626  ordtuni  18636  ordtbas2  18637  ordtbas  18638  ordtrest  18648  cmpcld  18847  1stckgenlem  18968  1stckgen  18969  ptbasfi  18996  fbun  19255  trfil2  19302  isufil2  19323  ufileu  19334  filufint  19335  fmfnfm  19373  hausflim  19396  flimclslem  19399  fclsfnflim  19442  flimfnfcls  19443  alexsubALTlem3  19463  alexsubALTlem4  19464  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmsxplem1  19569  ustund  19638  trust  19646  ustuqtop1  19658  prdsdsf  19784  prdsxmetlem  19785  prdsmet  19787  prdsbl  19908  prdsxmslem2  19946  restmetu  20004  icccmplem2  20242  rrxmval  20746  rrxmet  20749  rrxdstprj1  20750  ovolunlem1  20822  ovolunnul  20825  nulmbl2  20860  volun  20868  volcn  20928  itgsplitioo  21157  limcvallem  21188  limcdif  21193  ellimc2  21194  limcres  21203  limccnp  21208  limccnp2  21209  limcco  21210  dvreslem  21226  dvres2lem  21227  dvaddbr  21254  dvmulbr  21255  lhop2  21329  dvcnvrelem2  21332  evlseu  21368  elply2  21549  plyf  21551  elplyr  21554  elplyd  21555  ply1term  21557  ply0  21561  plyeq0lem  21563  plyeq0  21564  plyaddlem  21568  plymullem  21569  dgrlem  21582  coeidlem  21590  plyco  21594  plycj  21629  aannenlem2  21680  xrlimcnp  22247  perfectlem2  22454  shlej1  24586  shlub  24640  ordtrestNEW  26205  eulerpartlemt  26602  erdszelem8  26934  relexpfld  27186  dftrpred3g  27544  ftc1anclem7  28317  ftc1anc  28319  comppfsc  28423  topjoin  28430  prdsbnd  28536  rrnequiv  28578  elrfi  28875  cmpfiiin  28878  istopclsd  28881  mzpcompact2lem  28933  eldioph2lem2  28944  eldioph2  28945  rngunsnply  29375  idomsubgmo  29408  bnj1136  31711  bnj1452  31766  pclfinN  33138  dochdmj1  34629  djhspss  34645  djhunssN  34648  djhlsmcl  34653  dvh4dimlem  34682  dvhdimlem  34683  lclkrlem2c  34748  lclkrlem2v  34767  mapdh9a  35029  hdmapval0  35075  hdmapval3lemN  35079  hdmap10lem  35081