Theorem syl6eleq 2523

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  syl6eleqr  2524  prid2g  3970  ndmfvrcl  5703  fnwelem  6676  tz7.48-1  6884  brwitnlem  6935  oeeulem  7028  dffi3  7669  cnfcom3lem  7924  cnfcom3lemOLD  7932  alephgeom  8240  fpwwe2lem6  8790  canthwelem  8805  hargch  8828  r1wunlim  8892  eluzel2  10854  fznn0sub2  11475  fseq1p1m1  11518  exple1  11907  digit1  11982  bcval5  12078  bcpasc  12081  hashf1  12194  seqcoll  12200  seqcoll2  12201  swrdccat1  12335  swrdccat2  12336  cats1un  12354  splfv2a  12382  splval2  12383  caubnd  12830  limsupgre  12943  clim2ser  13116  clim2ser2  13117  iserex  13118  isermulc2  13119  iserle  13121  iserge0  13122  climub  13123  climserle  13124  isercolllem2  13127  isercolllem3  13128  isercoll  13129  isercoll2  13130  serf0  13142  iseraltlem2  13144  iseraltlem3  13145  iseralt  13146  sumeq2ii  13154  summolem3  13175  summolem2a  13176  fsum  13181  sum0  13182  fsumcl2lem  13192  fsumadd  13199  isumclim3  13210  isumadd  13218  fsump1i  13220  fsummulc2  13234  fsumrelem  13253  iserabs  13261  cvgcmp  13262  cvgcmpub  13263  cvgcmpce  13264  binom1dif  13279  isumshft  13285  isumsplit  13286  isumrpcl  13289  isumsup2  13292  climcndslem1  13295  climcndslem2  13296  climcnds  13297  arisum2  13306  trireciplem  13307  geoser  13312  geolim  13313  geo2lim  13318  cvgrat  13326  mertenslem1  13327  mertenslem2  13328  mertens  13329  efcvgfsum  13354  efcj  13360  effsumlt  13378  ruclem7  13501  bitsfzolem  13613  bitsfzo  13614  bitsfi  13616  bitsinv1lem  13620  bitsinv1  13621  bitsinvp1  13628  sadcp1  13634  sadadd  13646  sadass  13650  bitsres  13652  smupp1  13659  smuval2  13661  smupval  13667  smueqlem  13669  smumul  13672  algrp1  13732  phiprmpw  13834  crt  13836  phimullem  13837  eulerthlem2  13840  prmdiv  13843  pcpremul  13893  pcmpt  13937  pcfac  13944  pockthlem  13949  pockthg  13950  prmreclem2  13961  prmreclem3  13962  prmreclem4  13963  prmreclem5  13964  prmreclem6  13965  prmrec  13966  1arith  13971  vdwapun  14018  vdwlem1  14025  vdwlem2  14026  vdwlem3  14027  vdwlem6  14030  vdwlem8  14032  vdwlem10  14034  vdw  14038  imasvscafn  14458  xpsfrnel2  14486  oppccatid  14641  oppccomfpropd  14649  funcoppc  14768  invfuc  14867  hofcl  15052  yonedalem4c  15070  gsumwsubmcl  15496  gsumccat  15499  gsumwmhm  15503  mulgnnp1  15615  mulgnnsubcl  15619  mulgnn0z  15627  mulgnndir  15629  psgnunilem4  15983  psgnran  16001  sylow1lem1  16077  lsmmod2  16153  lsmdisj2r  16162  efginvrel2  16204  efgsdmi  16209  efgsrel  16211  efgs1b  16213  efgsp1  16214  efgredleme  16220  efgredlemc  16222  efgcpbllemb  16232  frgpuplem  16249  mulgnn0di  16293  frgpnabllem1  16331  lt6abl  16351  cycsubgcyg  16357  gsumval3eu  16361  gsumval3OLD  16362  gsumval3  16365  gsumzcl2  16369  gsumzclOLD  16373  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsumzoppg  16416  gsumzoppgOLD  16417  dprd2da  16515  pgpfaclem1  16556  isirred  16725  lspprid2  17001  lspsnat  17148  lsppratlem1  17150  lsppratlem3  17152  lidl0cl  17216  lidlacl  17217  lidlnegcl  17218  lidlmcl  17221  psrbaglefi  17375  psrbaglefiOLD  17376  psrass23  17416  psr1bascl  17555  ply1basf  17557  psgnghm  17852  matbas2i  18165  1mavmul  18201  mdetleib2  18241  marep01ma  18308  smadiadetlem4  18317  slesolinv  18328  cldrcl  18472  ordtbas  18638  iscnp2  18685  dis1stc  18945  ptbasfi  18996  ptpjopn  19027  ptclsg  19030  ptcnp  19037  kqtop  19160  reghmph  19208  ptcmplem2  19467  ptcmplem3  19468  ptcmplem4  19469  tsmslem1  19541  utop2nei  19667  isucn2  19696  cuspcvg  19718  cnextucn  19720  imasdsf1olem  19790  blcvx  20217  xrhmeo  20360  cnrehmeo  20367  evth  20373  reparphti  20411  iscau4  20632  iscmet3lem1  20644  lmle  20654  rrxfsupp  20743  pjthlem2  20767  ovollb2lem  20813  ovolunlem1a  20821  ovoliunlem1  20827  ovoliun2  20831  ovolscalem1  20838  ovolicc1  20841  ovolicc2lem4  20845  iundisj2  20872  voliunlem1  20873  volsup  20879  ioombl1lem4  20884  uniioovol  20901  uniioombllem3  20907  uniioombllem4  20908  uniioombllem6  20910  vitalilem5  20934  mbfimaopnlem  20975  mbflimsup  20986  mbfi1fseqlem3  21037  iblitg  21088  dvnp1  21241  cpncn  21252  dvlip2  21309  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumrlimge0  21344  dvfsumrlim2  21346  ftc1cn  21357  mpfind  21396  mpfpf1  21402  pf1mpf  21403  elplyd  21555  ply1termlem  21556  ply1term  21557  ply0  21561  plyeq0lem  21563  plyaddlem1  21566  plymullem1  21567  plyaddlem  21568  plymullem  21569  coeeulem  21577  plyco  21594  coeeq2  21595  coefv0  21600  coemulhi  21606  coemulc  21607  plycj  21629  dvply1  21635  vieta1lem2  21662  elqaalem2  21671  dvtaylp  21720  dvntaylp  21721  taylthlem1  21723  taylth  21725  ulmres  21738  ulmshftlem  21739  ulmshft  21740  ulmcau  21745  ulmdvlem1  21750  mtest  21754  mtestbdd  21755  pserulm  21772  psercn2  21773  psercnlem1  21775  psercn  21776  pserdvlem2  21778  abelthlem6  21786  abelth  21791  efif1olem1  21883  efif1olem3  21885  efif1olem4  21886  logcn  21977  advlogexp  21985  efopn  21988  cxpeq  22080  asinsin  22172  atantayl  22217  leibpilem2  22221  birthdaylem2  22231  birthdaylem3  22232  efrlim  22248  emcllem2  22275  emcllem5  22278  emcllem7  22280  harmonicbnd4  22289  fsumharmonic  22290  wilthlem2  22292  wilthlem3  22293  ftalem1  22295  ftalem2  22296  ftalem3  22297  ftalem5  22299  basellem2  22304  basellem3  22305  basellem5  22307  basellem8  22310  ppiprm  22374  ppinprm  22375  chtprm  22376  chtnprm  22377  chpp1  22378  vma1  22389  ppiltx  22400  musum  22416  0sgmppw  22422  1sgmprm  22423  ppiublem2  22427  chtublem  22435  fsumvma2  22438  chpchtsum  22443  logexprlim  22449  bposlem5  22512  lgscllem  22527  lgsval2lem  22530  lgsval4a  22542  lgsneg  22543  lgsdir2lem3  22549  lgsdir2lem5  22551  lgsdir  22554  lgsdilem2  22555  lgsdi  22556  lgsne0  22557  lgseisenlem1  22573  lgsquadlem2  22579  chebbnd1lem1  22603  chtppilimlem1  22607  rplogsumlem2  22619  rpvmasumlem  22621  dchrisumlem1  22623  dchrisumlem2  22624  dchrmusum2  22628  dchrvmasum2lem  22630  dchrvmasumiflem1  22635  dchrisum0flblem1  22642  dchrisum0flblem2  22643  dchrisum0flb  22644  dchrisum0re  22647  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0lem3  22653  mudivsum  22664  mulogsum  22666  mulog2sumlem2  22669  selberg2lem  22684  logdivbnd  22690  pntrsumo1  22699  pntrsumbnd2  22701  pntrlog2bndlem2  22712  pntrlog2bndlem4  22714  pntrlog2bndlem6a  22716  pntlemj  22737  pntlemf  22739  ostth2lem3  22769  eedimeq  22967  axlowdimlem16  23026  ebtwntg  23051  eupares  23419  eupap1  23420  eupath2lem3  23423  eupath2  23424  htthlem  24142  hhsscms  24503  shmodsi  24615  pjoc1i  24657  5oalem1  24880  mayete3i  24954  mayete3iOLD  24955  adj1  25160  iundisj2f  25756  fcnvgreu  25815  ssnnssfz  25899  iundisj2fi  25904  pnfneige0  26235  pl1cn  26239  indpreima  26335  esumfzf  26372  esumpcvgval  26381  esumpmono  26382  esumcvg  26389  measbase  26465  dya2iocnei  26551  oddpwdc  26585  eulerpartlems  26591  eulerpartlemb  26599  sseqf  26623  fibp1  26632  orrvcval4  26695  orrvcoel  26696  orrvccel  26697  ballotlem2  26719  ballotlemfrceq  26759  signsplypnf  26799  signswch  26810  signstf0  26817  signstfvn  26818  signstfvneq0  26821  signstfvcl  26822  signstfveq0  26826  signsvfn  26831  lgamgulm2  26870  lgamcvglem  26874  lgamcvg2  26889  gamcvg2lem  26893  subfacp1lem1  26915  subfacp1lem5  26920  subfacp1lem6  26921  subfacval2  26923  erdszelem7  26933  cvxscon  26980  cvmliftlem5  27026  cvmliftlem7  27028  cvmliftlem10  27031  cvmliftlem13  27033  relexpsucr  27179  clim2prod  27250  clim2div  27251  ntrivcvgfvn0  27261  ntrivcvgtail  27262  prodeq2ii  27273  prodmolem3  27293  prodmolem2a  27294  fprod  27301  fprodntriv  27302  fprodss  27308  fprodser  27309  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodabs  27331  fprodefsum  27332  fprodeq0  27333  fprodn0  27337  iprodclim3  27347  iprodmul  27350  fallfacfwd  27386  0fallfac  27387  binomfallfaclem2  27390  fallfacval4  27393  bdayelon  27668  imageval  27808  bpolysum  28043  bpolydiflem  28044  fsumkthpow  28046  mblfinlem2  28273  ftc1cnnc  28310  upixp  28467  sdclem2  28482  caushft  28501  ismtyres  28551  rrnmet  28572  rrndstprj1  28573  rrndstprj2  28574  rrncmslem  28575  rrnequiv  28578  iccbnd  28583  mapfzcons  28897  diophren  28997  irrapxlem1  29008  monotuz  29127  acongeq  29171  jm2.26lem3  29195  jm3.1lem2  29212  pw2f1ocnv  29231  idomodle  29406  fcnre  29592  refsumcn  29597  rfcnnnub  29603  climsuselem1  29626  stoweidlem11  29652  stoweidlem15  29656  stoweidlem17  29658  stoweidlem20  29661  stoweidlem34  29675  stoweidlem35  29676  stoweidlem46  29687  stoweidlem47  29688  stoweidlem56  29697  stoweidlem59  29700  stoweidlem62  29703  stirlinglem5  29719  stirlinglem14  29728  zlmodzxzscm  30588  rmsupp0  30612  lincsum  30672  lincscm  30673  lindslinindimp2lem4  30704  lincresunit3  30724  bnj1172  31694  bnj1245  31707  bnj1311  31717  bnj1450  31743  bnj1501  31760  osumcllem7N  33179  pexmidlem4N  33190  lcfrlem4  34763  lcfrlem5  34764  lcfrlem6  34765  lcfrlem16  34776  lcfrlem38  34798  mapdrvallem2  34863  mapdh8ab  34995  mapdh8ad  34997  mapdh8e  35002