Theorem syl6eleq 2500

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

Syntax hints:   -> wi 4   = wceq 1405   e. wcel 1842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397

This theorem is referenced by:  syl6eleqr  2501  3eltr3g  2506  prid2g  4078  ndmfvrcl  5830  fnwelem  6853  tz7.48-1  7065  brwitnlem  7114  oeeulem  7207  dffi3  7845  cnfcom3lem  8099  cnfcom3lemOLD  8107  alephgeom  8415  fpwwe2lem6  8963  canthwelem  8978  hargch  9001  r1wunlim  9065  eluzel2  11050  fseq1p1m1  11724  fznn0sub2  11753  nn0split  11762  exple1  12180  digit1  12254  bcval5  12350  bcpasc  12353  hashf1  12462  seqcoll  12468  seqcoll2  12469  ccatrn  12567  swrdccat1  12645  swrdccat2  12646  cats1un  12664  splfv2a  12695  splval2  12696  caubnd  13247  limsupgre  13360  clim2ser  13533  clim2ser2  13534  iserex  13535  isermulc2  13536  iserle  13538  iserge0  13539  climub  13540  climserle  13541  isercolllem2  13544  isercolllem3  13545  isercoll  13546  isercoll2  13547  serf0  13559  iseraltlem2  13561  iseraltlem3  13562  iseralt  13563  sumeq2ii  13571  summolem3  13592  summolem2a  13593  fsum  13598  sum0  13599  fsumcl2lem  13609  fsumadd  13617  isumclim3  13632  isumadd  13640  fsump1i  13642  fsummulc2  13657  fsumrelem  13679  iserabs  13687  cvgcmp  13688  cvgcmpub  13689  cvgcmpce  13690  binom1dif  13703  isumshft  13709  isumsplit  13710  isumrpcl  13713  isumsup2  13716  climcndslem1  13719  climcndslem2  13720  climcnds  13721  arisum2  13731  trireciplem  13732  geoser  13737  geolim  13738  geo2lim  13743  cvgrat  13751  mertenslem1  13752  mertenslem2  13753  mertens  13754  clim2prod  13756  clim2div  13757  ntrivcvgfvn0  13767  ntrivcvgtail  13768  prodeq2ii  13779  prodmolem3  13799  prodmolem2a  13800  fprod  13807  fprodntriv  13808  fprodss  13814  fprodser  13815  fprodcl2lem  13816  fprodmul  13824  fproddiv  13825  fprodabs  13837  fprodeq0  13838  fprodn0  13842  iprodclim3  13852  iprodmul  13855  fallfacfwd  13888  0fallfac  13889  binomfallfaclem2  13892  fallfacval4  13895  efcvgfsum  13922  efcj  13928  fprodefsum  13931  effsumlt  13947  ruclem7  14070  bitsfzolem  14185  bitsfzo  14186  bitsfi  14188  bitsinv1lem  14192  bitsinv1  14193  bitsinvp1  14200  sadcp1  14206  sadadd  14218  sadass  14222  bitsres  14224  smupp1  14231  smuval2  14233  smupval  14239  smueqlem  14241  smumul  14244  algrp1  14304  phiprmpw  14407  crt  14409  phimullem  14410  eulerthlem2  14413  prmdiv  14416  pcpremul  14468  pcmpt  14512  pcfac  14519  pockthlem  14524  pockthg  14525  prmreclem2  14536  prmreclem3  14537  prmreclem4  14538  prmreclem5  14539  prmreclem6  14540  prmrec  14541  1arith  14546  vdwapun  14593  vdwlem1  14600  vdwlem2  14601  vdwlem3  14602  vdwlem6  14605  vdwlem8  14607  vdwlem10  14609  vdw  14613  imasvscafn  15043  xpsfrnel2  15071  oppccatid  15224  oppccomfpropd  15232  brcic  15303  funcoppc  15380  invfuc  15479  hofcl  15744  yonedalem4c  15762  gsumwsubmcl  16222  gsumccat  16225  gsumwmhm  16229  mulgnnp1  16366  mulgnnsubcl  16370  mulgnn0z  16378  mulgnndir  16380  psgnunilem4  16738  psgnran  16756  sylow1lem1  16834  lsmmod2  16910  lsmdisj2r  16919  efginvrel2  16961  efgsdmi  16966  efgsrel  16968  efgs1b  16970  efgsp1  16971  efgredleme  16977  efgredlemc  16979  efgcpbllemb  16989  frgpuplem  17006  mulgnn0di  17050  frgpnabllem1  17093  lt6abl  17113  cycsubgcyg  17119  gsumval3eu  17123  gsumval3OLD  17124  gsumval3  17127  gsumzcl2  17131  gsumzclOLD  17135  gsumzaddlem  17150  gsumzaddlemOLD  17152  gsumconst  17169  gsumzmhm  17172  gsumzmhmOLD  17173  gsumzoppg  17182  gsumzoppgOLD  17183  telgsumfz0s  17232  dprdwd  17256  dprd2da  17303  pgpfaclem1  17344  srgbinom  17408  isirred  17560  lspprid2  17856  lspsnat  18003  lsppratlem1  18005  lsppratlem3  18007  lidl0cl  18071  lidlacl  18072  lidlnegcl  18073  lidlmcl  18077  psrbaglefi  18235  psrbaglefiOLD  18236  psrass23l  18275  psrass23  18277  mplcoe5lem  18342  mpfind  18417  psr1bascl  18451  ply1basf  18453  gsummoncoe1  18558  lply1binom  18560  lply1binomsc  18561  mpfpf1  18599  pf1mpf  18600  evl1scvarpw  18611  psgnghm  18806  matbas2i  19108  matecld  19112  matgsum  19123  mpt2matmul  19132  dmatmul  19183  1mavmul  19234  mdetleib2  19274  m1detdiag  19283  marep01ma  19346  smadiadetlem4  19355  slesolinv  19366  pmatcollpw3fi1lem1  19471  chpscmat  19527  chpscmatgsumbin  19529  chp0mat  19531  chpidmat  19532  chfacfisf  19539  chfacfisfcpmat  19540  chfacfpmmulgsum2  19550  cldrcl  19711  ordtbas  19878  iscnp2  19925  dis1stc  20184  ptbasfi  20266  ptpjopn  20297  ptclsg  20300  ptcnp  20307  kqtop  20430  reghmph  20478  ptcmplem2  20737  ptcmplem3  20738  ptcmplem4  20739  tsmslem1  20811  utop2nei  20937  isucn2  20966  cuspcvg  20988  cnextucn  20990  imasdsf1olem  21060  blcvx  21487  xrhmeo  21630  cnrehmeo  21637  evth  21643  reparphti  21681  iscau4  21902  iscmet3lem1  21914  lmle  21924  rrxfsupp  22013  pjthlem2  22037  ovollb2lem  22083  ovolunlem1a  22091  ovoliunlem1  22097  ovoliun2  22101  ovolscalem1  22108  ovolicc1  22111  ovolicc2lem4  22115  iundisj2  22143  voliunlem1  22144  volsup  22150  ioombl1lem4  22155  uniioovol  22172  uniioombllem3  22178  uniioombllem4  22179  uniioombllem6  22181  vitalilem5  22205  mbfimaopnlem  22246  mbflimsup  22257  mbfi1fseqlem3  22308  iblitg  22359  dvnp1  22512  cpncn  22523  dvlip2  22580  dvfsumlem2  22612  dvfsumlem3  22613  dvfsumrlimge0  22615  dvfsumrlim2  22617  ftc1cn  22628  elplyd  22783  ply1termlem  22784  ply1term  22785  ply0  22789  plyeq0lem  22791  plyaddlem1  22794  plymullem1  22795  plyaddlem  22796  plymullem  22797  coeeulem  22805  plyco  22822  coeeq2  22823  coefv0  22829  coemulhi  22835  coemulc  22836  plycj  22858  dvply1  22864  vieta1lem2  22891  elqaalem2  22900  dvtaylp  22949  dvntaylp  22950  taylthlem1  22952  taylth  22954  ulmres  22967  ulmshftlem  22968  ulmshft  22969  ulmcau  22974  ulmdvlem1  22979  mtest  22983  mtestbdd  22984  pserulm  23001  psercn2  23002  psercnlem1  23004  psercn  23005  pserdvlem2  23007  abelthlem6  23015  abelth  23020  efif1olem1  23113  efif1olem3  23115  efif1olem4  23116  logcn  23214  advlogexp  23222  efopn  23225  cxpeq  23319  asinsin  23440  atantayl  23485  leibpilem2  23489  birthdaylem2  23500  birthdaylem3  23501  efrlim  23517  emcllem2  23544  emcllem5  23547  emcllem7  23549  harmonicbnd4  23558  fsumharmonic  23559  lgamgulm2  23583  lgamcvglem  23587  lgamcvg2  23602  gamcvg2lem  23606  wilthlem2  23616  wilthlem3  23617  ftalem1  23619  ftalem2  23620  ftalem3  23621  ftalem5  23623  basellem2  23628  basellem3  23629  basellem5  23631  basellem8  23634  ppiprm  23698  ppinprm  23699  chtprm  23700  chtnprm  23701  chpp1  23702  vma1  23713  ppiltx  23724  musum  23740  0sgmppw  23746  1sgmprm  23747  ppiublem2  23751  chtublem  23759  fsumvma2  23762  chpchtsum  23767  logexprlim  23773  bposlem5  23836  lgscllem  23851  lgsval2lem  23854  lgsval4a  23866  lgsneg  23867  lgsdir2lem3  23873  lgsdir2lem5  23875  lgsdir  23878  lgsdilem2  23879  lgsdi  23880  lgsne0  23881  lgseisenlem1  23897  lgsquadlem2  23903  chebbnd1lem1  23927  chtppilimlem1  23931  rplogsumlem2  23943  rpvmasumlem  23945  dchrisumlem1  23947  dchrisumlem2  23948  dchrmusum2  23952  dchrvmasum2lem  23954  dchrvmasumiflem1  23959  dchrisum0flblem1  23966  dchrisum0flblem2  23967  dchrisum0flb  23968  dchrisum0re  23971  dchrisum0lem1b  23973  dchrisum0lem1  23974  dchrisum0lem2a  23975  dchrisum0lem2  23976  dchrisum0lem3  23977  mudivsum  23988  mulogsum  23990  mulog2sumlem2  23993  selberg2lem  24008  logdivbnd  24014  pntrsumo1  24023  pntrsumbnd2  24025  pntrlog2bndlem2  24036  pntrlog2bndlem4  24038  pntrlog2bndlem6a  24040  pntlemj  24061  pntlemf  24063  ostth2lem3  24093  tglngne  24212  ltgseg  24258  eedimeq  24499  axlowdimlem16  24558  ebtwntg  24583  eupares  25273  eupap1  25274  eupath2lem3  25277  eupath2  25278  htthlem  26128  hhsscms  26489  shmodsi  26601  pjoc1i  26643  5oalem1  26866  mayete3i  26940  adj1  27145  iundisj2f  27762  fcnvgreu  27837  ssnnssfz  27925  iundisj2fi  27930  pnfneige0  28266  pl1cn  28270  indpreima  28352  esumfzf  28396  esumpcvgval  28405  esumpmono  28406  esumcvg  28413  ldgenpisyslem1  28491  ldgenpisys  28494  measbase  28525  dya2iocnei  28610  oddpwdc  28679  eulerpartlems  28685  eulerpartlemb  28693  sseqf  28717  fibp1  28726  orrvcval4  28789  orrvcoel  28790  orrvccel  28791  ballotlem2  28813  ballotlemfrceq  28853  signsplypnf  28893  signswch  28904  signstf0  28911  signstfvn  28912  signstfvneq0  28915  signstfvcl  28916  signstfveq0  28920  signsvfn  28925  bnj1172  29265  bnj1245  29278  bnj1311  29288  bnj1450  29314  bnj1501  29331  subfacp1lem1  29357  subfacp1lem5  29362  subfacp1lem6  29363  subfacval2  29365  erdszelem7  29375  cvxscon  29421  cvmliftlem5  29467  cvmliftlem7  29469  cvmliftlem10  29472  cvmliftlem13  29474  mrsubvrs  29615  msubrn  29622  msubco  29624  msubvrs  29653  bdayelon  30113  imageval  30241  bpolysum  30476  bpolydiflem  30477  fsumkthpow  30479  fwddifnp1  30491  icoreunrn  31264  istoprelowl  31265  mblfinlem2  31405  ftc1cnnc  31443  upixp  31483  sdclem2  31498  caushft  31517  ismtyres  31567  rrnmet  31588  rrndstprj1  31589  rrndstprj2  31590  rrncmslem  31591  rrnequiv  31594  iccbnd  31599  osumcllem7N  32960  pexmidlem4N  32971  lcfrlem4  34546  lcfrlem5  34547  lcfrlem6  34548  lcfrlem16  34559  lcfrlem38  34581  mapdrvallem2  34646  mapdh8ab  34778  mapdh8ad  34780  mapdh8e  34785  mapfzcons  34991  diophren  35089  irrapxlem1  35100  monotuz  35219  acongeq  35263  jm2.26lem3  35286  jm3.1lem2  35303  pw2f1ocnv  35322  idomodle  35498  trclfvdecomr  35688  imo72b2lem1  35980  dvgrat  36022  cvgdvgrat  36023  hashnzfz2  36055  fcnre  36761  refsumcn  36766  rfcnnnub  36772  climsuselem1  36963  limcperiod  36984  sumnnodd  36986  lptioo2cn  37001  lptioo1cn  37002  cncfshift  37026  cncfperiod  37031  cncfshiftioo  37045  fperdvper  37065  dvnmptdivc  37085  dvnmul  37090  dvmptfprod  37092  dvnprodlem3  37095  stoweidlem11  37143  stoweidlem15  37147  stoweidlem17  37149  stoweidlem20  37152  stoweidlem34  37166  stoweidlem35  37167  stoweidlem46  37178  stoweidlem47  37179  stoweidlem56  37188  stoweidlem59  37191  stoweidlem62  37194  stirlinglem5  37210  stirlinglem14  37219  dirkertrigeqlem2  37231  dirkertrigeqlem3  37232  fourierdlem11  37250  fourierdlem15  37254  fourierdlem16  37255  fourierdlem21  37260  fourierdlem22  37261  fourierdlem25  37264  fourierdlem48  37287  fourierdlem52  37291  fourierdlem54  37293  fourierdlem58  37297  fourierdlem62  37301  fourierdlem64  37303  fourierdlem65  37304  fourierdlem69  37308  fourierdlem70  37309  fourierdlem71  37310  fourierdlem73  37312  fourierdlem80  37319  fourierdlem81  37320  fourierdlem83  37322  fourierdlem92  37331  fourierdlem93  37332  fourierdlem97  37336  fourierdlem103  37342  fourierdlem104  37343  fourierdlem112  37351  fourierdlem113  37352  fouriercnp  37359  fouriersw  37364  elaa2lem  37366  etransclem4  37371  etransclem7  37374  etransclem10  37377  etransclem14  37381  etransclem15  37382  etransclem24  37391  etransclem25  37392  etransclem31  37398  etransclem32  37399  etransclem35  37402  etransclem44  37411  etransclem46  37413  elmod2  37655  ssnn0ssfz  38429  zlmodzxzscm  38437  rmsupp0  38452  lincsum  38521  lincscm  38522  lindslinindimp2lem4  38553  lincresunit3  38573  elbigofrcl  38661  aacllem  38840