Theorem syl6eleq 2698

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl6eleq.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
syl6eleq.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6eleq	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eleq

Step	Hyp	Ref	Expression
1		syl6eleq.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		syl6eleq.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2690	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  syl6eleqr  2699  3eltr3g  2704  prid2g  4240  ndmfvrcl  6129  fnwelem  7179  tz7.48-1  7425  brwitnlem  7474  oeeulem  7568  dffi3  8220  cnfcom3lem  8483  alephgeom  8788  fpwwe2lem6  9336  canthwelem  9351  hargch  9374  r1wunlim  9438  eluzel2  11568  fseq1p1m1  12283  fznn0sub2  12315  nn0split  12323  fz1fzo0m1  12383  exple1  12782  digit1  12860  bcval5  12967  bcpasc  12970  hashf1  13098  seqcoll  13105  seqcoll2  13106  ccatrn  13225  swrdccat1  13309  swrdccat2  13310  cats1un  13327  splfv2a  13358  splval2  13359  caubnd  13946  limsupgre  14060  clim2ser  14233  clim2ser2  14234  iserex  14235  isermulc2  14236  iserle  14238  iserge0  14239  climub  14240  climserle  14241  isercolllem2  14244  isercolllem3  14245  isercoll  14246  isercoll2  14247  serf0  14259  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  sumeq2ii  14271  summolem3  14292  summolem2a  14293  fsum  14298  sum0  14299  fsumcl2lem  14309  fsumadd  14317  isumclim3  14332  isumadd  14340  fsump1i  14342  fsummulc2  14358  fsumrelem  14380  iserabs  14388  cvgcmp  14389  cvgcmpub  14390  cvgcmpce  14391  binom1dif  14404  isumshft  14410  isumsplit  14411  isumrpcl  14414  isumsup2  14417  climcndslem1  14420  climcndslem2  14421  climcnds  14422  arisum2  14432  trireciplem  14433  geoser  14438  geolim  14440  geo2lim  14445  cvgrat  14454  mertenslem1  14455  mertenslem2  14456  mertens  14457  clim2prod  14459  clim2div  14460  ntrivcvgfvn0  14470  ntrivcvgtail  14471  prodeq2ii  14482  prodmolem3  14502  prodmolem2a  14503  fprod  14510  fprodntriv  14511  fprodss  14517  fprodser  14518  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodabs  14543  fprodeq0  14544  fprodn0  14548  iprodclim3  14570  iprodmul  14573  fallfacfwd  14606  0fallfac  14607  binomfallfaclem2  14610  fallfacval4  14613  bpolysum  14623  bpolydiflem  14624  fsumkthpow  14626  efcvgfsum  14655  efcj  14661  fprodefsum  14664  effsumlt  14680  ruclem7  14804  bitsfzolem  14994  bitsfzo  14995  bitsfi  14997  bitsinv1lem  15001  bitsinv1  15002  bitsinvp1  15009  sadcp1  15015  sadadd  15027  sadass  15031  bitsres  15033  smupp1  15040  smuval2  15042  smupval  15048  smueqlem  15050  smumul  15053  algrp1  15125  phiprmpw  15319  crth  15321  phimullem  15322  eulerthlem2  15325  prmdiv  15328  pcpremul  15386  pcmpt  15434  pcfac  15441  pockthlem  15447  pockthg  15448  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  prmrec  15464  1arith  15469  vdwapun  15516  vdwlem1  15523  vdwlem2  15524  vdwlem3  15525  vdwlem6  15528  vdwlem8  15530  vdwlem10  15532  vdw  15536  imasvscafn  16020  xpsfrnel2  16048  oppccatid  16202  oppccomfpropd  16210  brcic  16281  funcoppc  16358  invfuc  16457  hofcl  16722  yonedalem4c  16740  gsumwsubmcl  17198  gsumccat  17201  gsumwmhm  17205  mulgnnp1  17372  mulgnnsubcl  17376  mulgnn0z  17390  mulgnndir  17392  mulgnndirOLD  17393  psgnunilem4  17740  psgnran  17758  sylow1lem1  17836  lsmmod2  17912  lsmdisj2r  17921  efginvrel2  17963  efgsdmi  17968  efgsrel  17970  efgs1b  17972  efgsp1  17973  efgredleme  17979  efgredlemc  17981  efgcpbllemb  17991  frgpuplem  18008  mulgnn0di  18054  frgpnabllem1  18099  lt6abl  18119  cycsubgcyg  18125  gsumval3eu  18128  gsumval3  18131  gsumzcl2  18134  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  telgsumfz0s  18211  dprdwd  18233  dprd2da  18264  pgpfaclem1  18303  srgbinom  18368  isirred  18522  lspprid2  18819  lspsnat  18966  lsppratlem1  18968  lsppratlem3  18970  lidl0cl  19033  lidlacl  19034  lidlnegcl  19035  lidlmcl  19038  psrbaglefi  19193  psrass23l  19229  psrass23  19231  mplcoe5lem  19288  mpfind  19357  psr1bascl  19391  ply1basf  19393  gsummoncoe1  19495  lply1binom  19497  lply1binomsc  19498  mpfpf1  19536  pf1mpf  19537  evl1scvarpw  19548  psgnghm  19745  matbas2i  20047  matecld  20051  matgsum  20062  mpt2matmul  20071  dmatmul  20122  1mavmul  20173  mdetleib2  20213  m1detdiag  20222  marep01ma  20285  smadiadetlem4  20294  slesolinv  20305  pmatcollpw3fi1lem1  20410  chpscmat  20466  chpscmatgsumbin  20468  chp0mat  20470  chpidmat  20471  chfacfisf  20478  chfacfisfcpmat  20479  chfacfpmmulgsum2  20489  cldrcl  20640  ordtbas  20806  iscnp2  20853  dis1stc  21112  ptbasfi  21194  ptpjopn  21225  ptclsg  21228  ptcnp  21235  kqtop  21358  reghmph  21406  ptcmplem2  21667  ptcmplem3  21668  ptcmplem4  21669  tsmslem1  21742  utop2nei  21864  isucn2  21893  cuspcvg  21915  cnextucn  21917  imasdsf1olem  21988  blcvx  22409  xrhmeo  22553  cnrehmeo  22560  evth  22566  reparphti  22605  iscau4  22885  iscmet3lem1  22897  lmle  22907  rrxfsupp  22993  pjthlem2  23017  ovollb2lem  23063  ovolunlem1a  23071  ovoliunlem1  23077  ovoliun2  23081  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem4  23095  iundisj2  23124  voliunlem1  23125  volsup  23131  ioombl1lem4  23136  uniioovol  23153  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  vitalilem5  23187  mbfimaopnlem  23228  mbflimsup  23239  mbfi1fseqlem3  23290  iblitg  23341  dvnp1  23494  cpncn  23505  dvlip2  23562  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumrlimge0  23597  dvfsumrlim2  23599  ftc1cn  23610  elplyd  23762  ply1termlem  23763  ply1term  23764  ply0  23768  plyeq0lem  23770  plyaddlem1  23773  plymullem1  23774  plyaddlem  23775  plymullem  23776  coeeulem  23784  plyco  23801  coeeq2  23802  coefv0  23808  coemulhi  23814  coemulc  23815  plycj  23837  dvply1  23843  vieta1lem2  23870  elqaalem2  23879  dvtaylp  23928  dvntaylp  23929  taylthlem1  23931  taylth  23933  ulmres  23946  ulmshftlem  23947  ulmshft  23948  ulmcau  23953  ulmdvlem1  23958  mtest  23962  mtestbdd  23963  pserulm  23980  psercn2  23981  psercnlem1  23983  psercn  23984  pserdvlem2  23986  abelthlem6  23994  abelth  23999  efif1olem1  24092  efif1olem3  24094  efif1olem4  24095  logcn  24193  advlogexp  24201  efopn  24204  cxpeq  24298  asinsin  24419  atantayl  24464  leibpilem2  24468  birthdaylem2  24479  birthdaylem3  24480  efrlim  24496  emcllem2  24523  emcllem5  24526  emcllem7  24528  harmonicbnd4  24537  fsumharmonic  24538  lgamgulm2  24562  lgamcvglem  24566  lgamcvg2  24581  gamcvg2lem  24585  wilthlem2  24595  wilthlem3  24596  ftalem1  24599  ftalem2  24600  ftalem3  24601  ftalem5  24603  basellem2  24608  basellem3  24609  basellem5  24611  basellem8  24614  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  chpp1  24681  vma1  24692  ppiltx  24703  musum  24717  0sgmppw  24723  1sgmprm  24724  ppiublem2  24728  chtublem  24736  fsumvma2  24739  chpchtsum  24744  logexprlim  24750  bposlem5  24813  lgscllem  24829  lgsval2lem  24832  lgsval4a  24844  lgsneg  24846  lgsdir2lem3  24852  lgsdir2lem5  24854  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  gausslemma2dlem3  24893  lgseisenlem1  24900  lgsquadlem2  24906  chebbnd1lem1  24958  chtppilimlem1  24962  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrmusum2  24983  dchrvmasum2lem  24985  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0flb  24999  dchrisum0re  25002  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  mudivsum  25019  mulogsum  25021  mulog2sumlem2  25024  selberg2lem  25039  logdivbnd  25045  pntrsumo1  25054  pntrsumbnd2  25056  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem6a  25071  pntlemj  25092  pntlemf  25094  ostth2lem3  25124  tglngne  25245  ltgseg  25291  eedimeq  25578  axlowdimlem16  25637  ebtwntg  25662  eupares  26502  eupap1  26503  eupath2lem3  26506  eupath2  26507  htthlem  27158  hhsscms  27520  shmodsi  27632  pjoc1i  27674  5oalem1  27897  mayete3i  27971  adj1  28176  iundisj2f  28785  fcnvgreu  28855  ssnnssfz  28937  iundisj2fi  28943  pmtrto1cl  29180  psgnfzto1stlem  29181  fzto1st1  29183  1smat1  29198  submateqlem2  29202  lmatfval  29208  mdetlap1  29220  madjusmdetlem1  29221  madjusmdetlem2  29222  madjusmdetlem3  29223  madjusmdetlem4  29224  pnfneige0  29325  pl1cn  29329  rrhqima  29386  indpreima  29414  esumfzf  29458  esumpcvgval  29467  esumpmono  29468  esumcvg  29475  ldgenpisyslem1  29553  ldgenpisys  29556  measbase  29587  dya2iocnei  29671  oddpwdc  29743  eulerpartlems  29749  eulerpartlemb  29757  sseqf  29781  fibp1  29790  orrvcval4  29853  orrvcoel  29854  orrvccel  29855  ballotlem2  29877  ballotlemfrceq  29917  signsplypnf  29953  signswch  29964  signstf0  29971  signstfvn  29972  signstfvneq0  29975  signstfvcl  29976  signstfveq0  29980  signsvfn  29985  bnj1172  30323  bnj1245  30336  bnj1311  30346  bnj1450  30372  bnj1501  30389  subfacp1lem1  30415  subfacp1lem5  30420  subfacp1lem6  30421  subfacval2  30423  erdszelem7  30433  cvxscon  30479  cvmliftlem5  30525  cvmliftlem7  30527  cvmliftlem10  30530  cvmliftlem13  30532  mrsubvrs  30673  msubrn  30680  msubco  30682  msubvrs  30711  bdayelon  31079  imageval  31207  fwddifnp1  31442  knoppcnlem8  31660  knoppcnlem10  31662  icoreunrn  32383  istoprelowl  32384  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  mblfinlem2  32617  ftc1cnnc  32654  upixp  32694  sdclem2  32708  caushft  32727  ismtyres  32777  rrnmet  32798  rrndstprj1  32799  rrndstprj2  32800  rrncmslem  32801  rrnequiv  32804  iccbnd  32809  osumcllem7N  34266  pexmidlem4N  34277  lcfrlem4  35852  lcfrlem5  35853  lcfrlem6  35854  lcfrlem16  35865  lcfrlem38  35887  mapdrvallem2  35952  mapdh8ab  36084  mapdh8ad  36086  mapdh8e  36091  mapfzcons  36297  diophren  36395  irrapxlem1  36404  monotuz  36524  acongeq  36568  jm2.26lem3  36586  jm3.1lem2  36603  pw2f1ocnv  36622  idomodle  36793  trclfvdecomr  37039  imo72b2lem1  37493  dvgrat  37533  cvgdvgrat  37534  hashnzfz2  37542  fcnre  38207  refsumcn  38212  rfcnnnub  38218  disjf1o  38373  disjinfi  38375  ssmapsn  38403  ssuzfz  38506  nnsplit  38515  fsumsermpt  38646  climsuselem1  38674  limcperiod  38695  sumnnodd  38697  lptioo2cn  38712  lptioo1cn  38713  climresmpt  38726  allbutfifvre  38742  climleltrp  38743  cncfshift  38759  cncfperiod  38764  cncfshiftioo  38778  fperdvper  38808  dvnmptdivc  38828  dvnmul  38833  dvmptfprod  38835  dvnprodlem3  38838  stoweidlem11  38904  stoweidlem15  38908  stoweidlem17  38910  stoweidlem20  38913  stoweidlem34  38927  stoweidlem35  38928  stoweidlem46  38939  stoweidlem47  38940  stoweidlem56  38949  stoweidlem59  38952  stoweidlem62  38955  stirlinglem5  38971  stirlinglem14  38980  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  fourierdlem11  39011  fourierdlem15  39015  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem25  39025  fourierdlem48  39047  fourierdlem52  39051  fourierdlem54  39053  fourierdlem58  39057  fourierdlem62  39061  fourierdlem64  39063  fourierdlem65  39064  fourierdlem69  39068  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem80  39079  fourierdlem81  39080  fourierdlem83  39082  fourierdlem92  39091  fourierdlem93  39092  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  fouriercnp  39119  fouriersw  39124  elaa2lem  39126  etransclem4  39131  etransclem7  39134  etransclem10  39137  etransclem14  39141  etransclem15  39142  etransclem24  39151  etransclem25  39152  etransclem31  39158  etransclem32  39159  etransclem35  39162  etransclem44  39171  etransclem46  39173  qndenserrnopnlem  39193  qndenserrn  39195  prsal  39214  salgencntex  39237  subsaliuncl  39252  subsalsal  39253  sge0tsms  39273  sge0fodjrnlem  39309  sge0isum  39320  iundjiunlem  39352  iundjiun  39353  meadjiunlem  39358  meaiunlelem  39361  meaiuninclem  39373  meaiininc2  39378  caragensplit  39390  carageneld  39392  carageniuncllem1  39411  caratheodorylem1  39416  caratheodorylem2  39417  hoicvr  39438  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmvlelem2  39486  hoiqssbllem2  39513  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  smflimlem3  39659  smfmullem4  39679  elmod2  39950  pwdif  40039  subgruhgredgd  40508  subumgredg2  40509  umgrres1lem  40529  wlkson  40864  1wlksonproplem  40912  trlsonfval  40913  pthsonfval  40946  spthson  40947  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  eupth2lems  41406  ssnn0ssfz  41920  zlmodzxzscm  41928  rmsupp0  41943  lincsum  42012  lincscm  42013  lindslinindimp2lem4  42044  lincresunit3  42064  elbigofrcl  42142  setrec1  42237  aacllem  42356