Theorem syl6eleq 2871

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 2863	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2766  df-clel 2841

This theorem is referenced by:  syl6eleqr  2872  3eltr3g  2877  prid2g  4568  ndmfvrcl  6528  fnwelem  7629  tz7.48-1  7881  brwitnlem  7933  oeeulem  8027  dffi3  8689  cnfcom3lem  8959  alephgeom  9301  fpwwe2lem6  9854  canthwelem  9869  hargch  9892  r1wunlim  9956  eluzel2  12062  fseq1p1m1  12796  fznn0sub2  12829  nn0split  12837  exple1  13354  digit1  13412  bcval5  13492  bcpasc  13495  hashf1  13627  seqcoll  13634  seqcoll2  13635  ccatrn  13751  swrdccat1OLD  13849  swrdccat2  13850  cats1un  13913  splfv2a  13972  splfv2aOLD  13973  splval2  13974  splval2OLD  13975  caubnd  14578  limsupgre  14698  clim2ser  14871  clim2ser2  14872  iserex  14873  isermulc2  14874  iserle  14876  iserge0  14877  climub  14878  climserle  14879  isercolllem2  14882  isercolllem3  14883  isercoll  14884  isercoll2  14885  serf0  14897  iseraltlem2  14899  iseraltlem3  14900  iseralt  14901  sumeq2ii  14909  summolem3  14930  summolem2a  14931  fsum  14936  sum0  14937  fsumcl2lem  14947  fsumadd  14955  isumclim3  14973  isumadd  14981  fsump1i  14983  fsummulc2  14998  fsumrelem  15021  iserabs  15029  cvgcmp  15030  cvgcmpub  15031  cvgcmpce  15032  binom1dif  15047  isumshft  15053  isumsplit  15054  isumrpcl  15057  isumsup2  15060  climcndslem1  15063  climcndslem2  15064  climcnds  15065  arisum2  15075  trireciplem  15076  geoser  15081  pwdif  15082  geolim  15085  geo2lim  15090  cvgrat  15098  mertenslem1  15099  mertenslem2  15100  mertens  15101  clim2prod  15103  clim2div  15104  ntrivcvgfvn0  15114  ntrivcvgtail  15115  prodeq2ii  15126  prodmolem3  15146  prodmolem2a  15147  fprod  15154  fprodntriv  15155  fprodss  15161  fprodser  15162  fprodcl2lem  15163  fprodmul  15173  fproddiv  15174  fprodabs  15187  fprodeq0  15188  fprodn0  15192  iprodclim3  15213  iprodmul  15216  fallfacfwd  15249  0fallfac  15250  binomfallfaclem2  15253  fallfacval4  15256  bpolysum  15266  bpolydiflem  15267  fsumkthpow  15269  efcvgfsum  15298  efcj  15304  fprodefsum  15307  effsumlt  15323  ruclem7  15448  bitsfzolem  15642  bitsfzo  15643  bitsfi  15645  bitsinv1lem  15649  bitsinv1  15650  bitsinvp1  15657  sadcp1  15663  sadadd  15675  sadass  15679  bitsres  15681  smupp1  15688  smuval2  15690  smupval  15696  smueqlem  15698  smumul  15701  algrp1  15773  phiprmpw  15968  crth  15970  phimullem  15971  eulerthlem2  15974  prmdiv  15977  pcpremul  16035  pcmpt  16083  pcfac  16090  pockthlem  16096  pockthg  16097  prmreclem2  16108  prmreclem3  16109  prmreclem4  16110  prmreclem5  16111  prmreclem6  16112  prmrec  16113  1arith  16118  vdwapun  16165  vdwlem1  16172  vdwlem2  16173  vdwlem3  16174  vdwlem6  16177  vdwlem8  16179  vdwlem10  16181  vdw  16185  imasvscafn  16665  xpsfrnel2cda  16699  oppccatid  16860  oppccomfpropd  16868  brcic  16939  funcoppc  17016  invfuc  17115  hofcl  17380  yonedalem4c  17398  gsumwsubmcl  17856  gsumccat  17859  gsumwmhm  17864  mulgnnp1  18034  mulgnnsubcl  18038  mulgnn0z  18051  mulgnndir  18053  psgnunilem4  18400  psgnran  18418  sylow1lem1  18497  lsmmod2  18573  lsmdisj2r  18582  efginvrel2  18624  efgsdmi  18629  efgsrel  18631  efgs1b  18633  efgsp1  18634  efgredleme  18641  efgredlemc  18643  efgcpbllemb  18654  frgpuplem  18671  mulgnn0di  18717  frgpnabllem1  18762  lt6abl  18782  cycsubgcyg  18788  gsumval3eu  18791  gsumval3  18794  gsumzcl2  18797  gsumzaddlem  18807  gsumconst  18820  gsumzmhm  18823  gsumzoppg  18830  telgsumfz0s  18874  dprdwd  18896  dprd2da  18927  pgpfaclem1  18966  srgbinom  19031  isirred  19185  lspprid2  19505  lspsnat  19652  lsppratlem1  19654  lsppratlem3  19656  lidl0cl  19719  lidlacl  19720  lidlnegcl  19721  lidlmcl  19724  psrbaglefi  19879  psrass23l  19915  psrass23  19917  mplcoe5lem  19974  mpfind  20042  mhpinvcl  20058  mhpvscacl  20060  psr1bascl  20087  ply1basf  20089  gsummoncoe1  20191  lply1binom  20193  lply1binomsc  20194  mpfpf1  20232  pf1mpf  20233  evl1scvarpw  20244  psgnghm  20442  frlmvscavalb  20632  frlmvplusgscavalb  20633  matbas2i  20751  matecld  20755  matgsum  20766  mpomatmul  20775  dmatmul  20826  1mavmul  20877  mdetleib2  20917  m1detdiag  20926  marep01ma  20989  smadiadetlem4  20998  slesolinv  21009  pmatcollpw3fi1lem1  21114  chpscmat  21170  chpscmatgsumbin  21172  chp0mat  21174  chpidmat  21175  chfacfisf  21182  chfacfisfcpmat  21183  chfacfpmmulgsum2  21193  cldrcl  21354  ordtbas  21520  iscnp2  21567  dis1stc  21827  ptbasfi  21909  ptpjopn  21940  ptclsg  21943  ptcnp  21950  kqtop  22073  reghmph  22121  ptcmplem2  22381  ptcmplem3  22382  ptcmplem4  22383  tsmslem1  22456  utop2nei  22578  isucn2  22607  cuspcvg  22629  cnextucn  22631  imasdsf1olem  22702  blcvx  23125  xrhmeo  23269  cnrehmeo  23276  evth  23282  reparphti  23320  iscau4  23601  iscmet3lem1  23613  lmle  23623  rrxfsupp  23724  rrxdsfi  23733  pjthlem2  23760  ovollb2lem  23808  ovolunlem1a  23816  ovoliunlem1  23822  ovoliun2  23826  ovolscalem1  23833  ovolicc1  23836  ovolicc2lem4  23840  iundisj2  23869  voliunlem1  23870  volsup  23876  ioombl1lem4  23881  uniioovol  23899  uniioombllem3  23905  uniioombllem4  23906  uniioombllem6  23908  vitalilem5  23932  mbfimaopnlem  23975  mbflimsup  23986  mbfi1fseqlem3  24037  iblitg  24088  dvnp1  24241  cpncn  24252  dvlip2  24311  dvfsumlem2  24343  dvfsumlem3  24344  dvfsumrlimge0  24346  dvfsumrlim2  24348  ftc1cn  24359  elplyd  24511  ply1termlem  24512  ply1term  24513  ply0  24517  plyeq0lem  24519  plyaddlem1  24522  plymullem1  24523  plyaddlem  24524  plymullem  24525  coeeulem  24533  plyco  24550  coeeq2  24551  coefv0  24557  coemulhi  24563  coemulc  24564  plycj  24586  dvply1  24592  vieta1lem2  24619  elqaalem2  24628  dvtaylp  24677  dvntaylp  24678  taylthlem1  24680  taylth  24682  ulmres  24695  ulmshftlem  24696  ulmshft  24697  ulmcau  24702  ulmdvlem1  24707  mtest  24711  mtestbdd  24712  pserulm  24729  psercn2  24730  psercnlem1  24732  psercn  24733  pserdvlem2  24735  abelthlem6  24743  abelth  24748  efif1olem1  24843  efif1olem3  24845  efif1olem4  24846  logcn  24947  advlogexp  24955  efopn  24958  cxpeq  25055  asinsin  25187  atantayl  25232  leibpilem2  25237  birthdaylem2  25248  birthdaylem3  25249  efrlim  25265  emcllem2  25292  emcllem5  25295  emcllem7  25297  harmonicbnd4  25306  fsumharmonic  25307  lgamgulm2  25331  lgamcvglem  25335  lgamcvg2  25350  gamcvg2lem  25354  wilthlem2  25364  wilthlem3  25365  ftalem1  25368  ftalem2  25369  ftalem3  25370  ftalem5  25372  basellem2  25377  basellem3  25378  basellem5  25380  basellem8  25383  ppiprm  25446  ppinprm  25447  chtprm  25448  chtnprm  25449  chpp1  25450  vma1  25461  ppiltx  25472  musum  25486  0sgmppw  25492  1sgmprm  25493  ppiublem2  25497  chtublem  25505  fsumvma2  25508  chpchtsum  25513  logexprlim  25519  bposlem5  25582  lgscllem  25598  lgsval2lem  25601  lgsval4a  25613  lgsneg  25615  lgsdir2lem3  25621  lgsdir2lem5  25623  lgsdir  25626  lgsdilem2  25627  lgsdi  25628  lgsne0  25629  gausslemma2dlem3  25662  lgseisenlem1  25669  lgsquadlem2  25675  chebbnd1lem1  25763  chtppilimlem1  25767  rplogsumlem2  25779  rpvmasumlem  25781  dchrisumlem1  25783  dchrisumlem2  25784  dchrmusum2  25788  dchrvmasum2lem  25790  dchrvmasumiflem1  25795  dchrisum0flblem1  25802  dchrisum0flblem2  25803  dchrisum0flb  25804  dchrisum0re  25807  dchrisum0lem1b  25809  dchrisum0lem1  25810  dchrisum0lem2a  25811  dchrisum0lem2  25812  dchrisum0lem3  25813  mudivsum  25824  mulogsum  25826  mulog2sumlem2  25829  selberg2lem  25844  logdivbnd  25850  pntrsumo1  25859  pntrsumbnd2  25861  pntrlog2bndlem2  25872  pntrlog2bndlem4  25874  pntrlog2bndlem6a  25876  pntlemj  25897  pntlemf  25899  ostth2lem3  25929  tglngne  26054  ltgseg  26100  eedimeq  26403  axlowdimlem16  26462  ebtwntg  26487  subgruhgredgd  26785  subumgredg2  26786  umgrres1lem  26811  wlkson  27156  wksonproplem  27210  trlsonfval  27211  pthsonfval  27245  spthson  27246  crctcshwlkn0lem4  27315  crctcshwlkn0lem5  27316  eupth2lems  27784  numclwwlk1lem2foa  27911  numclwwlk1lem2foaOLD  27912  numclwlk1lem2  27939  numclwwlk2lem1  27945  htthlem  28489  hhsscms  28851  shmodsi  28963  pjoc1i  29005  5oalem1  29228  mayete3i  29302  adj1  29507  iundisj2f  30124  fmptco1f1o  30158  fcnvgreu  30198  suppovss  30205  ssnnssfz  30287  iundisj2fi  30294  cshw1s2  30394  cycpmfv1  30476  cycpmfv2  30477  cyc3evpm  30496  cyc3genpm  30498  lindsun  30683  fldextfld1  30701  fldextfld2  30702  pmtrto1cl  30723  psgnfzto1stlem  30724  fzto1st1  30726  1smat1  30744  submateqlem2  30748  lmatfval  30754  mdetlap1  30766  madjusmdetlem1  30767  madjusmdetlem2  30768  madjusmdetlem3  30769  madjusmdetlem4  30770  pnfneige0  30871  pl1cn  30875  rrhqima  30932  indpreima  30961  esumfzf  31005  esumpcvgval  31014  esumpmono  31015  esumcvg  31022  ldgenpisyslem1  31100  ldgenpisys  31103  measbase  31134  dya2iocnei  31218  oddpwdc  31290  eulerpartlems  31296  eulerpartlemb  31304  sseqf  31329  fibp1  31338  orrvcval4  31401  orrvcoel  31402  orrvccel  31403  ballotlem2  31425  ballotlemfrceq  31465  signsplypnf  31499  signswch  31510  signstf0  31517  signstfvn  31518  signstfvneq0  31522  signstfvcl  31523  signstfveq0  31527  signstfveq0OLD  31528  signsvfn  31533  fct2relem  31549  fsum2dsub  31559  reprsuc  31567  reprpmtf1o  31578  breprexplema  31582  breprexplemc  31584  hgt749d  31601  hgt750lemb  31608  tgoldbachgnn  31611  bnj1172  31951  bnj1245  31964  bnj1311  31974  bnj1450  32000  bnj1501  32017  subfacp1lem1  32044  subfacp1lem5  32049  subfacp1lem6  32050  subfacval2  32052  erdszelem7  32062  cvxsconn  32108  cvmliftlem5  32154  cvmliftlem7  32156  cvmliftlem10  32159  cvmliftlem13  32161  mrsubvrs  32322  msubrn  32329  msubco  32331  msubvrs  32360  imageval  32945  fwddifnp1  33180  knoppcnlem8  33392  knoppcnlem10  33394  icoreunrn  34115  istoprelowl  34116  poimirlem3  34369  poimirlem4  34370  poimirlem6  34372  poimirlem7  34373  poimirlem8  34374  poimirlem12  34378  poimirlem15  34381  poimirlem16  34382  poimirlem17  34383  poimirlem18  34384  poimirlem19  34385  poimirlem20  34386  poimirlem21  34387  poimirlem22  34388  poimirlem23  34389  poimirlem24  34390  poimirlem25  34391  poimirlem26  34392  poimirlem27  34393  poimirlem28  34394  poimirlem29  34395  poimirlem31  34397  mblfinlem2  34404  ftc1cnnc  34440  upixp  34479  sdclem2  34492  caushft  34511  ismtyres  34561  rrnmet  34582  rrndstprj1  34583  rrndstprj2  34584  rrncmslem  34585  rrnequiv  34588  iccbnd  34593  osumcllem7N  36576  pexmidlem4N  36587  lcfrlem4  38159  lcfrlem5  38160  lcfrlem6  38161  lcfrlem16  38172  lcfrlem38  38194  mapdrvallem2  38259  mapdh8ab  38391  mapdh8ad  38393  mapdh8e  38398  mapfzcons  38742  diophren  38840  irrapxlem1  38849  monotuz  38968  acongeq  39010  jm2.26lem3  39028  jm3.1lem2  39045  pw2f1ocnv  39064  idomodle  39226  trclfvdecomr  39470  imo72b2lem1  39920  scottelrankd  39992  dvgrat  40094  cvgdvgrat  40095  hashnzfz2  40103  fcnre  40735  refsumcn  40740  rfcnnnub  40746  disjf1o  40907  disjinfi  40909  ssmapsn  40935  ssuzfz  41076  nnsplit  41085  uzssd2  41152  uzublem  41165  fsumsermpt  41321  climsuselem1  41349  limcperiod  41370  sumnnodd  41372  lptioo2cn  41387  lptioo1cn  41388  climresmpt  41401  allbutfifvre  41417  climleltrp  41418  cnrefiisplem  41571  cncfshift  41617  cncfperiod  41622  cncfshiftioo  41635  fperdvper  41663  dvnmptdivc  41683  dvnmul  41688  dvmptfprod  41690  dvnprodlem3  41693  stoweidlem11  41757  stoweidlem15  41761  stoweidlem17  41763  stoweidlem20  41766  stoweidlem34  41780  stoweidlem35  41781  stoweidlem46  41792  stoweidlem47  41793  stoweidlem56  41802  stoweidlem59  41805  stoweidlem62  41808  stirlinglem5  41824  stirlinglem14  41833  dirkertrigeqlem2  41845  dirkertrigeqlem3  41846  fourierdlem11  41864  fourierdlem15  41868  fourierdlem16  41869  fourierdlem21  41874  fourierdlem22  41875  fourierdlem25  41878  fourierdlem48  41900  fourierdlem52  41904  fourierdlem54  41906  fourierdlem58  41910  fourierdlem62  41914  fourierdlem64  41916  fourierdlem65  41917  fourierdlem69  41921  fourierdlem70  41922  fourierdlem71  41923  fourierdlem73  41925  fourierdlem80  41932  fourierdlem81  41933  fourierdlem83  41935  fourierdlem92  41944  fourierdlem93  41945  fourierdlem97  41949  fourierdlem103  41955  fourierdlem104  41956  fourierdlem112  41964  fourierdlem113  41965  fouriercnp  41972  fouriersw  41977  elaa2lem  41979  etransclem4  41984  etransclem7  41987  etransclem10  41990  etransclem14  41994  etransclem15  41995  etransclem24  42004  etransclem25  42005  etransclem31  42011  etransclem32  42012  etransclem35  42015  etransclem44  42024  etransclem46  42026  qndenserrnopnlem  42043  qndenserrn  42045  prsal  42064  salgencntex  42087  subsaliuncl  42102  subsalsal  42103  sge0tsms  42123  sge0fodjrnlem  42159  sge0isum  42170  iundjiunlem  42202  iundjiun  42203  meadjiunlem  42208  meaiunlelem  42211  meaiuninclem  42223  meaiininc2  42231  caragensplit  42243  carageneld  42245  carageniuncllem1  42264  caratheodorylem1  42269  caratheodorylem2  42270  hoicvr  42291  hsphoidmvle2  42328  hsphoidmvle  42329  hoidmv1lelem2  42335  hoidmv1lelem3  42336  hoidmvlelem2  42339  hoiqssbllem2  42366  pimdecfgtioc  42454  pimincfltioc  42455  pimdecfgtioo  42456  pimincfltioo  42457  smflimlem3  42510  smfmullem4  42530  smfsupxr  42551  smflimsuplem2  42556  smflimsuplem5  42559  elmod2  42966  ssnn0ssfz  43791  zlmodzxzscm  43799  rmsupp0  43812  lincsum  43881  lincscm  43882  lindslinindimp2lem4  43913  lincresunit3  43933  elbigofrcl  44008  setrec1  44191  aacllem  44299