MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eleq Structured version   Visualization version   GIF version

Theorem syl6eleq 2895
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
StepHypRef Expression
1 syl6eleq.1 . 2 (𝜑𝐴𝐵)
2 syl6eleq.2 . . 3 𝐵 = 𝐶
32a1i 11 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2887 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802
This theorem is referenced by:  syl6eleqr  2896  3eltr3g  2901  prid2g  4487  ndmfvrcl  6439  fnwelem  7526  tz7.48-1  7774  brwitnlem  7824  oeeulem  7918  dffi3  8576  cnfcom3lem  8847  alephgeom  9188  fpwwe2lem6  9742  canthwelem  9757  hargch  9780  r1wunlim  9844  eluzel2  11909  fseq1p1m1  12637  fznn0sub2  12670  nn0split  12678  fz1fzo0m1  12740  exple1  13143  digit1  13221  bcval5  13325  bcpasc  13328  hashf1  13458  seqcoll  13465  seqcoll2  13466  ccatrn  13586  swrdccat1  13681  swrdccat2  13682  cats1un  13699  splfv2a  13731  splval2  13732  caubnd  14321  limsupgre  14435  clim2ser  14608  clim2ser2  14609  iserex  14610  isermulc2  14611  iserle  14613  iserge0  14614  climub  14615  climserle  14616  isercolllem2  14619  isercolllem3  14620  isercoll  14621  isercoll2  14622  serf0  14634  iseraltlem2  14636  iseraltlem3  14637  iseralt  14638  sumeq2ii  14646  summolem3  14668  summolem2a  14669  fsum  14674  sum0  14675  fsumcl2lem  14685  fsumadd  14693  isumclim3  14713  isumadd  14721  fsump1i  14723  fsummulc2  14738  fsumrelem  14761  iserabs  14769  cvgcmp  14770  cvgcmpub  14771  cvgcmpce  14772  binom1dif  14787  isumshft  14793  isumsplit  14794  isumrpcl  14797  isumsup2  14800  climcndslem1  14803  climcndslem2  14804  climcnds  14805  arisum2  14815  trireciplem  14816  geoser  14821  geolim  14823  geo2lim  14828  cvgrat  14836  mertenslem1  14837  mertenslem2  14838  mertens  14839  clim2prod  14841  clim2div  14842  ntrivcvgfvn0  14852  ntrivcvgtail  14853  prodeq2ii  14864  prodmolem3  14884  prodmolem2a  14885  fprod  14892  fprodntriv  14893  fprodss  14899  fprodser  14900  fprodcl2lem  14901  fprodmul  14911  fproddiv  14912  fprodabs  14925  fprodeq0  14926  fprodn0  14930  iprodclim3  14951  iprodmul  14954  fallfacfwd  14987  0fallfac  14988  binomfallfaclem2  14991  fallfacval4  14994  bpolysum  15004  bpolydiflem  15005  fsumkthpow  15007  efcvgfsum  15036  efcj  15042  fprodefsum  15045  effsumlt  15061  ruclem7  15185  bitsfzolem  15375  bitsfzo  15376  bitsfi  15378  bitsinv1lem  15382  bitsinv1  15383  bitsinvp1  15390  sadcp1  15396  sadadd  15408  sadass  15412  bitsres  15414  smupp1  15421  smuval2  15423  smupval  15429  smueqlem  15431  smumul  15434  algrp1  15506  phiprmpw  15698  crth  15700  phimullem  15701  eulerthlem2  15704  prmdiv  15707  pcpremul  15765  pcmpt  15813  pcfac  15820  pockthlem  15826  pockthg  15827  prmreclem2  15838  prmreclem3  15839  prmreclem4  15840  prmreclem5  15841  prmreclem6  15842  prmrec  15843  1arith  15848  vdwapun  15895  vdwlem1  15902  vdwlem2  15903  vdwlem3  15904  vdwlem6  15907  vdwlem8  15909  vdwlem10  15911  vdw  15915  imasvscafn  16402  xpsfrnel2  16430  oppccatid  16583  oppccomfpropd  16591  brcic  16662  funcoppc  16739  invfuc  16838  hofcl  17104  yonedalem4c  17122  gsumwsubmcl  17580  gsumccat  17583  gsumwmhm  17587  mulgnnp1  17754  mulgnnsubcl  17758  mulgnn0z  17771  mulgnndir  17773  psgnunilem4  18118  psgnran  18136  sylow1lem1  18214  lsmmod2  18290  lsmdisj2r  18299  efginvrel2  18341  efgsdmi  18346  efgsrel  18348  efgs1b  18350  efgsp1  18351  efgredleme  18357  efgredlemc  18359  efgcpbllemb  18369  frgpuplem  18386  mulgnn0di  18432  frgpnabllem1  18477  lt6abl  18497  cycsubgcyg  18503  gsumval3eu  18506  gsumval3  18509  gsumzcl2  18512  gsumzaddlem  18522  gsumconst  18535  gsumzmhm  18538  gsumzoppg  18545  telgsumfz0s  18590  dprdwd  18612  dprd2da  18643  pgpfaclem1  18682  srgbinom  18747  isirred  18901  lspprid2  19205  lspsnat  19353  lsppratlem1  19356  lsppratlem3  19358  lidl0cl  19421  lidlacl  19422  lidlnegcl  19423  lidlmcl  19426  psrbaglefi  19581  psrass23l  19617  psrass23  19619  mplcoe5lem  19676  mpfind  19744  psr1bascl  19778  ply1basf  19780  gsummoncoe1  19882  lply1binom  19884  lply1binomsc  19885  mpfpf1  19923  pf1mpf  19924  evl1scvarpw  19935  psgnghm  20133  matbas2i  20438  matecld  20442  matgsum  20453  mpt2matmul  20463  dmatmul  20514  1mavmul  20565  mdetleib2  20605  m1detdiag  20614  marep01ma  20678  smadiadetlem4  20687  slesolinv  20698  pmatcollpw3fi1lem1  20804  chpscmat  20860  chpscmatgsumbin  20862  chp0mat  20864  chpidmat  20865  chfacfisf  20872  chfacfisfcpmat  20873  chfacfpmmulgsum2  20883  cldrcl  21044  ordtbas  21210  iscnp2  21257  dis1stc  21516  ptbasfi  21598  ptpjopn  21629  ptclsg  21632  ptcnp  21639  kqtop  21762  reghmph  21810  ptcmplem2  22070  ptcmplem3  22071  ptcmplem4  22072  tsmslem1  22145  utop2nei  22267  isucn2  22296  cuspcvg  22318  cnextucn  22320  imasdsf1olem  22391  blcvx  22814  xrhmeo  22958  cnrehmeo  22965  evth  22971  reparphti  23009  iscau4  23289  iscmet3lem1  23301  lmle  23311  rrxfsupp  23397  pjthlem2  23421  ovollb2lem  23469  ovolunlem1a  23477  ovoliunlem1  23483  ovoliun2  23487  ovolscalem1  23494  ovolicc1  23497  ovolicc2lem4  23501  iundisj2  23530  voliunlem1  23531  volsup  23537  ioombl1lem4  23542  uniioovol  23560  uniioombllem3  23566  uniioombllem4  23567  uniioombllem6  23569  vitalilem5  23593  mbfimaopnlem  23636  mbflimsup  23647  mbfi1fseqlem3  23698  iblitg  23749  dvnp1  23902  cpncn  23913  dvlip2  23972  dvfsumlem2  24004  dvfsumlem3  24005  dvfsumrlimge0  24007  dvfsumrlim2  24009  ftc1cn  24020  elplyd  24172  ply1termlem  24173  ply1term  24174  ply0  24178  plyeq0lem  24180  plyaddlem1  24183  plymullem1  24184  plyaddlem  24185  plymullem  24186  coeeulem  24194  plyco  24211  coeeq2  24212  coefv0  24218  coemulhi  24224  coemulc  24225  plycj  24247  dvply1  24253  vieta1lem2  24280  elqaalem2  24289  dvtaylp  24338  dvntaylp  24339  taylthlem1  24341  taylth  24343  ulmres  24356  ulmshftlem  24357  ulmshft  24358  ulmcau  24363  ulmdvlem1  24368  mtest  24372  mtestbdd  24373  pserulm  24390  psercn2  24391  psercnlem1  24393  psercn  24394  pserdvlem2  24396  abelthlem6  24404  abelth  24409  efif1olem1  24503  efif1olem3  24505  efif1olem4  24506  logcn  24607  advlogexp  24615  efopn  24618  cxpeq  24712  asinsin  24833  atantayl  24878  leibpilem2  24882  birthdaylem2  24893  birthdaylem3  24894  efrlim  24910  emcllem2  24937  emcllem5  24940  emcllem7  24942  harmonicbnd4  24951  fsumharmonic  24952  lgamgulm2  24976  lgamcvglem  24980  lgamcvg2  24995  gamcvg2lem  24999  wilthlem2  25009  wilthlem3  25010  ftalem1  25013  ftalem2  25014  ftalem3  25015  ftalem5  25017  basellem2  25022  basellem3  25023  basellem5  25025  basellem8  25028  ppiprm  25091  ppinprm  25092  chtprm  25093  chtnprm  25094  chpp1  25095  vma1  25106  ppiltx  25117  musum  25131  0sgmppw  25137  1sgmprm  25138  ppiublem2  25142  chtublem  25150  fsumvma2  25153  chpchtsum  25158  logexprlim  25164  bposlem5  25227  lgscllem  25243  lgsval2lem  25246  lgsval4a  25258  lgsneg  25260  lgsdir2lem3  25266  lgsdir2lem5  25268  lgsdir  25271  lgsdilem2  25272  lgsdi  25273  lgsne0  25274  gausslemma2dlem3  25307  lgseisenlem1  25314  lgsquadlem2  25320  chebbnd1lem1  25372  chtppilimlem1  25376  rplogsumlem2  25388  rpvmasumlem  25390  dchrisumlem1  25392  dchrisumlem2  25393  dchrmusum2  25397  dchrvmasum2lem  25399  dchrvmasumiflem1  25404  dchrisum0flblem1  25411  dchrisum0flblem2  25412  dchrisum0flb  25413  dchrisum0re  25416  dchrisum0lem1b  25418  dchrisum0lem1  25419  dchrisum0lem2a  25420  dchrisum0lem2  25421  dchrisum0lem3  25422  mudivsum  25433  mulogsum  25435  mulog2sumlem2  25438  selberg2lem  25453  logdivbnd  25459  pntrsumo1  25468  pntrsumbnd2  25470  pntrlog2bndlem2  25481  pntrlog2bndlem4  25483  pntrlog2bndlem6a  25485  pntlemj  25506  pntlemf  25508  ostth2lem3  25538  tglngne  25659  ltgseg  25705  eedimeq  25992  axlowdimlem16  26051  ebtwntg  26076  subgruhgredgd  26392  subumgredg2  26393  umgrres1lem  26418  wlkson  26780  wksonproplem  26829  trlsonfval  26830  pthsonfval  26864  spthson  26865  crctcshwlkn0lem4  26934  crctcshwlkn0lem5  26935  eupth2lems  27411  numclwwlk1lem2foa  27533  numclwlk1lem2  27550  numclwwlk2lem1  27556  numclwwlk2lem1OLD  27563  htthlem  28102  hhsscms  28464  shmodsi  28576  pjoc1i  28618  5oalem1  28841  mayete3i  28915  adj1  29120  iundisj2f  29728  fmptco1f1o  29761  fcnvgreu  29799  ssnnssfz  29876  iundisj2fi  29883  pmtrto1cl  30174  psgnfzto1stlem  30175  fzto1st1  30177  1smat1  30195  submateqlem2  30199  lmatfval  30205  mdetlap1  30217  madjusmdetlem1  30218  madjusmdetlem2  30219  madjusmdetlem3  30220  madjusmdetlem4  30221  pnfneige0  30322  pl1cn  30326  rrhqima  30383  indpreima  30412  esumfzf  30456  esumpcvgval  30465  esumpmono  30466  esumcvg  30473  ldgenpisyslem1  30551  ldgenpisys  30554  measbase  30585  dya2iocnei  30669  oddpwdc  30741  eulerpartlems  30747  eulerpartlemb  30755  sseqf  30779  fibp1  30788  orrvcval4  30851  orrvcoel  30852  orrvccel  30853  ballotlem2  30875  ballotlemfrceq  30915  signsplypnf  30952  signswch  30963  signstf0  30970  signstfvn  30971  signstfvneq0  30974  signstfvcl  30975  signstfveq0  30979  signsvfn  30984  fct2relem  31000  fsum2dsub  31010  reprsuc  31018  reprpmtf1o  31029  breprexplema  31033  breprexplemc  31035  hgt749d  31052  hgt750lemb  31059  tgoldbachgnn  31062  bnj1172  31392  bnj1245  31405  bnj1311  31415  bnj1450  31441  bnj1501  31458  subfacp1lem1  31484  subfacp1lem5  31489  subfacp1lem6  31490  subfacval2  31492  erdszelem7  31502  cvxsconn  31548  cvmliftlem5  31594  cvmliftlem7  31596  cvmliftlem10  31599  cvmliftlem13  31601  mrsubvrs  31742  msubrn  31749  msubco  31751  msubvrs  31780  imageval  32358  fwddifnp1  32593  knoppcnlem8  32807  knoppcnlem10  32809  icoreunrn  33523  istoprelowl  33524  poimirlem3  33725  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem12  33734  poimirlem15  33737  poimirlem16  33738  poimirlem17  33739  poimirlem18  33740  poimirlem19  33741  poimirlem20  33742  poimirlem21  33743  poimirlem22  33744  poimirlem23  33745  poimirlem24  33746  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  poimirlem28  33750  poimirlem29  33751  poimirlem31  33753  mblfinlem2  33760  ftc1cnnc  33796  upixp  33836  sdclem2  33849  caushft  33868  ismtyres  33918  rrnmet  33939  rrndstprj1  33940  rrndstprj2  33941  rrncmslem  33942  rrnequiv  33945  iccbnd  33950  osumcllem7N  35742  pexmidlem4N  35753  lcfrlem4  37326  lcfrlem5  37327  lcfrlem6  37328  lcfrlem16  37339  lcfrlem38  37361  mapdrvallem2  37426  mapdh8ab  37558  mapdh8ad  37560  mapdh8e  37565  mapfzcons  37781  diophren  37879  irrapxlem1  37888  monotuz  38007  acongeq  38051  jm2.26lem3  38069  jm3.1lem2  38086  pw2f1ocnv  38105  idomodle  38275  trclfvdecomr  38520  imo72b2lem1  38971  dvgrat  39011  cvgdvgrat  39012  hashnzfz2  39020  fcnre  39678  refsumcn  39683  rfcnnnub  39689  disjf1o  39867  disjinfi  39869  ssmapsn  39895  ssuzfz  40045  nnsplit  40054  uzssd2  40123  uzublem  40136  fsumsermpt  40291  climsuselem1  40319  limcperiod  40340  sumnnodd  40342  lptioo2cn  40357  lptioo1cn  40358  climresmpt  40371  allbutfifvre  40387  climleltrp  40388  cnrefiisplem  40535  cncfshift  40567  cncfperiod  40572  cncfshiftioo  40585  fperdvper  40613  dvnmptdivc  40633  dvnmul  40638  dvmptfprod  40640  dvnprodlem3  40643  stoweidlem11  40707  stoweidlem15  40711  stoweidlem17  40713  stoweidlem20  40716  stoweidlem34  40730  stoweidlem35  40731  stoweidlem46  40742  stoweidlem47  40743  stoweidlem56  40752  stoweidlem59  40755  stoweidlem62  40758  stirlinglem5  40774  stirlinglem14  40783  dirkertrigeqlem2  40795  dirkertrigeqlem3  40796  fourierdlem11  40814  fourierdlem15  40818  fourierdlem16  40819  fourierdlem21  40824  fourierdlem22  40825  fourierdlem25  40828  fourierdlem48  40850  fourierdlem52  40854  fourierdlem54  40856  fourierdlem58  40860  fourierdlem62  40864  fourierdlem64  40866  fourierdlem65  40867  fourierdlem69  40871  fourierdlem70  40872  fourierdlem71  40873  fourierdlem73  40875  fourierdlem80  40882  fourierdlem81  40883  fourierdlem83  40885  fourierdlem92  40894  fourierdlem93  40895  fourierdlem97  40899  fourierdlem103  40905  fourierdlem104  40906  fourierdlem112  40914  fourierdlem113  40915  fouriercnp  40922  fouriersw  40927  elaa2lem  40929  etransclem4  40934  etransclem7  40937  etransclem10  40940  etransclem14  40944  etransclem15  40945  etransclem24  40954  etransclem25  40955  etransclem31  40961  etransclem32  40962  etransclem35  40965  etransclem44  40974  etransclem46  40976  qndenserrnopnlem  40996  qndenserrn  40998  prsal  41017  salgencntex  41040  subsaliuncl  41055  subsalsal  41056  sge0tsms  41076  sge0fodjrnlem  41112  sge0isum  41123  iundjiunlem  41155  iundjiun  41156  meadjiunlem  41161  meaiunlelem  41164  meaiuninclem  41176  meaiininc2  41184  caragensplit  41196  carageneld  41198  carageniuncllem1  41217  caratheodorylem1  41222  caratheodorylem2  41223  hoicvr  41244  hsphoidmvle2  41281  hsphoidmvle  41282  hoidmv1lelem2  41288  hoidmv1lelem3  41289  hoidmvlelem2  41292  hoiqssbllem2  41319  pimdecfgtioc  41407  pimincfltioc  41408  pimdecfgtioo  41409  pimincfltioo  41410  smflimlem3  41463  smfmullem4  41483  smfsupxr  41504  smflimsuplem2  41509  smflimsuplem5  41512  elmod2  41915  pwdif  42076  ssnn0ssfz  42695  zlmodzxzscm  42703  rmsupp0  42717  lincsum  42786  lincscm  42787  lindslinindimp2lem4  42818  lincresunit3  42838  elbigofrcl  42912  setrec1  43006  aacllem  43118
  Copyright terms: Public domain W3C validator