Theorem syl6eleq 2555

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 2547	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 1819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-cleq 2449  df-clel 2452

This theorem is referenced by:  syl6eleqr  2556  3eltr3g  2561  prid2g  4139  ndmfvrcl  5897  fnwelem  6914  tz7.48-1  7126  brwitnlem  7175  oeeulem  7268  dffi3  7909  cnfcom3lem  8164  cnfcom3lemOLD  8172  alephgeom  8480  fpwwe2lem6  9030  canthwelem  9045  hargch  9068  r1wunlim  9132  eluzel2  11111  fseq1p1m1  11777  fznn0sub2  11806  nn0split  11815  exple1  12227  digit1  12302  bcval5  12398  bcpasc  12401  hashf1  12509  seqcoll  12515  seqcoll2  12516  ccatrn  12614  swrdccat1  12693  swrdccat2  12694  cats1un  12712  splfv2a  12743  splval2  12744  caubnd  13202  limsupgre  13315  clim2ser  13488  clim2ser2  13489  iserex  13490  isermulc2  13491  iserle  13493  iserge0  13494  climub  13495  climserle  13496  isercolllem2  13499  isercolllem3  13500  isercoll  13501  isercoll2  13502  serf0  13514  iseraltlem2  13516  iseraltlem3  13517  iseralt  13518  sumeq2ii  13526  summolem3  13547  summolem2a  13548  fsum  13553  sum0  13554  fsumcl2lem  13564  fsumadd  13572  isumclim3  13585  isumadd  13593  fsump1i  13595  fsummulc2  13610  fsumrelem  13632  iserabs  13640  cvgcmp  13641  cvgcmpub  13642  cvgcmpce  13643  binom1dif  13656  isumshft  13662  isumsplit  13663  isumrpcl  13666  isumsup2  13669  climcndslem1  13672  climcndslem2  13673  climcnds  13674  arisum2  13683  trireciplem  13684  geoser  13689  geolim  13690  geo2lim  13695  cvgrat  13703  mertenslem1  13704  mertenslem2  13705  mertens  13706  clim2prod  13708  clim2div  13709  ntrivcvgfvn0  13719  ntrivcvgtail  13720  prodeq2ii  13731  prodmolem3  13751  prodmolem2a  13752  fprod  13759  fprodntriv  13760  fprodss  13766  fprodser  13767  fprodcl2lem  13768  fprodmul  13776  fproddiv  13777  fprodabs  13789  fprodeq0  13790  fprodn0  13794  iprodclim3  13804  iprodmul  13807  efcvgfsum  13832  efcj  13838  fprodefsum  13841  effsumlt  13857  ruclem7  13980  bitsfzolem  14095  bitsfzo  14096  bitsfi  14098  bitsinv1lem  14102  bitsinv1  14103  bitsinvp1  14110  sadcp1  14116  sadadd  14128  sadass  14132  bitsres  14134  smupp1  14141  smuval2  14143  smupval  14149  smueqlem  14151  smumul  14154  algrp1  14214  phiprmpw  14317  crt  14319  phimullem  14320  eulerthlem2  14323  prmdiv  14326  pcpremul  14378  pcmpt  14422  pcfac  14429  pockthlem  14434  pockthg  14435  prmreclem2  14446  prmreclem3  14447  prmreclem4  14448  prmreclem5  14449  prmreclem6  14450  prmrec  14451  1arith  14456  vdwapun  14503  vdwlem1  14510  vdwlem2  14511  vdwlem3  14512  vdwlem6  14515  vdwlem8  14517  vdwlem10  14519  vdw  14523  imasvscafn  14953  xpsfrnel2  14981  oppccatid  15134  oppccomfpropd  15142  brcic  15213  funcoppc  15290  invfuc  15389  hofcl  15654  yonedalem4c  15672  gsumwsubmcl  16132  gsumccat  16135  gsumwmhm  16139  mulgnnp1  16276  mulgnnsubcl  16280  mulgnn0z  16288  mulgnndir  16290  psgnunilem4  16648  psgnran  16666  sylow1lem1  16744  lsmmod2  16820  lsmdisj2r  16829  efginvrel2  16871  efgsdmi  16876  efgsrel  16878  efgs1b  16880  efgsp1  16881  efgredleme  16887  efgredlemc  16889  efgcpbllemb  16899  frgpuplem  16916  mulgnn0di  16960  frgpnabllem1  17003  lt6abl  17023  cycsubgcyg  17029  gsumval3eu  17033  gsumval3OLD  17034  gsumval3  17037  gsumzcl2  17041  gsumzclOLD  17045  gsumzaddlem  17060  gsumzaddlemOLD  17062  gsumconst  17080  gsumzmhm  17083  gsumzmhmOLD  17084  gsumzoppg  17093  gsumzoppgOLD  17094  telgsumfz0s  17146  dprdwd  17170  dprd2da  17217  pgpfaclem1  17258  srgbinom  17322  isirred  17474  lspprid2  17770  lspsnat  17917  lsppratlem1  17919  lsppratlem3  17921  lidl0cl  17985  lidlacl  17986  lidlnegcl  17987  lidlmcl  17991  psrbaglefi  18149  psrbaglefiOLD  18150  psrass23l  18189  psrass23  18191  mplcoe5lem  18256  mpfind  18331  psr1bascl  18365  ply1basf  18367  gsummoncoe1  18472  lply1binom  18474  lply1binomsc  18475  mpfpf1  18513  pf1mpf  18514  evl1scvarpw  18525  psgnghm  18742  matbas2i  19050  matecld  19054  matgsum  19065  mpt2matmul  19074  dmatmul  19125  1mavmul  19176  mdetleib2  19216  m1detdiag  19225  marep01ma  19288  smadiadetlem4  19297  slesolinv  19308  pmatcollpw3fi1lem1  19413  chpscmat  19469  chpscmatgsumbin  19471  chp0mat  19473  chpidmat  19474  chfacfisf  19481  chfacfisfcpmat  19482  chfacfpmmulgsum2  19492  cldrcl  19653  ordtbas  19819  iscnp2  19866  dis1stc  20125  ptbasfi  20207  ptpjopn  20238  ptclsg  20241  ptcnp  20248  kqtop  20371  reghmph  20419  ptcmplem2  20678  ptcmplem3  20679  ptcmplem4  20680  tsmslem1  20752  utop2nei  20878  isucn2  20907  cuspcvg  20929  cnextucn  20931  imasdsf1olem  21001  blcvx  21428  xrhmeo  21571  cnrehmeo  21578  evth  21584  reparphti  21622  iscau4  21843  iscmet3lem1  21855  lmle  21865  rrxfsupp  21954  pjthlem2  21978  ovollb2lem  22024  ovolunlem1a  22032  ovoliunlem1  22038  ovoliun2  22042  ovolscalem1  22049  ovolicc1  22052  ovolicc2lem4  22056  iundisj2  22084  voliunlem1  22085  volsup  22091  ioombl1lem4  22096  uniioovol  22113  uniioombllem3  22119  uniioombllem4  22120  uniioombllem6  22122  vitalilem5  22146  mbfimaopnlem  22187  mbflimsup  22198  mbfi1fseqlem3  22249  iblitg  22300  dvnp1  22453  cpncn  22464  dvlip2  22521  dvfsumlem2  22553  dvfsumlem3  22554  dvfsumrlimge0  22556  dvfsumrlim2  22558  ftc1cn  22569  elplyd  22724  ply1termlem  22725  ply1term  22726  ply0  22730  plyeq0lem  22732  plyaddlem1  22735  plymullem1  22736  plyaddlem  22737  plymullem  22738  coeeulem  22746  plyco  22763  coeeq2  22764  coefv0  22770  coemulhi  22776  coemulc  22777  plycj  22799  dvply1  22805  vieta1lem2  22832  elqaalem2  22841  dvtaylp  22890  dvntaylp  22891  taylthlem1  22893  taylth  22895  ulmres  22908  ulmshftlem  22909  ulmshft  22910  ulmcau  22915  ulmdvlem1  22920  mtest  22924  mtestbdd  22925  pserulm  22942  psercn2  22943  psercnlem1  22945  psercn  22946  pserdvlem2  22948  abelthlem6  22956  abelth  22961  efif1olem1  23054  efif1olem3  23056  efif1olem4  23057  logcn  23153  advlogexp  23161  efopn  23164  cxpeq  23256  asinsin  23348  atantayl  23393  leibpilem2  23397  birthdaylem2  23407  birthdaylem3  23408  efrlim  23424  emcllem2  23451  emcllem5  23454  emcllem7  23456  harmonicbnd4  23465  fsumharmonic  23466  wilthlem2  23468  wilthlem3  23469  ftalem1  23471  ftalem2  23472  ftalem3  23473  ftalem5  23475  basellem2  23480  basellem3  23481  basellem5  23483  basellem8  23486  ppiprm  23550  ppinprm  23551  chtprm  23552  chtnprm  23553  chpp1  23554  vma1  23565  ppiltx  23576  musum  23592  0sgmppw  23598  1sgmprm  23599  ppiublem2  23603  chtublem  23611  fsumvma2  23614  chpchtsum  23619  logexprlim  23625  bposlem5  23688  lgscllem  23703  lgsval2lem  23706  lgsval4a  23718  lgsneg  23719  lgsdir2lem3  23725  lgsdir2lem5  23727  lgsdir  23730  lgsdilem2  23731  lgsdi  23732  lgsne0  23733  lgseisenlem1  23749  lgsquadlem2  23755  chebbnd1lem1  23779  chtppilimlem1  23783  rplogsumlem2  23795  rpvmasumlem  23797  dchrisumlem1  23799  dchrisumlem2  23800  dchrmusum2  23804  dchrvmasum2lem  23806  dchrvmasumiflem1  23811  dchrisum0flblem1  23818  dchrisum0flblem2  23819  dchrisum0flb  23820  dchrisum0re  23823  dchrisum0lem1b  23825  dchrisum0lem1  23826  dchrisum0lem2a  23827  dchrisum0lem2  23828  dchrisum0lem3  23829  mudivsum  23840  mulogsum  23842  mulog2sumlem2  23845  selberg2lem  23860  logdivbnd  23866  pntrsumo1  23875  pntrsumbnd2  23877  pntrlog2bndlem2  23888  pntrlog2bndlem4  23890  pntrlog2bndlem6a  23892  pntlemj  23913  pntlemf  23915  ostth2lem3  23945  tglngne  24062  ltgseg  24107  eedimeq  24327  axlowdimlem16  24386  ebtwntg  24411  eupares  25101  eupap1  25102  eupath2lem3  25105  eupath2  25106  htthlem  25960  hhsscms  26321  shmodsi  26433  pjoc1i  26475  5oalem1  26698  mayete3i  26772  mayete3iOLD  26773  adj1  26978  iundisj2f  27586  fcnvgreu  27662  ssnnssfz  27749  iundisj2fi  27754  pnfneige0  28086  pl1cn  28090  indpreima  28191  esumfzf  28231  esumpcvgval  28240  esumpmono  28241  esumcvg  28248  measbase  28329  dya2iocnei  28414  oddpwdc  28468  eulerpartlems  28474  eulerpartlemb  28482  sseqf  28506  fibp1  28515  orrvcval4  28578  orrvcoel  28579  orrvccel  28580  ballotlem2  28602  ballotlemfrceq  28642  signsplypnf  28682  signswch  28693  signstf0  28700  signstfvn  28701  signstfvneq0  28704  signstfvcl  28705  signstfveq0  28709  signsvfn  28714  lgamgulm2  28753  lgamcvglem  28757  lgamcvg2  28772  gamcvg2lem  28776  subfacp1lem1  28798  subfacp1lem5  28803  subfacp1lem6  28804  subfacval2  28806  erdszelem7  28816  cvxscon  28863  cvmliftlem5  28909  cvmliftlem7  28911  cvmliftlem10  28914  cvmliftlem13  28916  mrsubvrs  29057  msubrn  29064  msubco  29066  msubvrs  29095  relexpsucr  29228  fallfacfwd  29333  0fallfac  29334  binomfallfaclem2  29337  fallfacval4  29340  bdayelon  29614  imageval  29742  bpolysum  29977  bpolydiflem  29978  fsumkthpow  29980  mblfinlem2  30214  ftc1cnnc  30251  upixp  30382  sdclem2  30397  caushft  30416  ismtyres  30466  rrnmet  30487  rrndstprj1  30488  rrndstprj2  30489  rrncmslem  30490  rrnequiv  30493  iccbnd  30498  mapfzcons  30810  diophren  30909  irrapxlem1  30920  monotuz  31039  acongeq  31083  jm2.26lem3  31105  jm3.1lem2  31122  pw2f1ocnv  31141  idomodle  31315  dvgrat  31355  cvgdvgrat  31356  hashnzfz2  31388  fcnre  31561  refsumcn  31566  rfcnnnub  31572  climsuselem1  31774  limcperiod  31795  sumnnodd  31797  lptioo2cn  31812  lptioo1cn  31813  cncfshift  31837  cncfperiod  31842  cncfshiftioo  31856  fperdvper  31876  dvnmptdivc  31896  dvnmul  31901  dvmptfprod  31903  dvnprodlem3  31906  stoweidlem11  31954  stoweidlem15  31958  stoweidlem17  31960  stoweidlem20  31963  stoweidlem34  31977  stoweidlem35  31978  stoweidlem46  31989  stoweidlem47  31990  stoweidlem56  31999  stoweidlem59  32002  stoweidlem62  32005  stirlinglem5  32021  stirlinglem14  32030  dirkertrigeqlem2  32042  dirkertrigeqlem3  32043  fourierdlem11  32061  fourierdlem15  32065  fourierdlem16  32066  fourierdlem21  32071  fourierdlem22  32072  fourierdlem25  32075  fourierdlem48  32098  fourierdlem52  32102  fourierdlem54  32104  fourierdlem58  32108  fourierdlem62  32112  fourierdlem64  32114  fourierdlem65  32115  fourierdlem69  32119  fourierdlem70  32120  fourierdlem71  32121  fourierdlem73  32123  fourierdlem80  32130  fourierdlem81  32131  fourierdlem83  32133  fourierdlem92  32142  fourierdlem93  32143  fourierdlem97  32147  fourierdlem103  32153  fourierdlem104  32154  fourierdlem112  32162  fourierdlem113  32163  fouriercnp  32170  fouriersw  32175  elaa2lem  32177  etransclem4  32182  etransclem7  32185  etransclem10  32188  etransclem14  32192  etransclem15  32193  etransclem24  32202  etransclem25  32203  etransclem31  32209  etransclem32  32210  etransclem35  32213  etransclem44  32222  etransclem46  32224  ssnn0ssfz  33040  zlmodzxzscm  33048  rmsupp0  33063  lincsum  33132  lincscm  33133  lindslinindimp2lem4  33164  lincresunit3  33184  aacllem  33318  bnj1172  34158  bnj1245  34171  bnj1311  34181  bnj1450  34207  bnj1501  34224  osumcllem7N  35787  pexmidlem4N  35798  lcfrlem4  37373  lcfrlem5  37374  lcfrlem6  37375  lcfrlem16  37386  lcfrlem38  37408  mapdrvallem2  37473  mapdh8ab  37605  mapdh8ad  37607  mapdh8e  37612  imo72b2lem1  38089