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

Theorem syl6eleq 2386
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 10 . 2  |-  ( ph  ->  B  =  C )
41, 3eleqtrd 2372 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696
This theorem is referenced by:  syl6eleqr  2387  prid2g  3746  ndmfvrcl  5569  fnwelem  6246  tz7.48-1  6471  brwitnlem  6522  oeeulem  6615  dffi3  7200  cnfcom3lem  7422  alephgeom  7725  fpwwe2lem6  8273  canthwelem  8288  hargch  8315  r1wunlim  8375  eluzel2  10251  fznn0sub2  10841  fseq1p1m1  10873  exple1  11177  digit1  11251  bcval5  11346  bcpasc  11349  hashf1  11411  seqcoll  11417  seqcoll2  11418  swrdccat1  11476  swrdccat2  11477  splfv2a  11487  splval2  11488  cats1un  11492  caubnd  11858  limsupgre  11971  clim2ser  12144  clim2ser2  12145  iserex  12146  isermulc2  12147  iserle  12149  iserge0  12150  climub  12151  climserle  12152  isercolllem2  12155  isercolllem3  12156  isercoll  12157  isercoll2  12158  serf0  12169  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  sumeq2ii  12182  summolem3  12203  summolem2a  12204  fsum  12209  sum0  12210  fsumcl2lem  12220  fsumadd  12227  isumclim3  12238  isumadd  12246  fsump1i  12248  fsummulc2  12262  fsumrelem  12281  iserabs  12289  cvgcmp  12290  cvgcmpub  12291  cvgcmpce  12292  binom1dif  12307  isumshft  12314  isumsplit  12315  isumrpcl  12318  isumsup2  12321  climcndslem1  12324  climcndslem2  12325  climcnds  12326  arisum2  12335  trireciplem  12336  geoser  12341  geolim  12342  geo2lim  12347  cvgrat  12355  mertenslem1  12356  mertenslem2  12357  mertens  12358  efcvgfsum  12383  efcj  12389  effsumlt  12407  ruclem7  12530  bitsfzolem  12641  bitsfzo  12642  bitsfi  12644  bitsinv1lem  12648  bitsinv1  12649  bitsinvp1  12656  sadcp1  12662  sadadd  12674  sadass  12678  bitsres  12680  smupp1  12687  smuval2  12689  smupval  12695  smueqlem  12697  smumul  12700  algrp1  12760  phiprmpw  12860  crt  12862  phimullem  12863  eulerthlem2  12866  prmdiv  12869  pcpremul  12912  pcmpt  12956  pcfac  12963  pockthlem  12968  pockthg  12969  prmreclem2  12980  prmreclem3  12981  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  prmrec  12985  1arith  12990  vdwapun  13037  vdwlem1  13044  vdwlem2  13045  vdwlem3  13046  vdwlem6  13049  vdwlem8  13051  vdwlem10  13053  vdw  13057  imasvscafn  13455  xpsfrnel2  13483  oppccatid  13638  oppccomfpropd  13646  funcoppc  13765  invfuc  13864  hofcl  14049  yonedalem4c  14067  gsumwsubmcl  14477  gsumccat  14480  gsumwmhm  14483  mulgnnp1  14591  mulgnnsubcl  14595  mulgnn0z  14603  mulgnndir  14605  sylow1lem1  14925  lsmmod2  15001  lsmdisj2r  15010  efginvrel2  15052  efgsdmi  15057  efgsrel  15059  efgs1b  15061  efgsp1  15062  efgredleme  15068  efgredlemc  15070  efgcpbllemb  15080  frgpuplem  15097  mulgnn0di  15141  frgpnabllem1  15177  lt6abl  15197  cycsubgcyg  15203  gsumval3eu  15206  gsumval3  15207  gsumzcl  15211  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  dprd2da  15293  pgpfaclem1  15332  isirred  15497  lspprid2  15771  lspsnat  15914  lsppratlem1  15916  lsppratlem3  15918  lidl0cl  15980  lidlacl  15981  lidlnegcl  15982  lidlmcl  15985  psrbaglefi  16134  psrass23  16170  psr1bascl  16296  ply1basf  16299  cldrcl  16779  ordtbas  16938  iscnp2  16985  dis1stc  17241  ptbasfi  17292  ptpjopn  17322  ptclsg  17325  ptcnp  17332  kqtop  17452  reghmph  17500  ptcmplem2  17763  ptcmplem3  17764  ptcmplem4  17765  tsmslem1  17827  imasdsf1olem  17953  blcvx  18320  xrhmeo  18460  cnrehmeo  18467  evth  18473  reparphti  18511  iscau4  18721  iscmet3lem1  18733  lmle  18743  pjthlem2  18818  ovollb2lem  18863  ovolunlem1a  18871  ovoliunlem1  18877  ovoliun2  18881  ovolscalem1  18888  ovolicc1  18891  ovolicc2lem4  18895  iundisj2  18922  voliunlem1  18923  volsup  18929  ioombl1lem4  18934  uniioovol  18950  uniioombllem3  18956  uniioombllem4  18957  uniioombllem6  18959  vitalilem5  18983  mbfimaopnlem  19026  mbflimsup  19037  mbfi1fseqlem3  19088  iblitg  19139  dvnp1  19290  cpncn  19301  dvlip2  19358  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumrlimge0  19393  dvfsumrlim2  19395  ftc1cn  19406  mpfind  19444  mpfpf1  19450  pf1mpf  19451  elplyd  19600  ply1termlem  19601  ply1term  19602  ply0  19606  plyeq0lem  19608  plyaddlem1  19611  plymullem1  19612  plyaddlem  19613  plymullem  19614  coeeulem  19622  plyco  19639  coeeq2  19640  coefv0  19645  coemulhi  19651  coemulc  19652  plycj  19674  dvply1  19680  vieta1lem2  19707  elqaalem2  19716  dvtaylp  19765  dvntaylp  19766  taylthlem1  19768  taylth  19770  ulmres  19783  ulmshftlem  19784  ulmshft  19785  ulmcau  19788  ulmdvlem1  19793  mtest  19797  pserulm  19814  psercn2  19815  psercnlem1  19817  psercn  19818  pserdvlem2  19820  abelthlem6  19828  abelth  19833  efif1olem1  19920  efif1olem3  19922  efif1olem4  19923  logcn  20010  advlogexp  20018  efopn  20021  cxpeq  20113  asinsin  20204  atantayl  20249  leibpilem2  20253  birthdaylem2  20263  birthdaylem3  20264  efrlim  20280  emcllem2  20306  emcllem5  20309  emcllem7  20311  harmonicbnd4  20320  fsumharmonic  20321  wilthlem2  20323  wilthlem3  20324  ftalem1  20326  ftalem2  20327  ftalem3  20328  ftalem5  20330  basellem2  20335  basellem3  20336  basellem5  20338  basellem8  20341  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  chpp1  20409  vma1  20420  ppiltx  20431  musum  20447  0sgmppw  20453  1sgmprm  20454  ppiublem2  20458  chtublem  20466  fsumvma2  20469  chpchtsum  20474  logexprlim  20480  bposlem5  20543  lgscllem  20558  lgsval2lem  20561  lgsval4a  20573  lgsneg  20574  lgsdir2lem3  20580  lgsdir2lem5  20582  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  lgseisenlem1  20604  lgsquadlem2  20610  chebbnd1lem1  20634  chtppilimlem1  20638  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlem1  20654  dchrisumlem2  20655  dchrmusum2  20659  dchrvmasum2lem  20661  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0flblem2  20674  dchrisum0flb  20675  dchrisum0re  20678  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  mudivsum  20695  mulogsum  20697  mulog2sumlem2  20700  selberg2lem  20715  logdivbnd  20721  pntrsumo1  20730  pntrsumbnd2  20732  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  pntrlog2bndlem6a  20747  pntlemj  20768  pntlemf  20770  ostth2lem3  20800  htthlem  21513  hhsscms  21872  shmodsi  21984  pjoc1i  22026  5oalem1  22249  mayete3i  22323  mayete3iOLD  22324  adj1  22529  ballotlemfrceq  23103  ssnnssfz  23292  iundisj2fi  23379  iundisj2f  23381  pnfneige0  23389  esumpcvgval  23461  esumpmono  23462  esumcvg  23469  indpreima  23623  orrvcval4  23680  orrvcoel  23681  orrvccel  23682  dmgmseqn0  23711  subfacp1lem1  23725  subfacp1lem5  23730  subfacp1lem6  23731  subfacval2  23733  erdszelem7  23743  cvxscon  23789  cvmliftlem5  23835  cvmliftlem7  23837  cvmliftlem10  23840  cvmliftlem13  23842  eupares  23914  eupap1  23915  eupath2lem3  23918  eupath2  23919  relexpsucr  24041  cprodeq2ii  24135  prodmolem3  24156  prodmolem2a  24157  fprod  24164  bdayelon  24405  imageval  24540  eedimeq  24598  axlowdimlem16  24657  bpolysum  24860  bpolydiflem  24861  fsumkthpow  24863  ftc1cnnc  25025  npincppr  25262  inposet  25381  exopcopn  25675  isray  26257  isside0  26267  aishp  26275  upixp  26506  sdclem2  26555  caushft  26580  ismtyres  26635  rrnmet  26656  rrndstprj1  26657  rrndstprj2  26658  rrncmslem  26659  rrnequiv  26662  iccbnd  26667  mapfzcons  26896  diophren  26999  irrapxlem1  27010  monotuz  27129  acongeq  27173  jm2.26lem3  27197  jm3.1lem2  27214  pw2f1ocnv  27233  psgnunilem4  27523  psgnghm  27540  matbas2i  27579  idomodle  27615  fcnre  27799  refsumcn  27804  rfcnnnub  27810  climsuselem1  27836  stoweidlem11  27863  stoweidlem15  27867  stoweidlem17  27869  stoweidlem20  27872  stoweidlem34  27886  stoweidlem47  27899  stoweidlem56  27908  stoweidlem59  27911  stoweidlem62  27914  stirlinglem5  27930  bnj1172  29347  bnj1245  29360  bnj1311  29370  bnj1450  29396  bnj1501  29413  osumcllem7N  30773  pexmidlem4N  30784  lcfrlem4  32357  lcfrlem5  32358  lcfrlem6  32359  lcfrlem16  32370  lcfrlem38  32392  mapdrvallem2  32457  mapdh8ab  32589  mapdh8ad  32591  mapdh8e  32596
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator