Theorem unssd 3789

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

Syntax hints:   -> wi 4   /\ wa 384   u. cun 3572   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  uneqdifeq  4057  tpssi  4369  sofld  5581  fr3nr  6979  suceloni  7013  ralxpmap  7907  marypha1lem  8339  wemapso2lem  8457  unwf  8673  rankunb  8713  ackbij1lem6  9047  ackbij1lem16  9057  ssfin4  9132  isfin1-3  9208  ttukeylem7  9337  fpwwe2lem13  9464  wuncval2  9569  inar1  9597  un0addcl  11326  un0mulcl  11327  ssfzunsnext  12386  fzosplit  12501  fzouzsplit  12503  hashf1lem1  13239  ccatrn  13372  trclfvlb3  13752  trclun  13755  relexpfld  13789  saddisj  15187  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  lcmfun  15358  prmreclem5  15624  4sqlem11  15659  4sqlem19  15667  vdwlem1  15685  vdwlem12  15696  ramub1lem1  15730  ramub1lem2  15731  mrieqvlemd  16289  mreexmrid  16303  mreexexlem2d  16305  mreexexlem3d  16306  mreexexlem4d  16307  acsfiindd  17177  tsrdir  17238  f1omvdco2  17868  symgsssg  17887  symggen  17890  lsmunss  18073  efgsfo  18152  lsptpcl  18979  lspun  18987  lsmsp  19086  lspsolvlem  19142  lspsolv  19143  lsppratlem3  19149  lsppratlem4  19150  islbs3  19155  lbsextlem4  19161  aspval2  19347  evlseu  19516  clslp  20952  neitr  20984  ordtuni  20994  ordtbas2  20995  ordtbas  20996  ordtrest  21006  cmpcld  21205  comppfsc  21335  1stckgenlem  21356  1stckgen  21357  ptbasfi  21384  fbun  21644  trfil2  21691  isufil2  21712  ufileu  21723  filufint  21724  fmfnfm  21762  hausflim  21785  flimclslem  21788  fclsfnflim  21831  flimfnfcls  21832  alexsubALTlem3  21853  alexsubALTlem4  21854  tsmsgsum  21942  tsmsres  21947  tsmsxplem1  21956  ustund  22025  trust  22033  ustuqtop1  22045  prdsdsf  22172  prdsxmetlem  22173  prdsmet  22175  prdsbl  22296  prdsxmslem2  22334  restmetu  22375  icccmplem2  22626  rrxmval  23188  rrxmet  23191  rrxdstprj1  23192  ovolunlem1  23265  ovolunnul  23268  nulmbl2  23304  volun  23313  volcn  23374  itgsplitioo  23604  limcvallem  23635  limcdif  23640  ellimc2  23641  limcres  23650  limccnp  23655  limccnp2  23656  limcco  23657  dvreslem  23673  dvres2lem  23674  dvaddbr  23701  dvmulbr  23702  lhop2  23778  dvcnvrelem2  23781  elply2  23952  plyf  23954  elplyr  23957  elplyd  23958  ply1term  23960  ply0  23964  plyeq0lem  23966  plyeq0  23967  plyaddlem  23971  plymullem  23972  dgrlem  23985  coeidlem  23993  plyco  23997  plycj  24033  aannenlem2  24084  xrlimcnp  24695  perfectlem2  24955  shlej1  28219  shlub  28273  disjiunel  29409  fcoinver  29418  ordtrestNEW  29967  carsggect  30380  eulerpartlemt  30433  hgt750lemb  30734  hgt750leme  30736  bnj1136  31065  bnj1452  31120  erdszelem8  31180  mclsssvlem  31459  mclsax  31466  mclsind  31467  mthmpps  31479  mclsppslem  31480  dftrpred3g  31733  noextend  31819  ssltun1  31915  ssltun2  31916  topjoin  32360  poimirlem32  33441  ftc1anclem7  33491  ftc1anc  33493  prdsbnd  33592  rrnequiv  33634  pclfinN  35186  dochdmj1  36679  djhspss  36695  djhunssN  36698  djhlsmcl  36703  dvh4dimlem  36732  dvhdimlem  36733  lclkrlem2c  36798  lclkrlem2v  36817  mapdh9a  37079  hdmapval0  37125  hdmapval3lemN  37129  hdmap10lem  37131  elrfi  37257  cmpfiiin  37260  istopclsd  37263  mzpcompact2lem  37314  eldioph2lem2  37324  eldioph2  37325  rngunsnply  37743  idomsubgmo  37776  dfrcl2  37966  iunrelexp0  37994  relexp0a  38008  brtrclfv2  38019  frege77d  38038  frege109d  38049  frege131d  38056  clsk3nimkb  38338  isotone1  38346  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrneixb  38393  ntrneix3  38395  ntrneix13  38397  unima  39346  infxrpnf  39674  mccllem  39829  limciccioolb  39853  limcicciooub  39869  limcresiooub  39874  limcresioolb  39875  icccncfext  40100  dvnprodlem2  40162  ovolsplit  40205  fourierdlem20  40344  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem54  40377  fourierdlem64  40387  fourierdlem76  40399  fourierdlem101  40424  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  sge0resplit  40623  sge0xaddlem1  40650  ismeannd  40684  caragenuncl  40727  omeunle  40730  isomenndlem  40744  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  perfectALTVlem2  41631