Theorem syl6eleq 2494

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721

This theorem is referenced by:  syl6eleqr  2495  prid2g  3871  ndmfvrcl  5715  fnwelem  6420  tz7.48-1  6659  brwitnlem  6710  oeeulem  6803  dffi3  7394  cnfcom3lem  7616  alephgeom  7919  fpwwe2lem6  8466  canthwelem  8481  hargch  8508  r1wunlim  8568  eluzel2  10449  fznn0sub2  11042  fseq1p1m1  11077  exple1  11394  digit1  11468  bcval5  11564  bcpasc  11567  hashf1  11661  seqcoll  11667  seqcoll2  11668  swrdccat1  11729  swrdccat2  11730  splfv2a  11740  splval2  11741  cats1un  11745  caubnd  12117  limsupgre  12230  clim2ser  12403  clim2ser2  12404  iserex  12405  isermulc2  12406  iserle  12408  iserge0  12409  climub  12410  climserle  12411  isercolllem2  12414  isercolllem3  12415  isercoll  12416  isercoll2  12417  serf0  12429  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  sumeq2ii  12442  summolem3  12463  summolem2a  12464  fsum  12469  sum0  12470  fsumcl2lem  12480  fsumadd  12487  isumclim3  12498  isumadd  12506  fsump1i  12508  fsummulc2  12522  fsumrelem  12541  iserabs  12549  cvgcmp  12550  cvgcmpub  12551  cvgcmpce  12552  binom1dif  12567  isumshft  12574  isumsplit  12575  isumrpcl  12578  isumsup2  12581  climcndslem1  12584  climcndslem2  12585  climcnds  12586  arisum2  12595  trireciplem  12596  geoser  12601  geolim  12602  geo2lim  12607  cvgrat  12615  mertenslem1  12616  mertenslem2  12617  mertens  12618  efcvgfsum  12643  efcj  12649  effsumlt  12667  ruclem7  12790  bitsfzolem  12901  bitsfzo  12902  bitsfi  12904  bitsinv1lem  12908  bitsinv1  12909  bitsinvp1  12916  sadcp1  12922  sadadd  12934  sadass  12938  bitsres  12940  smupp1  12947  smuval2  12949  smupval  12955  smueqlem  12957  smumul  12960  algrp1  13020  phiprmpw  13120  crt  13122  phimullem  13123  eulerthlem2  13126  prmdiv  13129  pcpremul  13172  pcmpt  13216  pcfac  13223  pockthlem  13228  pockthg  13229  prmreclem2  13240  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  prmrec  13245  1arith  13250  vdwapun  13297  vdwlem1  13304  vdwlem2  13305  vdwlem3  13306  vdwlem6  13309  vdwlem8  13311  vdwlem10  13313  vdw  13317  imasvscafn  13717  xpsfrnel2  13745  oppccatid  13900  oppccomfpropd  13908  funcoppc  14027  invfuc  14126  hofcl  14311  yonedalem4c  14329  gsumwsubmcl  14739  gsumccat  14742  gsumwmhm  14745  mulgnnp1  14853  mulgnnsubcl  14857  mulgnn0z  14865  mulgnndir  14867  sylow1lem1  15187  lsmmod2  15263  lsmdisj2r  15272  efginvrel2  15314  efgsdmi  15319  efgsrel  15321  efgs1b  15323  efgsp1  15324  efgredleme  15330  efgredlemc  15332  efgcpbllemb  15342  frgpuplem  15359  mulgnn0di  15403  frgpnabllem1  15439  lt6abl  15459  cycsubgcyg  15465  gsumval3eu  15468  gsumval3  15469  gsumzcl  15473  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  dprd2da  15555  pgpfaclem1  15594  isirred  15759  lspprid2  16029  lspsnat  16172  lsppratlem1  16174  lsppratlem3  16176  lidl0cl  16238  lidlacl  16239  lidlnegcl  16240  lidlmcl  16243  psrbaglefi  16392  psrass23  16428  psr1bascl  16553  ply1basf  16555  cldrcl  17045  ordtbas  17210  iscnp2  17257  dis1stc  17515  ptbasfi  17566  ptpjopn  17597  ptclsg  17600  ptcnp  17607  kqtop  17730  reghmph  17778  ptcmplem2  18037  ptcmplem3  18038  ptcmplem4  18039  tsmslem1  18111  utop2nei  18233  isucn2  18262  cuspcvg  18284  cnextucn  18286  imasdsf1olem  18356  blcvx  18782  xrhmeo  18924  cnrehmeo  18931  evth  18937  reparphti  18975  iscau4  19185  iscmet3lem1  19197  lmle  19207  pjthlem2  19292  ovollb2lem  19337  ovolunlem1a  19345  ovoliunlem1  19351  ovoliun2  19355  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem4  19369  iundisj2  19396  voliunlem1  19397  volsup  19403  ioombl1lem4  19408  uniioovol  19424  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  vitalilem5  19457  mbfimaopnlem  19500  mbflimsup  19511  mbfi1fseqlem3  19562  iblitg  19613  dvnp1  19764  cpncn  19775  dvlip2  19832  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumrlimge0  19867  dvfsumrlim2  19869  ftc1cn  19880  mpfind  19918  mpfpf1  19924  pf1mpf  19925  elplyd  20074  ply1termlem  20075  ply1term  20076  ply0  20080  plyeq0lem  20082  plyaddlem1  20085  plymullem1  20086  plyaddlem  20087  plymullem  20088  coeeulem  20096  plyco  20113  coeeq2  20114  coefv0  20119  coemulhi  20125  coemulc  20126  plycj  20148  dvply1  20154  vieta1lem2  20181  elqaalem2  20190  dvtaylp  20239  dvntaylp  20240  taylthlem1  20242  taylth  20244  ulmres  20257  ulmshftlem  20258  ulmshft  20259  ulmcau  20264  ulmdvlem1  20269  mtest  20273  mtestbdd  20274  pserulm  20291  psercn2  20292  psercnlem1  20294  psercn  20295  pserdvlem2  20297  abelthlem6  20305  abelth  20310  efif1olem1  20397  efif1olem3  20399  efif1olem4  20400  logcn  20491  advlogexp  20499  efopn  20502  cxpeq  20594  asinsin  20685  atantayl  20730  leibpilem2  20734  birthdaylem2  20744  birthdaylem3  20745  efrlim  20761  emcllem2  20788  emcllem5  20791  emcllem7  20793  harmonicbnd4  20802  fsumharmonic  20803  wilthlem2  20805  wilthlem3  20806  ftalem1  20808  ftalem2  20809  ftalem3  20810  ftalem5  20812  basellem2  20817  basellem3  20818  basellem5  20820  basellem8  20823  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  chpp1  20891  vma1  20902  ppiltx  20913  musum  20929  0sgmppw  20935  1sgmprm  20936  ppiublem2  20940  chtublem  20948  fsumvma2  20951  chpchtsum  20956  logexprlim  20962  bposlem5  21025  lgscllem  21040  lgsval2lem  21043  lgsval4a  21055  lgsneg  21056  lgsdir2lem3  21062  lgsdir2lem5  21064  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgseisenlem1  21086  lgsquadlem2  21092  chebbnd1lem1  21116  chtppilimlem1  21120  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem2  21137  dchrmusum2  21141  dchrvmasum2lem  21143  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0flb  21157  dchrisum0re  21160  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  mudivsum  21177  mulogsum  21179  mulog2sumlem2  21182  selberg2lem  21197  logdivbnd  21203  pntrsumo1  21212  pntrsumbnd2  21214  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem6a  21229  pntlemj  21250  pntlemf  21252  ostth2lem3  21282  eupares  21650  eupap1  21651  eupath2lem3  21654  eupath2  21655  htthlem  22373  hhsscms  22732  shmodsi  22844  pjoc1i  22886  5oalem1  23109  mayete3i  23183  mayete3iOLD  23184  adj1  23389  iundisj2f  23983  ssnnssfz  24101  iundisj2fi  24106  pnfneige0  24289  indpreima  24375  esumfzf  24412  esumpcvgval  24421  esumpmono  24422  esumcvg  24429  measbase  24504  dya2iocnei  24585  orrvcval4  24675  orrvcoel  24676  orrvccel  24677  ballotlem2  24699  ballotlemfrceq  24739  lgamgulm2  24773  lgamcvglem  24777  lgamcvg2  24792  gamcvg2lem  24796  subfacp1lem1  24818  subfacp1lem5  24823  subfacp1lem6  24824  subfacval2  24826  erdszelem7  24836  cvxscon  24883  cvmliftlem5  24929  cvmliftlem7  24931  cvmliftlem10  24934  cvmliftlem13  24936  relexpsucr  25083  clim2prod  25169  clim2div  25170  ntrivcvgfvn0  25180  ntrivcvgtail  25181  prodeq2ii  25192  prodmolem3  25212  prodmolem2a  25213  fprod  25220  fprodntriv  25221  fprodss  25227  fprodser  25228  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodabs  25250  fprodefsum  25251  fprodeq0  25252  fprodn0  25256  iprodclim3  25266  iprodmul  25269  fallfacfwd  25303  0fallfac  25304  binomfallfaclem2  25307  bdayelon  25548  imageval  25683  eedimeq  25741  axlowdimlem16  25800  bpolysum  26003  bpolydiflem  26004  fsumkthpow  26006  mblfinlem  26143  ftc1cnnc  26178  upixp  26321  sdclem2  26336  caushft  26357  ismtyres  26407  rrnmet  26428  rrndstprj1  26429  rrndstprj2  26430  rrncmslem  26431  rrnequiv  26434  iccbnd  26439  mapfzcons  26662  diophren  26764  irrapxlem1  26775  monotuz  26894  acongeq  26938  jm2.26lem3  26962  jm3.1lem2  26979  pw2f1ocnv  26998  psgnunilem4  27288  psgnghm  27305  matbas2i  27344  idomodle  27380  fcnre  27563  refsumcn  27568  rfcnnnub  27574  climsuselem1  27600  stoweidlem11  27627  stoweidlem15  27631  stoweidlem17  27633  stoweidlem20  27636  stoweidlem34  27650  stoweidlem35  27651  stoweidlem46  27662  stoweidlem47  27663  stoweidlem56  27672  stoweidlem59  27675  stoweidlem62  27678  stirlinglem5  27694  stirlinglem14  27703  bnj1172  29076  bnj1245  29089  bnj1311  29099  bnj1450  29125  bnj1501  29142  osumcllem7N  30444  pexmidlem4N  30455  lcfrlem4  32028  lcfrlem5  32029  lcfrlem6  32030  lcfrlem16  32041  lcfrlem38  32063  mapdrvallem2  32128  mapdh8ab  32260  mapdh8ad  32262  mapdh8e  32267

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400