Theorem unssd 3535

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 3533	. . 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 3329   C_ wss 3331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-un 3336  df-in 3338  df-ss 3345

This theorem is referenced by:  tpssi  4042  sofld  5289  fr3nr  6394  suceloni  6427  ralxpmap  7265  marypha1lem  7686  wemapso2OLD  7769  wemapso2lem  7770  unwf  8020  rankunb  8060  ackbij1lem6  8397  ackbij1lem16  8407  ssfin4  8482  isfin1-3  8558  ttukeylem7  8687  fpwwe2lem13  8812  wuncval2  8917  inar1  8945  un0addcl  10616  un0mulcl  10617  fzosplit  11585  fzouzsplit  11587  hashf1lem1  12211  saddisj  13664  prmreclem5  13984  4sqlem11  14019  4sqlem19  14027  vdwlem1  14045  vdwlem12  14056  ramub1lem1  14090  ramub1lem2  14091  mrieqvlemd  14570  mreexmrid  14584  mreexexlem2d  14586  mreexexlem3d  14587  mreexexlem4d  14588  acsfiindd  15350  tsrdir  15411  f1omvdco2  15957  symgsssg  15976  symggen  15979  lsmunss  16160  efgsfo  16239  gsumzaddlemOLD  16413  lsptpcl  17063  lspun  17071  lsmsp  17170  lspsolvlem  17226  lspsolv  17227  lsppratlem3  17233  lsppratlem4  17234  islbs3  17239  lbsextlem4  17245  aspval2  17420  evlseu  17605  clslp  18755  neitr  18787  ordtuni  18797  ordtbas2  18798  ordtbas  18799  ordtrest  18809  cmpcld  19008  1stckgenlem  19129  1stckgen  19130  ptbasfi  19157  fbun  19416  trfil2  19463  isufil2  19484  ufileu  19495  filufint  19496  fmfnfm  19534  hausflim  19557  flimclslem  19560  fclsfnflim  19603  flimfnfcls  19604  alexsubALTlem3  19624  alexsubALTlem4  19625  tsmsgsum  19712  tsmsgsumOLD  19715  tsmsresOLD  19720  tsmsres  19721  tsmsxplem1  19730  ustund  19799  trust  19807  ustuqtop1  19819  prdsdsf  19945  prdsxmetlem  19946  prdsmet  19948  prdsbl  20069  prdsxmslem2  20107  restmetu  20165  icccmplem2  20403  rrxmval  20907  rrxmet  20910  rrxdstprj1  20911  ovolunlem1  20983  ovolunnul  20986  nulmbl2  21021  volun  21029  volcn  21089  itgsplitioo  21318  limcvallem  21349  limcdif  21354  ellimc2  21355  limcres  21364  limccnp  21369  limccnp2  21370  limcco  21371  dvreslem  21387  dvres2lem  21388  dvaddbr  21415  dvmulbr  21416  lhop2  21490  dvcnvrelem2  21493  elply2  21667  plyf  21669  elplyr  21672  elplyd  21673  ply1term  21675  ply0  21679  plyeq0lem  21681  plyeq0  21682  plyaddlem  21686  plymullem  21687  dgrlem  21700  coeidlem  21708  plyco  21712  plycj  21747  aannenlem2  21798  xrlimcnp  22365  perfectlem2  22572  shlej1  24766  shlub  24820  ordtrestNEW  26354  eulerpartlemt  26757  erdszelem8  27089  relexpfld  27342  dftrpred3g  27700  ftc1anclem7  28476  ftc1anc  28478  comppfsc  28582  topjoin  28589  prdsbnd  28695  rrnequiv  28737  elrfi  29033  cmpfiiin  29036  istopclsd  29039  mzpcompact2lem  29091  eldioph2lem2  29102  eldioph2  29103  rngunsnply  29533  idomsubgmo  29566  bnj1136  31991  bnj1452  32046  pclfinN  33547  dochdmj1  35038  djhspss  35054  djhunssN  35057  djhlsmcl  35062  dvh4dimlem  35091  dvhdimlem  35092  lclkrlem2c  35157  lclkrlem2v  35176  mapdh9a  35438  hdmapval0  35484  hdmapval3lemN  35488  hdmap10lem  35490