Theorem syl6eleq 2549

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

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446

This theorem is referenced by:  syl6eleqr  2550  3eltr3g  2555  prid2g  4080  ndmfvrcl  5814  fnwelem  6787  tz7.48-1  6998  brwitnlem  7047  oeeulem  7140  dffi3  7782  cnfcom3lem  8037  cnfcom3lemOLD  8045  alephgeom  8353  fpwwe2lem6  8903  canthwelem  8918  hargch  8941  r1wunlim  9005  eluzel2  10967  fznn0sub2  11589  fseq1p1m1  11635  exple1  12024  digit1  12099  bcval5  12195  bcpasc  12198  hashf1  12312  seqcoll  12318  seqcoll2  12319  swrdccat1  12453  swrdccat2  12454  cats1un  12472  splfv2a  12500  splval2  12501  caubnd  12948  limsupgre  13061  clim2ser  13234  clim2ser2  13235  iserex  13236  isermulc2  13237  iserle  13239  iserge0  13240  climub  13241  climserle  13242  isercolllem2  13245  isercolllem3  13246  isercoll  13247  isercoll2  13248  serf0  13260  iseraltlem2  13262  iseraltlem3  13263  iseralt  13264  sumeq2ii  13272  summolem3  13293  summolem2a  13294  fsum  13299  sum0  13300  fsumcl2lem  13310  fsumadd  13317  isumclim3  13328  isumadd  13336  fsump1i  13338  fsummulc2  13353  fsumrelem  13372  iserabs  13380  cvgcmp  13381  cvgcmpub  13382  cvgcmpce  13383  binom1dif  13398  isumshft  13404  isumsplit  13405  isumrpcl  13408  isumsup2  13411  climcndslem1  13414  climcndslem2  13415  climcnds  13416  arisum2  13425  trireciplem  13426  geoser  13431  geolim  13432  geo2lim  13437  cvgrat  13445  mertenslem1  13446  mertenslem2  13447  mertens  13448  efcvgfsum  13473  efcj  13479  effsumlt  13497  ruclem7  13620  bitsfzolem  13732  bitsfzo  13733  bitsfi  13735  bitsinv1lem  13739  bitsinv1  13740  bitsinvp1  13747  sadcp1  13753  sadadd  13765  sadass  13769  bitsres  13771  smupp1  13778  smuval2  13780  smupval  13786  smueqlem  13788  smumul  13791  algrp1  13851  phiprmpw  13953  crt  13955  phimullem  13956  eulerthlem2  13959  prmdiv  13962  pcpremul  14012  pcmpt  14056  pcfac  14063  pockthlem  14068  pockthg  14069  prmreclem2  14080  prmreclem3  14081  prmreclem4  14082  prmreclem5  14083  prmreclem6  14084  prmrec  14085  1arith  14090  vdwapun  14137  vdwlem1  14144  vdwlem2  14145  vdwlem3  14146  vdwlem6  14149  vdwlem8  14151  vdwlem10  14153  vdw  14157  imasvscafn  14577  xpsfrnel2  14605  oppccatid  14760  oppccomfpropd  14768  funcoppc  14887  invfuc  14986  hofcl  15171  yonedalem4c  15189  gsumwsubmcl  15618  gsumccat  15621  gsumwmhm  15625  mulgnnp1  15737  mulgnnsubcl  15741  mulgnn0z  15749  mulgnndir  15751  psgnunilem4  16105  psgnran  16123  sylow1lem1  16201  lsmmod2  16277  lsmdisj2r  16286  efginvrel2  16328  efgsdmi  16333  efgsrel  16335  efgs1b  16337  efgsp1  16338  efgredleme  16344  efgredlemc  16346  efgcpbllemb  16356  frgpuplem  16373  mulgnn0di  16417  frgpnabllem1  16455  lt6abl  16475  cycsubgcyg  16481  gsumval3eu  16485  gsumval3OLD  16486  gsumval3  16489  gsumzcl2  16493  gsumzclOLD  16497  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumconst  16532  gsumzmhm  16535  gsumzmhmOLD  16536  gsumzoppg  16545  gsumzoppgOLD  16546  dprd2da  16646  pgpfaclem1  16687  srgbinom  16749  isirred  16897  lspprid2  17185  lspsnat  17332  lsppratlem1  17334  lsppratlem3  17336  lidl0cl  17400  lidlacl  17401  lidlnegcl  17402  lidlmcl  17405  psrbaglefi  17547  psrbaglefiOLD  17548  psrass23l  17587  psrass23  17589  mplcoe5lem  17654  mpfind  17729  psr1bascl  17763  ply1basf  17765  mpfpf1  17894  pf1mpf  17895  evl1scvarpw  17906  psgnghm  18119  matbas2i  18432  matecld  18436  1mavmul  18470  mdetleib2  18510  m1detdiag  18519  marep01ma  18582  smadiadetlem4  18591  slesolinv  18602  cldrcl  18746  ordtbas  18912  iscnp2  18959  dis1stc  19219  ptbasfi  19270  ptpjopn  19301  ptclsg  19304  ptcnp  19311  kqtop  19434  reghmph  19482  ptcmplem2  19741  ptcmplem3  19742  ptcmplem4  19743  tsmslem1  19815  utop2nei  19941  isucn2  19970  cuspcvg  19992  cnextucn  19994  imasdsf1olem  20064  blcvx  20491  xrhmeo  20634  cnrehmeo  20641  evth  20647  reparphti  20685  iscau4  20906  iscmet3lem1  20918  lmle  20928  rrxfsupp  21017  pjthlem2  21041  ovollb2lem  21087  ovolunlem1a  21095  ovoliunlem1  21101  ovoliun2  21105  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem4  21119  iundisj2  21146  voliunlem1  21147  volsup  21153  ioombl1lem4  21158  uniioovol  21175  uniioombllem3  21181  uniioombllem4  21182  uniioombllem6  21184  vitalilem5  21208  mbfimaopnlem  21249  mbflimsup  21260  mbfi1fseqlem3  21311  iblitg  21362  dvnp1  21515  cpncn  21526  dvlip2  21583  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumrlimge0  21618  dvfsumrlim2  21620  ftc1cn  21631  elplyd  21786  ply1termlem  21787  ply1term  21788  ply0  21792  plyeq0lem  21794  plyaddlem1  21797  plymullem1  21798  plyaddlem  21799  plymullem  21800  coeeulem  21808  plyco  21825  coeeq2  21826  coefv0  21831  coemulhi  21837  coemulc  21838  plycj  21860  dvply1  21866  vieta1lem2  21893  elqaalem2  21902  dvtaylp  21951  dvntaylp  21952  taylthlem1  21954  taylth  21956  ulmres  21969  ulmshftlem  21970  ulmshft  21971  ulmcau  21976  ulmdvlem1  21981  mtest  21985  mtestbdd  21986  pserulm  22003  psercn2  22004  psercnlem1  22006  psercn  22007  pserdvlem2  22009  abelthlem6  22017  abelth  22022  efif1olem1  22114  efif1olem3  22116  efif1olem4  22117  logcn  22208  advlogexp  22216  efopn  22219  cxpeq  22311  asinsin  22403  atantayl  22448  leibpilem2  22452  birthdaylem2  22462  birthdaylem3  22463  efrlim  22479  emcllem2  22506  emcllem5  22509  emcllem7  22511  harmonicbnd4  22520  fsumharmonic  22521  wilthlem2  22523  wilthlem3  22524  ftalem1  22526  ftalem2  22527  ftalem3  22528  ftalem5  22530  basellem2  22535  basellem3  22536  basellem5  22538  basellem8  22541  ppiprm  22605  ppinprm  22606  chtprm  22607  chtnprm  22608  chpp1  22609  vma1  22620  ppiltx  22631  musum  22647  0sgmppw  22653  1sgmprm  22654  ppiublem2  22658  chtublem  22666  fsumvma2  22669  chpchtsum  22674  logexprlim  22680  bposlem5  22743  lgscllem  22758  lgsval2lem  22761  lgsval4a  22773  lgsneg  22774  lgsdir2lem3  22780  lgsdir2lem5  22782  lgsdir  22785  lgsdilem2  22786  lgsdi  22787  lgsne0  22788  lgseisenlem1  22804  lgsquadlem2  22810  chebbnd1lem1  22834  chtppilimlem1  22838  rplogsumlem2  22850  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem2  22855  dchrmusum2  22859  dchrvmasum2lem  22861  dchrvmasumiflem1  22866  dchrisum0flblem1  22873  dchrisum0flblem2  22874  dchrisum0flb  22875  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  mudivsum  22895  mulogsum  22897  mulog2sumlem2  22900  selberg2lem  22915  logdivbnd  22921  pntrsumo1  22930  pntrsumbnd2  22932  pntrlog2bndlem2  22943  pntrlog2bndlem4  22945  pntrlog2bndlem6a  22947  pntlemj  22968  pntlemf  22970  ostth2lem3  23000  tglngne  23103  eedimeq  23279  axlowdimlem16  23338  ebtwntg  23363  eupares  23731  eupap1  23732  eupath2lem3  23735  eupath2  23736  htthlem  24454  hhsscms  24815  shmodsi  24927  pjoc1i  24969  5oalem1  25192  mayete3i  25266  mayete3iOLD  25267  adj1  25472  iundisj2f  26066  fcnvgreu  26125  ssnnssfz  26210  iundisj2fi  26215  pnfneige0  26515  pl1cn  26519  indpreima  26615  esumfzf  26652  esumpcvgval  26661  esumpmono  26662  esumcvg  26669  measbase  26745  dya2iocnei  26831  oddpwdc  26871  eulerpartlems  26877  eulerpartlemb  26885  sseqf  26909  fibp1  26918  orrvcval4  26981  orrvcoel  26982  orrvccel  26983  ballotlem2  27005  ballotlemfrceq  27045  signsplypnf  27085  signswch  27096  signstf0  27103  signstfvn  27104  signstfvneq0  27107  signstfvcl  27108  signstfveq0  27112  signsvfn  27117  lgamgulm2  27156  lgamcvglem  27160  lgamcvg2  27175  gamcvg2lem  27179  subfacp1lem1  27201  subfacp1lem5  27206  subfacp1lem6  27207  subfacval2  27209  erdszelem7  27219  cvxscon  27266  cvmliftlem5  27312  cvmliftlem7  27314  cvmliftlem10  27317  cvmliftlem13  27319  relexpsucr  27466  clim2prod  27537  clim2div  27538  ntrivcvgfvn0  27548  ntrivcvgtail  27549  prodeq2ii  27560  prodmolem3  27580  prodmolem2a  27581  fprod  27588  fprodntriv  27589  fprodss  27595  fprodser  27596  fprodcl2lem  27597  fprodmul  27605  fproddiv  27606  fprodabs  27618  fprodefsum  27619  fprodeq0  27620  fprodn0  27624  iprodclim3  27634  iprodmul  27637  fallfacfwd  27673  0fallfac  27674  binomfallfaclem2  27677  fallfacval4  27680  bdayelon  27955  imageval  28095  bpolysum  28330  bpolydiflem  28331  fsumkthpow  28333  mblfinlem2  28567  ftc1cnnc  28604  upixp  28761  sdclem2  28776  caushft  28795  ismtyres  28845  rrnmet  28866  rrndstprj1  28867  rrndstprj2  28868  rrncmslem  28869  rrnequiv  28872  iccbnd  28877  mapfzcons  29190  diophren  29290  irrapxlem1  29301  monotuz  29420  acongeq  29464  jm2.26lem3  29488  jm3.1lem2  29505  pw2f1ocnv  29524  idomodle  29699  fcnre  29885  refsumcn  29890  rfcnnnub  29896  climsuselem1  29918  stoweidlem11  29944  stoweidlem15  29948  stoweidlem17  29950  stoweidlem20  29953  stoweidlem34  29967  stoweidlem35  29968  stoweidlem46  29979  stoweidlem47  29980  stoweidlem56  29989  stoweidlem59  29992  stoweidlem62  29995  stirlinglem5  30011  stirlinglem14  30020  nn0split  30875  ssnn0ssfz  30879  zlmodzxzscm  30892  rmsupp0  30919  telescfzgsum0  30953  gsummoncoe1  30985  lply1binom  30997  lply1binomsc  30998  matgsum  31015  dmatmul  31030  dmatmulcl  31033  dmatcrng  31035  scmatmulcl  31040  scmatcrng  31042  lincsum  31070  lincscm  31071  lindslinindimp2lem4  31102  lincresunit3  31122  pmatcollpw1lem4  31230  pmatcollpw1  31232  pmatcollpw  31234  pmatcollpw4fi1lem1  31242  pmatcollpwscmatlem3  31247  cpscmat  31296  cpscmatgsumbin  31298  cp0mat  31300  cpidmat  31301  chfacfisf  31308  chfacfisfcpmat  31309  chfacfpmmulgsum2  31319  bnj1172  32292  bnj1245  32305  bnj1311  32315  bnj1450  32341  bnj1501  32358  osumcllem7N  33912  pexmidlem4N  33923  lcfrlem4  35496  lcfrlem5  35497  lcfrlem6  35498  lcfrlem16  35509  lcfrlem38  35531  mapdrvallem2  35596  mapdh8ab  35728  mapdh8ad  35730  mapdh8e  35735