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

Theorem syl6eleq 2525
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
StepHypRef Expression
1 syl6eleq.1 . 2  |-  ( ph  ->  A  e.  B )
2 syl6eleq.2 . . 3  |-  B  =  C
32a1i 11 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2511 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  syl6eleqr  2526  prid2g  3903  ndmfvrcl  5748  fnwelem  6453  tz7.48-1  6692  brwitnlem  6743  oeeulem  6836  dffi3  7428  cnfcom3lem  7652  alephgeom  7955  fpwwe2lem6  8502  canthwelem  8517  hargch  8544  r1wunlim  8604  eluzel2  10485  fznn0sub2  11078  fseq1p1m1  11114  exple1  11431  digit1  11505  bcval5  11601  bcpasc  11604  hashf1  11698  seqcoll  11704  seqcoll2  11705  swrdccat1  11766  swrdccat2  11767  splfv2a  11777  splval2  11778  cats1un  11782  caubnd  12154  limsupgre  12267  clim2ser  12440  clim2ser2  12441  iserex  12442  isermulc2  12443  iserle  12445  iserge0  12446  climub  12447  climserle  12448  isercolllem2  12451  isercolllem3  12452  isercoll  12453  isercoll2  12454  serf0  12466  iseraltlem2  12468  iseraltlem3  12469  iseralt  12470  sumeq2ii  12479  summolem3  12500  summolem2a  12501  fsum  12506  sum0  12507  fsumcl2lem  12517  fsumadd  12524  isumclim3  12535  isumadd  12543  fsump1i  12545  fsummulc2  12559  fsumrelem  12578  iserabs  12586  cvgcmp  12587  cvgcmpub  12588  cvgcmpce  12589  binom1dif  12604  isumshft  12611  isumsplit  12612  isumrpcl  12615  isumsup2  12618  climcndslem1  12621  climcndslem2  12622  climcnds  12623  arisum2  12632  trireciplem  12633  geoser  12638  geolim  12639  geo2lim  12644  cvgrat  12652  mertenslem1  12653  mertenslem2  12654  mertens  12655  efcvgfsum  12680  efcj  12686  effsumlt  12704  ruclem7  12827  bitsfzolem  12938  bitsfzo  12939  bitsfi  12941  bitsinv1lem  12945  bitsinv1  12946  bitsinvp1  12953  sadcp1  12959  sadadd  12971  sadass  12975  bitsres  12977  smupp1  12984  smuval2  12986  smupval  12992  smueqlem  12994  smumul  12997  algrp1  13057  phiprmpw  13157  crt  13159  phimullem  13160  eulerthlem2  13163  prmdiv  13166  pcpremul  13209  pcmpt  13253  pcfac  13260  pockthlem  13265  pockthg  13266  prmreclem2  13277  prmreclem3  13278  prmreclem4  13279  prmreclem5  13280  prmreclem6  13281  prmrec  13282  1arith  13287  vdwapun  13334  vdwlem1  13341  vdwlem2  13342  vdwlem3  13343  vdwlem6  13346  vdwlem8  13348  vdwlem10  13350  vdw  13354  imasvscafn  13754  xpsfrnel2  13782  oppccatid  13937  oppccomfpropd  13945  funcoppc  14064  invfuc  14163  hofcl  14348  yonedalem4c  14366  gsumwsubmcl  14776  gsumccat  14779  gsumwmhm  14782  mulgnnp1  14890  mulgnnsubcl  14894  mulgnn0z  14902  mulgnndir  14904  sylow1lem1  15224  lsmmod2  15300  lsmdisj2r  15309  efginvrel2  15351  efgsdmi  15356  efgsrel  15358  efgs1b  15360  efgsp1  15361  efgredleme  15367  efgredlemc  15369  efgcpbllemb  15379  frgpuplem  15396  mulgnn0di  15440  frgpnabllem1  15476  lt6abl  15496  cycsubgcyg  15502  gsumval3eu  15505  gsumval3  15506  gsumzcl  15510  gsumzaddlem  15518  gsumconst  15524  gsumzmhm  15525  gsumzoppg  15531  dprd2da  15592  pgpfaclem1  15631  isirred  15796  lspprid2  16066  lspsnat  16209  lsppratlem1  16211  lsppratlem3  16213  lidl0cl  16275  lidlacl  16276  lidlnegcl  16277  lidlmcl  16280  psrbaglefi  16429  psrass23  16465  psr1bascl  16590  ply1basf  16592  cldrcl  17082  ordtbas  17248  iscnp2  17295  dis1stc  17554  ptbasfi  17605  ptpjopn  17636  ptclsg  17639  ptcnp  17646  kqtop  17769  reghmph  17817  ptcmplem2  18076  ptcmplem3  18077  ptcmplem4  18078  tsmslem1  18150  utop2nei  18272  isucn2  18301  cuspcvg  18323  cnextucn  18325  imasdsf1olem  18395  blcvx  18821  xrhmeo  18963  cnrehmeo  18970  evth  18976  reparphti  19014  iscau4  19224  iscmet3lem1  19236  lmle  19246  pjthlem2  19331  ovollb2lem  19376  ovolunlem1a  19384  ovoliunlem1  19390  ovoliun2  19394  ovolscalem1  19401  ovolicc1  19404  ovolicc2lem4  19408  iundisj2  19435  voliunlem1  19436  volsup  19442  ioombl1lem4  19447  uniioovol  19463  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  vitalilem5  19496  mbfimaopnlem  19539  mbflimsup  19550  mbfi1fseqlem3  19601  iblitg  19652  dvnp1  19803  cpncn  19814  dvlip2  19871  dvfsumlem2  19903  dvfsumlem3  19904  dvfsumrlimge0  19906  dvfsumrlim2  19908  ftc1cn  19919  mpfind  19957  mpfpf1  19963  pf1mpf  19964  elplyd  20113  ply1termlem  20114  ply1term  20115  ply0  20119  plyeq0lem  20121  plyaddlem1  20124  plymullem1  20125  plyaddlem  20126  plymullem  20127  coeeulem  20135  plyco  20152  coeeq2  20153  coefv0  20158  coemulhi  20164  coemulc  20165  plycj  20187  dvply1  20193  vieta1lem2  20220  elqaalem2  20229  dvtaylp  20278  dvntaylp  20279  taylthlem1  20281  taylth  20283  ulmres  20296  ulmshftlem  20297  ulmshft  20298  ulmcau  20303  ulmdvlem1  20308  mtest  20312  mtestbdd  20313  pserulm  20330  psercn2  20331  psercnlem1  20333  psercn  20334  pserdvlem2  20336  abelthlem6  20344  abelth  20349  efif1olem1  20436  efif1olem3  20438  efif1olem4  20439  logcn  20530  advlogexp  20538  efopn  20541  cxpeq  20633  asinsin  20724  atantayl  20769  leibpilem2  20773  birthdaylem2  20783  birthdaylem3  20784  efrlim  20800  emcllem2  20827  emcllem5  20830  emcllem7  20832  harmonicbnd4  20841  fsumharmonic  20842  wilthlem2  20844  wilthlem3  20845  ftalem1  20847  ftalem2  20848  ftalem3  20849  ftalem5  20851  basellem2  20856  basellem3  20857  basellem5  20859  basellem8  20862  ppiprm  20926  ppinprm  20927  chtprm  20928  chtnprm  20929  chpp1  20930  vma1  20941  ppiltx  20952  musum  20968  0sgmppw  20974  1sgmprm  20975  ppiublem2  20979  chtublem  20987  fsumvma2  20990  chpchtsum  20995  logexprlim  21001  bposlem5  21064  lgscllem  21079  lgsval2lem  21082  lgsval4a  21094  lgsneg  21095  lgsdir2lem3  21101  lgsdir2lem5  21103  lgsdir  21106  lgsdilem2  21107  lgsdi  21108  lgsne0  21109  lgseisenlem1  21125  lgsquadlem2  21131  chebbnd1lem1  21155  chtppilimlem1  21159  rplogsumlem2  21171  rpvmasumlem  21173  dchrisumlem1  21175  dchrisumlem2  21176  dchrmusum2  21180  dchrvmasum2lem  21182  dchrvmasumiflem1  21187  dchrisum0flblem1  21194  dchrisum0flblem2  21195  dchrisum0flb  21196  dchrisum0re  21199  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  mudivsum  21216  mulogsum  21218  mulog2sumlem2  21221  selberg2lem  21236  logdivbnd  21242  pntrsumo1  21251  pntrsumbnd2  21253  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  pntrlog2bndlem6a  21268  pntlemj  21289  pntlemf  21291  ostth2lem3  21321  eupares  21689  eupap1  21690  eupath2lem3  21693  eupath2  21694  htthlem  22412  hhsscms  22771  shmodsi  22883  pjoc1i  22925  5oalem1  23148  mayete3i  23222  mayete3iOLD  23223  adj1  23428  iundisj2f  24022  ssnnssfz  24140  iundisj2fi  24145  pnfneige0  24328  indpreima  24414  esumfzf  24451  esumpcvgval  24460  esumpmono  24461  esumcvg  24468  measbase  24543  dya2iocnei  24624  orrvcval4  24714  orrvcoel  24715  orrvccel  24716  ballotlem2  24738  ballotlemfrceq  24778  lgamgulm2  24812  lgamcvglem  24816  lgamcvg2  24831  gamcvg2lem  24835  subfacp1lem1  24857  subfacp1lem5  24862  subfacp1lem6  24863  subfacval2  24865  erdszelem7  24875  cvxscon  24922  cvmliftlem5  24968  cvmliftlem7  24970  cvmliftlem10  24973  cvmliftlem13  24975  relexpsucr  25122  clim2prod  25208  clim2div  25209  ntrivcvgfvn0  25219  ntrivcvgtail  25220  prodeq2ii  25231  prodmolem3  25251  prodmolem2a  25252  fprod  25259  fprodntriv  25260  fprodss  25266  fprodser  25267  fprodcl2lem  25268  fprodmul  25276  fproddiv  25277  fprodabs  25289  fprodefsum  25290  fprodeq0  25291  fprodn0  25295  iprodclim3  25305  iprodmul  25308  fallfacfwd  25344  0fallfac  25345  binomfallfaclem2  25348  fallfacval4  25351  bdayelon  25627  imageval  25767  eedimeq  25829  axlowdimlem16  25888  bpolysum  26091  bpolydiflem  26092  fsumkthpow  26094  mblfinlem  26234  ftc1cnnc  26269  upixp  26422  sdclem2  26437  caushft  26458  ismtyres  26508  rrnmet  26529  rrndstprj1  26530  rrndstprj2  26531  rrncmslem  26532  rrnequiv  26535  iccbnd  26540  mapfzcons  26763  diophren  26865  irrapxlem1  26876  monotuz  26995  acongeq  27039  jm2.26lem3  27063  jm3.1lem2  27080  pw2f1ocnv  27099  psgnunilem4  27388  psgnghm  27405  matbas2i  27444  idomodle  27480  fcnre  27663  refsumcn  27668  rfcnnnub  27674  climsuselem1  27700  stoweidlem11  27727  stoweidlem15  27731  stoweidlem17  27733  stoweidlem20  27736  stoweidlem34  27750  stoweidlem35  27751  stoweidlem46  27762  stoweidlem47  27763  stoweidlem56  27772  stoweidlem59  27775  stoweidlem62  27778  stirlinglem5  27794  stirlinglem14  27803  bnj1172  29307  bnj1245  29320  bnj1311  29330  bnj1450  29356  bnj1501  29373  osumcllem7N  30696  pexmidlem4N  30707  lcfrlem4  32280  lcfrlem5  32281  lcfrlem6  32282  lcfrlem16  32293  lcfrlem38  32315  mapdrvallem2  32380  mapdh8ab  32512  mapdh8ad  32514  mapdh8e  32519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator