Theorem unssd 3585

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

Syntax hints:   -> wi 4   /\ wa 370   u. cun 3377   C_ wss 3379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-un 3384  df-in 3386  df-ss 3393

This theorem is referenced by:  tpssi  4109  sofld  5246  fr3nr  6564  suceloni  6598  ralxpmap  7476  marypha1lem  7900  wemapso2lem  8020  unwf  8233  rankunb  8273  ackbij1lem6  8606  ackbij1lem16  8616  ssfin4  8691  isfin1-3  8767  ttukeylem7  8896  fpwwe2lem13  9018  wuncval2  9123  inar1  9151  un0addcl  10854  un0mulcl  10855  fzosplit  11902  fzouzsplit  11904  hashf1lem1  12566  ccatrn  12681  trclfvlb3  13019  trclun  13022  relexpfld  13056  saddisj  14382  lcmfunsnlem2lem1  14554  lcmfunsnlem2lem2  14555  lcmfunsnlem2  14556  lcmfun  14561  prmreclem5  14807  4sqlem11  14842  4sqlem19  14856  vdwlem1  14874  vdwlem12  14885  ramub1lem1  14927  ramub1lem2  14928  mrieqvlemd  15478  mreexmrid  15492  mreexexlem2d  15494  mreexexlem3d  15495  mreexexlem4d  15496  acsfiindd  16366  tsrdir  16427  f1omvdco2  17032  symgsssg  17051  symggen  17054  lsmunss  17253  efgsfo  17332  lsptpcl  18145  lspun  18153  lsmsp  18252  lspsolvlem  18308  lspsolv  18309  lsppratlem3  18315  lsppratlem4  18316  islbs3  18321  lbsextlem4  18327  aspval2  18514  evlseu  18682  clslp  20106  neitr  20138  ordtuni  20148  ordtbas2  20149  ordtbas  20150  ordtrest  20160  cmpcld  20359  comppfsc  20489  1stckgenlem  20510  1stckgen  20511  ptbasfi  20538  fbun  20797  trfil2  20844  isufil2  20865  ufileu  20876  filufint  20877  fmfnfm  20915  hausflim  20938  flimclslem  20941  fclsfnflim  20984  flimfnfcls  20985  alexsubALTlem3  21006  alexsubALTlem4  21007  tsmsgsum  21095  tsmsres  21100  tsmsxplem1  21109  ustund  21178  trust  21186  ustuqtop1  21198  prdsdsf  21324  prdsxmetlem  21325  prdsmet  21327  prdsbl  21448  prdsxmslem2  21486  restmetu  21527  icccmplem2  21783  rrxmval  22301  rrxmet  22304  rrxdstprj1  22305  ovolunlem1  22392  ovolunnul  22395  nulmbl2  22432  volun  22440  volcn  22506  itgsplitioo  22737  limcvallem  22768  limcdif  22773  ellimc2  22774  limcres  22783  limccnp  22788  limccnp2  22789  limcco  22790  dvreslem  22806  dvres2lem  22807  dvaddbr  22834  dvmulbr  22835  lhop2  22909  dvcnvrelem2  22912  elply2  23092  plyf  23094  elplyr  23097  elplyd  23098  ply1term  23100  ply0  23104  plyeq0lem  23106  plyeq0  23107  plyaddlem  23111  plymullem  23112  dgrlem  23125  coeidlem  23133  plyco  23137  plycj  23173  aannenlem2  23227  xrlimcnp  23836  perfectlem2  24100  shlej1  26955  shlub  27009  disjiunel  28152  fcoinver  28160  ordtrestNEW  28679  carsggect  29102  eulerpartlemt  29156  bnj1136  29758  bnj1452  29813  erdszelem8  29873  mclsssvlem  30152  mclsax  30159  mclsind  30160  mthmpps  30172  mclsppslem  30173  dftrpred3g  30425  topjoin  30970  poimirlem32  31879  ftc1anclem7  31930  ftc1anc  31932  prdsbnd  32032  rrnequiv  32074  pclfinN  33377  dochdmj1  34870  djhspss  34886  djhunssN  34889  djhlsmcl  34894  dvh4dimlem  34923  dvhdimlem  34924  lclkrlem2c  34989  lclkrlem2v  35008  mapdh9a  35270  hdmapval0  35316  hdmapval3lemN  35320  hdmap10lem  35322  elrfi  35448  cmpfiiin  35451  istopclsd  35454  mzpcompact2lem  35505  eldioph2lem2  35515  eldioph2  35516  rngunsnply  35952  idomsubgmo  35985  dfrcl2  36179  iunrelexp0  36207  relexp0a  36221  brtrclfv2  36232  frege77d  36251  frege109d  36262  frege131d  36269  unima  37332  mccllem  37560  limciccioolb  37584  limcicciooub  37600  limcresiooub  37606  limcresioolb  37607  icccncfext  37648  dvnprodlem2  37705  fourierdlem20  37872  fourierdlem46  37899  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem51  37904  fourierdlem54  37907  fourierdlem64  37917  fourierdlem76  37929  fourierdlem101  37954  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem114  37967  sge0resplit  38099  sge0xaddlem1  38126  ismeannd  38156  caragenuncl  38185  omeunle  38188  isomenndlem  38202  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem4  38267  perfectALTVlem2  38657