Theorem syl6eleq 2565

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  syl6eleqr  2566  3eltr3g  2571  prid2g  4134  ndmfvrcl  5889  fnwelem  6895  tz7.48-1  7105  brwitnlem  7154  oeeulem  7247  dffi3  7887  cnfcom3lem  8143  cnfcom3lemOLD  8151  alephgeom  8459  fpwwe2lem6  9009  canthwelem  9024  hargch  9047  r1wunlim  9111  eluzel2  11083  fseq1p1m1  11748  fznn0sub2  11775  nn0split  11783  exple1  12187  digit1  12262  bcval5  12358  bcpasc  12361  hashf1  12466  seqcoll  12472  seqcoll2  12473  swrdccat1  12639  swrdccat2  12640  cats1un  12658  splfv2a  12689  splval2  12690  caubnd  13147  limsupgre  13260  clim2ser  13433  clim2ser2  13434  iserex  13435  isermulc2  13436  iserle  13438  iserge0  13439  climub  13440  climserle  13441  isercolllem2  13444  isercolllem3  13445  isercoll  13446  isercoll2  13447  serf0  13459  iseraltlem2  13461  iseraltlem3  13462  iseralt  13463  sumeq2ii  13471  summolem3  13492  summolem2a  13493  fsum  13498  sum0  13499  fsumcl2lem  13509  fsumadd  13517  isumclim3  13530  isumadd  13538  fsump1i  13540  fsummulc2  13555  fsumrelem  13577  iserabs  13585  cvgcmp  13586  cvgcmpub  13587  cvgcmpce  13588  binom1dif  13601  isumshft  13607  isumsplit  13608  isumrpcl  13611  isumsup2  13614  climcndslem1  13617  climcndslem2  13618  climcnds  13619  arisum2  13628  trireciplem  13629  geoser  13634  geolim  13635  geo2lim  13640  cvgrat  13648  mertenslem1  13649  mertenslem2  13650  mertens  13651  efcvgfsum  13676  efcj  13682  effsumlt  13700  ruclem7  13823  bitsfzolem  13936  bitsfzo  13937  bitsfi  13939  bitsinv1lem  13943  bitsinv1  13944  bitsinvp1  13951  sadcp1  13957  sadadd  13969  sadass  13973  bitsres  13975  smupp1  13982  smuval2  13984  smupval  13990  smueqlem  13992  smumul  13995  algrp1  14055  phiprmpw  14158  crt  14160  phimullem  14161  eulerthlem2  14164  prmdiv  14167  pcpremul  14219  pcmpt  14263  pcfac  14270  pockthlem  14275  pockthg  14276  prmreclem2  14287  prmreclem3  14288  prmreclem4  14289  prmreclem5  14290  prmreclem6  14291  prmrec  14292  1arith  14297  vdwapun  14344  vdwlem1  14351  vdwlem2  14352  vdwlem3  14353  vdwlem6  14356  vdwlem8  14358  vdwlem10  14360  vdw  14364  imasvscafn  14785  xpsfrnel2  14813  oppccatid  14968  oppccomfpropd  14976  funcoppc  15095  invfuc  15194  hofcl  15379  yonedalem4c  15397  gsumwsubmcl  15826  gsumccat  15829  gsumwmhm  15833  mulgnnp1  15947  mulgnnsubcl  15951  mulgnn0z  15959  mulgnndir  15961  psgnunilem4  16315  psgnran  16333  sylow1lem1  16411  lsmmod2  16487  lsmdisj2r  16496  efginvrel2  16538  efgsdmi  16543  efgsrel  16545  efgs1b  16547  efgsp1  16548  efgredleme  16554  efgredlemc  16556  efgcpbllemb  16566  frgpuplem  16583  mulgnn0di  16627  frgpnabllem1  16665  lt6abl  16685  cycsubgcyg  16691  gsumval3eu  16695  gsumval3OLD  16696  gsumval3  16699  gsumzcl2  16703  gsumzclOLD  16707  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumconst  16742  gsumzmhm  16745  gsumzmhmOLD  16746  gsumzoppg  16755  gsumzoppgOLD  16756  telgsumfz0s  16808  dprd2da  16878  pgpfaclem1  16919  srgbinom  16981  isirred  17129  lspprid2  17424  lspsnat  17571  lsppratlem1  17573  lsppratlem3  17575  lidl0cl  17639  lidlacl  17640  lidlnegcl  17641  lidlmcl  17644  psrbaglefi  17791  psrbaglefiOLD  17792  psrass23l  17831  psrass23  17833  mplcoe5lem  17898  mpfind  17973  psr1bascl  18007  ply1basf  18009  gsummoncoe1  18114  lply1binom  18116  lply1binomsc  18117  mpfpf1  18155  pf1mpf  18156  evl1scvarpw  18167  psgnghm  18380  matbas2i  18688  matecld  18692  matgsum  18703  dmatmul  18763  1mavmul  18814  mdetleib2  18854  m1detdiag  18863  marep01ma  18926  smadiadetlem4  18935  slesolinv  18946  pmatcollpw3fi1lem1  19051  chpscmat  19107  chpscmatgsumbin  19109  chp0mat  19111  chpidmat  19112  chfacfisf  19119  chfacfisfcpmat  19120  chfacfpmmulgsum2  19130  cldrcl  19290  ordtbas  19456  iscnp2  19503  dis1stc  19763  ptbasfi  19814  ptpjopn  19845  ptclsg  19848  ptcnp  19855  kqtop  19978  reghmph  20026  ptcmplem2  20285  ptcmplem3  20286  ptcmplem4  20287  tsmslem1  20359  utop2nei  20485  isucn2  20514  cuspcvg  20536  cnextucn  20538  imasdsf1olem  20608  blcvx  21035  xrhmeo  21178  cnrehmeo  21185  evth  21191  reparphti  21229  iscau4  21450  iscmet3lem1  21462  lmle  21472  rrxfsupp  21561  pjthlem2  21585  ovollb2lem  21631  ovolunlem1a  21639  ovoliunlem1  21645  ovoliun2  21649  ovolscalem1  21656  ovolicc1  21659  ovolicc2lem4  21663  iundisj2  21691  voliunlem1  21692  volsup  21698  ioombl1lem4  21703  uniioovol  21720  uniioombllem3  21726  uniioombllem4  21727  uniioombllem6  21729  vitalilem5  21753  mbfimaopnlem  21794  mbflimsup  21805  mbfi1fseqlem3  21856  iblitg  21907  dvnp1  22060  cpncn  22071  dvlip2  22128  dvfsumlem2  22160  dvfsumlem3  22161  dvfsumrlimge0  22163  dvfsumrlim2  22165  ftc1cn  22176  elplyd  22331  ply1termlem  22332  ply1term  22333  ply0  22337  plyeq0lem  22339  plyaddlem1  22342  plymullem1  22343  plyaddlem  22344  plymullem  22345  coeeulem  22353  plyco  22370  coeeq2  22371  coefv0  22376  coemulhi  22382  coemulc  22383  plycj  22405  dvply1  22411  vieta1lem2  22438  elqaalem2  22447  dvtaylp  22496  dvntaylp  22497  taylthlem1  22499  taylth  22501  ulmres  22514  ulmshftlem  22515  ulmshft  22516  ulmcau  22521  ulmdvlem1  22526  mtest  22530  mtestbdd  22531  pserulm  22548  psercn2  22549  psercnlem1  22551  psercn  22552  pserdvlem2  22554  abelthlem6  22562  abelth  22567  efif1olem1  22659  efif1olem3  22661  efif1olem4  22662  logcn  22753  advlogexp  22761  efopn  22764  cxpeq  22856  asinsin  22948  atantayl  22993  leibpilem2  22997  birthdaylem2  23007  birthdaylem3  23008  efrlim  23024  emcllem2  23051  emcllem5  23054  emcllem7  23056  harmonicbnd4  23065  fsumharmonic  23066  wilthlem2  23068  wilthlem3  23069  ftalem1  23071  ftalem2  23072  ftalem3  23073  ftalem5  23075  basellem2  23080  basellem3  23081  basellem5  23083  basellem8  23086  ppiprm  23150  ppinprm  23151  chtprm  23152  chtnprm  23153  chpp1  23154  vma1  23165  ppiltx  23176  musum  23192  0sgmppw  23198  1sgmprm  23199  ppiublem2  23203  chtublem  23211  fsumvma2  23214  chpchtsum  23219  logexprlim  23225  bposlem5  23288  lgscllem  23303  lgsval2lem  23306  lgsval4a  23318  lgsneg  23319  lgsdir2lem3  23325  lgsdir2lem5  23327  lgsdir  23330  lgsdilem2  23331  lgsdi  23332  lgsne0  23333  lgseisenlem1  23349  lgsquadlem2  23355  chebbnd1lem1  23379  chtppilimlem1  23383  rplogsumlem2  23395  rpvmasumlem  23397  dchrisumlem1  23399  dchrisumlem2  23400  dchrmusum2  23404  dchrvmasum2lem  23406  dchrvmasumiflem1  23411  dchrisum0flblem1  23418  dchrisum0flblem2  23419  dchrisum0flb  23420  dchrisum0re  23423  dchrisum0lem1b  23425  dchrisum0lem1  23426  dchrisum0lem2a  23427  dchrisum0lem2  23428  dchrisum0lem3  23429  mudivsum  23440  mulogsum  23442  mulog2sumlem2  23445  selberg2lem  23460  logdivbnd  23466  pntrsumo1  23475  pntrsumbnd2  23477  pntrlog2bndlem2  23488  pntrlog2bndlem4  23490  pntrlog2bndlem6a  23492  pntlemj  23513  pntlemf  23515  ostth2lem3  23545  tglngne  23662  ltgseg  23706  eedimeq  23874  axlowdimlem16  23933  ebtwntg  23958  eupares  24648  eupap1  24649  eupath2lem3  24652  eupath2  24653  htthlem  25507  hhsscms  25868  shmodsi  25980  pjoc1i  26022  5oalem1  26245  mayete3i  26319  mayete3iOLD  26320  adj1  26525  iundisj2f  27119  fcnvgreu  27183  ssnnssfz  27262  iundisj2fi  27267  pnfneige0  27566  pl1cn  27570  indpreima  27675  esumfzf  27712  esumpcvgval  27721  esumpmono  27722  esumcvg  27729  measbase  27805  dya2iocnei  27890  oddpwdc  27930  eulerpartlems  27936  eulerpartlemb  27944  sseqf  27968  fibp1  27977  orrvcval4  28040  orrvcoel  28041  orrvccel  28042  ballotlem2  28064  ballotlemfrceq  28104  signsplypnf  28144  signswch  28155  signstf0  28162  signstfvn  28163  signstfvneq0  28166  signstfvcl  28167  signstfveq0  28171  signsvfn  28176  lgamgulm2  28215  lgamcvglem  28219  lgamcvg2  28234  gamcvg2lem  28238  subfacp1lem1  28260  subfacp1lem5  28265  subfacp1lem6  28266  subfacval2  28268  erdszelem7  28278  cvxscon  28325  cvmliftlem5  28371  cvmliftlem7  28373  cvmliftlem10  28376  cvmliftlem13  28378  relexpsucr  28525  clim2prod  28596  clim2div  28597  ntrivcvgfvn0  28607  ntrivcvgtail  28608  prodeq2ii  28619  prodmolem3  28639  prodmolem2a  28640  fprod  28647  fprodntriv  28648  fprodss  28654  fprodser  28655  fprodcl2lem  28656  fprodmul  28664  fproddiv  28665  fprodabs  28677  fprodefsum  28678  fprodeq0  28679  fprodn0  28683  iprodclim3  28693  iprodmul  28696  fallfacfwd  28732  0fallfac  28733  binomfallfaclem2  28736  fallfacval4  28739  bdayelon  29014  imageval  29154  bpolysum  29389  bpolydiflem  29390  fsumkthpow  29392  mblfinlem2  29627  ftc1cnnc  29664  upixp  29821  sdclem2  29836  caushft  29855  ismtyres  29905  rrnmet  29926  rrndstprj1  29927  rrndstprj2  29928  rrncmslem  29929  rrnequiv  29932  iccbnd  29937  mapfzcons  30250  diophren  30349  irrapxlem1  30360  monotuz  30479  acongeq  30523  jm2.26lem3  30547  jm3.1lem2  30564  pw2f1ocnv  30583  idomodle  30758  hashnzfz2  30826  fcnre  30978  refsumcn  30983  rfcnnnub  30989  climsuselem1  31149  limcperiod  31170  sumnnodd  31172  lptioo2cn  31187  lptioo1cn  31188  cncfshift  31212  cncfperiod  31217  stoweidlem11  31311  stoweidlem15  31315  stoweidlem17  31317  stoweidlem20  31320  stoweidlem34  31334  stoweidlem35  31335  stoweidlem46  31346  stoweidlem47  31347  stoweidlem56  31356  stoweidlem59  31359  stoweidlem62  31362  stirlinglem5  31378  stirlinglem14  31387  fourierdlem16  31423  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem25  31432  fourierdlem51  31458  fourierdlem52  31459  fourierdlem54  31461  fourierdlem65  31472  fourierdlem69  31476  fourierdlem71  31478  fourierdlem80  31487  fourierdlem83  31490  fourierdlem92  31499  fourierdlem93  31500  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fourierdlem113  31520  fourierdlem114  31521  ssnn0ssfz  32002  zlmodzxzscm  32010  rmsupp0  32034  lincsum  32103  lincscm  32104  lindslinindimp2lem4  32135  lincresunit3  32155  bnj1172  33136  bnj1245  33149  bnj1311  33159  bnj1450  33185  bnj1501  33202  osumcllem7N  34758  pexmidlem4N  34769  lcfrlem4  36342  lcfrlem5  36343  lcfrlem6  36344  lcfrlem16  36355  lcfrlem38  36377  mapdrvallem2  36442  mapdh8ab  36574  mapdh8ad  36576  mapdh8e  36581