Theorem syl6eleq 2559

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl6eleq.1	|- ( ph -> A e. B )
syl6eleq.2	|- B = C

Assertion

Ref	Expression
syl6eleq	|- ( ph -> A e. C )

Proof of Theorem syl6eleq

Step	Hyp	Ref	Expression
1		syl6eleq.1	. 2 |- ( ph -> A e. B )
2		syl6eleq.2	. . 3 |- B = C
3	2	a1i 11	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2551	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1452   e. wcel 1904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-cleq 2464  df-clel 2467

This theorem is referenced by:  syl6eleqr  2560  3eltr3g  2565  prid2g  4070  ndmfvrcl  5904  fnwelem  6930  tz7.48-1  7178  brwitnlem  7227  oeeulem  7320  dffi3  7963  cnfcom3lem  8226  alephgeom  8531  fpwwe2lem6  9078  canthwelem  9093  hargch  9116  r1wunlim  9180  eluzel2  11187  fseq1p1m1  11894  fznn0sub2  11923  nn0split  11931  fz1fzo0m1  11991  exple1  12370  digit1  12444  bcval5  12541  bcpasc  12544  hashf1  12661  seqcoll  12668  seqcoll2  12669  ccatrn  12784  swrdccat1  12867  swrdccat2  12868  cats1un  12886  splfv2a  12917  splval2  12918  caubnd  13498  limsupgre  13619  limsupgreOLD  13620  clim2ser  13795  clim2ser2  13796  iserex  13797  isermulc2  13798  iserle  13800  iserge0  13801  climub  13802  climserle  13803  isercolllem2  13806  isercolllem3  13807  isercoll  13808  isercoll2  13809  serf0  13824  iseraltlem2  13826  iseraltlem3  13827  iseralt  13828  sumeq2ii  13836  summolem3  13857  summolem2a  13858  fsum  13863  sum0  13864  fsumcl2lem  13874  fsumadd  13882  isumclim3  13897  isumadd  13905  fsump1i  13907  fsummulc2  13922  fsumrelem  13944  iserabs  13952  cvgcmp  13953  cvgcmpub  13954  cvgcmpce  13955  binom1dif  13968  isumshft  13974  isumsplit  13975  isumrpcl  13978  isumsup2  13981  climcndslem1  13984  climcndslem2  13985  climcnds  13986  arisum2  13996  trireciplem  13997  geoser  14002  geolim  14003  geo2lim  14008  cvgrat  14016  mertenslem1  14017  mertenslem2  14018  mertens  14019  clim2prod  14021  clim2div  14022  ntrivcvgfvn0  14032  ntrivcvgtail  14033  prodeq2ii  14044  prodmolem3  14064  prodmolem2a  14065  fprod  14072  fprodntriv  14073  fprodss  14079  fprodser  14080  fprodcl2lem  14081  fprodmul  14091  fproddiv  14092  fprodabs  14105  fprodeq0  14106  fprodn0  14110  iprodclim3  14130  iprodmul  14133  fallfacfwd  14166  0fallfac  14167  binomfallfaclem2  14170  fallfacval4  14173  bpolysum  14183  bpolydiflem  14184  fsumkthpow  14186  efcvgfsum  14217  efcj  14223  fprodefsum  14226  effsumlt  14242  ruclem7  14365  bitsfzolem  14486  bitsfzolemOLD  14487  bitsfzo  14488  bitsfi  14490  bitsinv1lem  14494  bitsinv1  14495  bitsinvp1  14502  sadcp1  14508  sadadd  14520  sadass  14524  bitsres  14526  smupp1  14533  smuval2  14535  smupval  14541  smueqlem  14543  smumul  14546  algrp1  14612  phiprmpw  14803  crt  14805  phimullem  14806  eulerthlem2  14809  prmdiv  14812  pcpremul  14872  pcmpt  14916  pcfac  14923  pockthlem  14928  pockthg  14929  prmreclem2  14940  prmreclem3  14941  prmreclem4  14942  prmreclem5  14943  prmreclem6  14944  prmrec  14945  1arith  14950  vdwapun  15003  vdwlem1  15010  vdwlem2  15011  vdwlem3  15012  vdwlem6  15015  vdwlem8  15017  vdwlem10  15019  vdw  15023  imasvscafn  15521  xpsfrnel2  15549  oppccatid  15702  oppccomfpropd  15710  brcic  15781  funcoppc  15858  invfuc  15957  hofcl  16222  yonedalem4c  16240  gsumwsubmcl  16700  gsumccat  16703  gsumwmhm  16707  mulgnnp1  16844  mulgnnsubcl  16848  mulgnn0z  16856  mulgnndir  16858  psgnunilem4  17216  psgnran  17234  sylow1lem1  17328  lsmmod2  17404  lsmdisj2r  17413  efginvrel2  17455  efgsdmi  17460  efgsrel  17462  efgs1b  17464  efgsp1  17465  efgredleme  17471  efgredlemc  17473  efgcpbllemb  17483  frgpuplem  17500  mulgnn0di  17544  frgpnabllem1  17587  lt6abl  17607  cycsubgcyg  17613  gsumval3eu  17616  gsumval3  17619  gsumzcl2  17622  gsumzaddlem  17632  gsumconst  17645  gsumzmhm  17648  gsumzoppg  17655  telgsumfz0s  17699  dprdwd  17721  dprd2da  17753  pgpfaclem1  17792  srgbinom  17856  isirred  18005  lspprid2  18299  lspsnat  18446  lsppratlem1  18448  lsppratlem3  18450  lidl0cl  18513  lidlacl  18514  lidlnegcl  18515  lidlmcl  18518  psrbaglefi  18673  psrass23l  18709  psrass23  18711  mplcoe5lem  18768  mpfind  18836  psr1bascl  18870  ply1basf  18872  gsummoncoe1  18975  lply1binom  18977  lply1binomsc  18978  mpfpf1  19016  pf1mpf  19017  evl1scvarpw  19028  psgnghm  19225  matbas2i  19524  matecld  19528  matgsum  19539  mpt2matmul  19548  dmatmul  19599  1mavmul  19650  mdetleib2  19690  m1detdiag  19699  marep01ma  19762  smadiadetlem4  19771  slesolinv  19782  pmatcollpw3fi1lem1  19887  chpscmat  19943  chpscmatgsumbin  19945  chp0mat  19947  chpidmat  19948  chfacfisf  19955  chfacfisfcpmat  19956  chfacfpmmulgsum2  19966  cldrcl  20118  ordtbas  20285  iscnp2  20332  dis1stc  20591  ptbasfi  20673  ptpjopn  20704  ptclsg  20707  ptcnp  20714  kqtop  20837  reghmph  20885  ptcmplem2  21146  ptcmplem3  21147  ptcmplem4  21148  tsmslem1  21221  utop2nei  21343  isucn2  21372  cuspcvg  21394  cnextucn  21396  imasdsf1olem  21466  blcvx  21894  xrhmeo  22052  cnrehmeo  22059  evth  22065  reparphti  22106  iscau4  22327  iscmet3lem1  22339  lmle  22349  rrxfsupp  22434  pjthlem2  22470  ovollb2lem  22519  ovolunlem1a  22527  ovoliunlem1  22533  ovoliun2  22537  ovolscalem1  22544  ovolicc1  22547  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  iundisj2  22581  voliunlem1  22582  volsup  22588  ioombl1lem4  22593  uniioovol  22615  uniioombllem3  22622  uniioombllem4  22623  uniioombllem6  22625  vitalilem5  22649  mbfimaopnlem  22690  mbflimsup  22702  mbflimsupOLD  22703  mbfi1fseqlem3  22754  iblitg  22805  dvnp1  22958  cpncn  22969  dvlip2  23026  dvfsumlem2  23058  dvfsumlem3  23059  dvfsumrlimge0  23061  dvfsumrlim2  23063  ftc1cn  23074  elplyd  23235  ply1termlem  23236  ply1term  23237  ply0  23241  plyeq0lem  23243  plyaddlem1  23246  plymullem1  23247  plyaddlem  23248  plymullem  23249  coeeulem  23257  plyco  23274  coeeq2  23275  coefv0  23281  coemulhi  23287  coemulc  23288  plycj  23310  dvply1  23316  vieta1lem2  23343  elqaalem2  23352  elqaalem2OLD  23355  dvtaylp  23404  dvntaylp  23405  taylthlem1  23407  taylth  23409  ulmres  23422  ulmshftlem  23423  ulmshft  23424  ulmcau  23429  ulmdvlem1  23434  mtest  23438  mtestbdd  23439  pserulm  23456  psercn2  23457  psercnlem1  23459  psercn  23460  pserdvlem2  23462  abelthlem6  23470  abelth  23475  efif1olem1  23570  efif1olem3  23572  efif1olem4  23573  logcn  23671  advlogexp  23679  efopn  23682  cxpeq  23776  asinsin  23897  atantayl  23942  leibpilem2  23946  birthdaylem2  23957  birthdaylem3  23958  efrlim  23974  emcllem2  24001  emcllem5  24004  emcllem7  24006  harmonicbnd4  24015  fsumharmonic  24016  lgamgulm2  24040  lgamcvglem  24044  lgamcvg2  24059  gamcvg2lem  24063  wilthlem2  24073  wilthlem3  24074  ftalem1  24076  ftalem2  24077  ftalem3  24078  ftalem5  24080  ftalem5OLD  24082  basellem2  24087  basellem3  24088  basellem5  24090  basellem8  24093  ppiprm  24157  ppinprm  24158  chtprm  24159  chtnprm  24160  chpp1  24161  vma1  24172  ppiltx  24183  musum  24199  0sgmppw  24205  1sgmprm  24206  ppiublem2  24210  chtublem  24218  fsumvma2  24221  chpchtsum  24226  logexprlim  24232  bposlem5  24295  lgscllem  24310  lgsval2lem  24313  lgsval4a  24325  lgsneg  24326  lgsdir2lem3  24332  lgsdir2lem5  24334  lgsdir  24337  lgsdilem2  24338  lgsdi  24339  lgsne0  24340  lgseisenlem1  24356  lgsquadlem2  24362  chebbnd1lem1  24386  chtppilimlem1  24390  rplogsumlem2  24402  rpvmasumlem  24404  dchrisumlem1  24406  dchrisumlem2  24407  dchrmusum2  24411  dchrvmasum2lem  24413  dchrvmasumiflem1  24418  dchrisum0flblem1  24425  dchrisum0flblem2  24426  dchrisum0flb  24427  dchrisum0re  24430  dchrisum0lem1b  24432  dchrisum0lem1  24433  dchrisum0lem2a  24434  dchrisum0lem2  24435  dchrisum0lem3  24436  mudivsum  24447  mulogsum  24449  mulog2sumlem2  24452  selberg2lem  24467  logdivbnd  24473  pntrsumo1  24482  pntrsumbnd2  24484  pntrlog2bndlem2  24495  pntrlog2bndlem4  24497  pntrlog2bndlem6a  24499  pntlemj  24520  pntlemf  24522  ostth2lem3  24552  tglngne  24674  ltgseg  24720  eedimeq  25007  axlowdimlem16  25066  ebtwntg  25091  eupares  25782  eupap1  25783  eupath2lem3  25786  eupath2  25787  htthlem  26651  hhsscms  27011  shmodsi  27123  pjoc1i  27165  5oalem1  27388  mayete3i  27462  adj1  27667  iundisj2f  28277  fcnvgreu  28350  ssnnssfz  28442  iundisj2fi  28448  pmtrto1cl  28686  psgnfzto1stlem  28687  fzto1st1  28689  1smat1  28704  submateqlem2  28708  lmatfval  28714  mdetlap1  28726  madjusmdetlem1  28727  madjusmdetlem2  28728  madjusmdetlem3  28729  madjusmdetlem4  28730  pnfneige0  28831  pl1cn  28835  rrhqima  28892  indpreima  28920  esumfzf  28964  esumpcvgval  28973  esumpmono  28974  esumcvg  28981  ldgenpisyslem1  29059  ldgenpisys  29062  measbase  29093  dya2iocnei  29177  oddpwdc  29260  eulerpartlems  29266  eulerpartlemb  29274  sseqf  29298  fibp1  29307  orrvcval4  29370  orrvcoel  29371  orrvccel  29372  ballotlem2  29394  ballotlemfrceq  29434  ballotlemfrceqOLD  29472  signsplypnf  29511  signswch  29522  signstf0  29529  signstfvn  29530  signstfvneq0  29533  signstfvcl  29534  signstfveq0  29538  signsvfn  29543  bnj1172  29882  bnj1245  29895  bnj1311  29905  bnj1450  29931  bnj1501  29948  subfacp1lem1  29974  subfacp1lem5  29979  subfacp1lem6  29980  subfacval2  29982  erdszelem7  29992  cvxscon  30038  cvmliftlem5  30084  cvmliftlem7  30086  cvmliftlem10  30089  cvmliftlem13  30091  mrsubvrs  30232  msubrn  30239  msubco  30241  msubvrs  30270  bdayelon  30640  imageval  30768  fwddifnp1  31003  icoreunrn  31832  istoprelowl  31833  poimirlem3  32007  poimirlem4  32008  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem12  32016  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem23  32027  poimirlem24  32028  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem28  32032  poimirlem29  32033  poimirlem31  32035  mblfinlem2  32042  ftc1cnnc  32080  upixp  32120  sdclem2  32135  caushft  32154  ismtyres  32204  rrnmet  32225  rrndstprj1  32226  rrndstprj2  32227  rrncmslem  32228  rrnequiv  32231  iccbnd  32236  osumcllem7N  33598  pexmidlem4N  33609  lcfrlem4  35184  lcfrlem5  35185  lcfrlem6  35186  lcfrlem16  35197  lcfrlem38  35219  mapdrvallem2  35284  mapdh8ab  35416  mapdh8ad  35418  mapdh8e  35423  mapfzcons  35629  diophren  35727  irrapxlem1  35737  monotuz  35860  acongeq  35904  jm2.26lem3  35927  jm3.1lem2  35944  pw2f1ocnv  35963  idomodle  36141  trclfvdecomr  36391  imo72b2lem1  36685  dvgrat  36731  cvgdvgrat  36732  hashnzfz2  36740  fcnre  37409  refsumcn  37414  rfcnnnub  37420  disjf1o  37537  disjinfi  37539  ssmapsn  37569  ssuzfz  37659  nnsplit  37668  fsumsermpt  37754  climsuselem1  37783  limcperiod  37805  sumnnodd  37807  lptioo2cn  37823  lptioo1cn  37824  cncfshift  37848  cncfperiod  37853  cncfshiftioo  37867  fperdvper  37887  dvnmptdivc  37910  dvnmul  37915  dvmptfprod  37917  dvnprodlem3  37920  stoweidlem11  37983  stoweidlem15  37987  stoweidlem17  37989  stoweidlem20  37992  stoweidlem34  38007  stoweidlem35  38008  stoweidlem46  38019  stoweidlem47  38020  stoweidlem56  38029  stoweidlem59  38032  stoweidlem62  38035  stoweidlem62OLD  38036  stirlinglem5  38052  stirlinglem14  38061  dirkertrigeqlem2  38073  dirkertrigeqlem3  38074  fourierdlem11  38092  fourierdlem15  38096  fourierdlem16  38097  fourierdlem21  38102  fourierdlem22  38103  fourierdlem25  38106  fourierdlem48  38130  fourierdlem52  38134  fourierdlem54  38136  fourierdlem58  38140  fourierdlem62  38144  fourierdlem64  38146  fourierdlem65  38147  fourierdlem69  38151  fourierdlem70  38152  fourierdlem71  38153  fourierdlem73  38155  fourierdlem80  38162  fourierdlem81  38163  fourierdlem83  38165  fourierdlem92  38174  fourierdlem93  38175  fourierdlem97  38179  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  fourierdlem113  38195  fouriercnp  38202  fouriersw  38207  elaa2lem  38209  elaa2lemOLD  38210  etransclem4  38215  etransclem7  38218  etransclem10  38221  etransclem14  38225  etransclem15  38226  etransclem24  38235  etransclem25  38236  etransclem31  38242  etransclem32  38243  etransclem35  38246  etransclem44  38255  etransclem46  38257  qndenserrnopnlem  38278  qndenserrn  38280  prsal  38291  salgencntex  38314  sge0tsms  38336  sge0fodjrnlem  38372  sge0isum  38383  iundjiunlem  38413  iundjiun  38414  meadjiunlem  38419  meaiunlelem  38422  caragensplit  38440  carageneld  38442  carageniuncllem1  38461  caratheodorylem1  38466  caratheodorylem2  38467  hoicvr  38488  hsphoidmvle2  38525  hsphoidmvle  38526  hoidmv1lelem2  38532  hoidmv1lelem3  38533  hoidmvlelem2  38536  hoiqssbllem2  38563  elmod2  38869  subgruhgredgd  39520  subumgredg2  39521  umgrres1lem  39541  wlkson  39854  1wlksonproplem  39900  trlsonfval  39901  pthsonfval  39932  spthson  39933  crctcsh1wlkn0lem4  39991  crctcsh1wlkn0lem5  39992  eupth2lems  40150  ssnn0ssfz  40638  zlmodzxzscm  40646  rmsupp0  40661  lincsum  40730  lincscm  40731  lindslinindimp2lem4  40762  lincresunit3  40782  elbigofrcl  40869  aacllem  41046