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

Theorem syl6eleq 2470
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 2456 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717
This theorem is referenced by:  syl6eleqr  2471  prid2g  3847  ndmfvrcl  5689  fnwelem  6390  tz7.48-1  6629  brwitnlem  6680  oeeulem  6773  dffi3  7364  cnfcom3lem  7586  alephgeom  7889  fpwwe2lem6  8436  canthwelem  8451  hargch  8478  r1wunlim  8538  eluzel2  10418  fznn0sub2  11011  fseq1p1m1  11045  exple1  11359  digit1  11433  bcval5  11529  bcpasc  11532  hashf1  11626  seqcoll  11632  seqcoll2  11633  swrdccat1  11694  swrdccat2  11695  splfv2a  11705  splval2  11706  cats1un  11710  caubnd  12082  limsupgre  12195  clim2ser  12368  clim2ser2  12369  iserex  12370  isermulc2  12371  iserle  12373  iserge0  12374  climub  12375  climserle  12376  isercolllem2  12379  isercolllem3  12380  isercoll  12381  isercoll2  12382  serf0  12394  iseraltlem2  12396  iseraltlem3  12397  iseralt  12398  sumeq2ii  12407  summolem3  12428  summolem2a  12429  fsum  12434  sum0  12435  fsumcl2lem  12445  fsumadd  12452  isumclim3  12463  isumadd  12471  fsump1i  12473  fsummulc2  12487  fsumrelem  12506  iserabs  12514  cvgcmp  12515  cvgcmpub  12516  cvgcmpce  12517  binom1dif  12532  isumshft  12539  isumsplit  12540  isumrpcl  12543  isumsup2  12546  climcndslem1  12549  climcndslem2  12550  climcnds  12551  arisum2  12560  trireciplem  12561  geoser  12566  geolim  12567  geo2lim  12572  cvgrat  12580  mertenslem1  12581  mertenslem2  12582  mertens  12583  efcvgfsum  12608  efcj  12614  effsumlt  12632  ruclem7  12755  bitsfzolem  12866  bitsfzo  12867  bitsfi  12869  bitsinv1lem  12873  bitsinv1  12874  bitsinvp1  12881  sadcp1  12887  sadadd  12899  sadass  12903  bitsres  12905  smupp1  12912  smuval2  12914  smupval  12920  smueqlem  12922  smumul  12925  algrp1  12985  phiprmpw  13085  crt  13087  phimullem  13088  eulerthlem2  13091  prmdiv  13094  pcpremul  13137  pcmpt  13181  pcfac  13188  pockthlem  13193  pockthg  13194  prmreclem2  13205  prmreclem3  13206  prmreclem4  13207  prmreclem5  13208  prmreclem6  13209  prmrec  13210  1arith  13215  vdwapun  13262  vdwlem1  13269  vdwlem2  13270  vdwlem3  13271  vdwlem6  13274  vdwlem8  13276  vdwlem10  13278  vdw  13282  imasvscafn  13682  xpsfrnel2  13710  oppccatid  13865  oppccomfpropd  13873  funcoppc  13992  invfuc  14091  hofcl  14276  yonedalem4c  14294  gsumwsubmcl  14704  gsumccat  14707  gsumwmhm  14710  mulgnnp1  14818  mulgnnsubcl  14822  mulgnn0z  14830  mulgnndir  14832  sylow1lem1  15152  lsmmod2  15228  lsmdisj2r  15237  efginvrel2  15279  efgsdmi  15284  efgsrel  15286  efgs1b  15288  efgsp1  15289  efgredleme  15295  efgredlemc  15297  efgcpbllemb  15307  frgpuplem  15324  mulgnn0di  15368  frgpnabllem1  15404  lt6abl  15424  cycsubgcyg  15430  gsumval3eu  15433  gsumval3  15434  gsumzcl  15438  gsumzaddlem  15446  gsumconst  15452  gsumzmhm  15453  gsumzoppg  15459  dprd2da  15520  pgpfaclem1  15559  isirred  15724  lspprid2  15994  lspsnat  16137  lsppratlem1  16139  lsppratlem3  16141  lidl0cl  16203  lidlacl  16204  lidlnegcl  16205  lidlmcl  16208  psrbaglefi  16357  psrass23  16393  psr1bascl  16518  ply1basf  16520  cldrcl  17006  ordtbas  17171  iscnp2  17218  dis1stc  17476  ptbasfi  17527  ptpjopn  17558  ptclsg  17561  ptcnp  17568  kqtop  17691  reghmph  17739  ptcmplem2  17998  ptcmplem3  17999  ptcmplem4  18000  tsmslem1  18072  utop2nei  18194  isucn2  18223  cuspcvg  18245  cnextucn  18247  imasdsf1olem  18304  blcvx  18693  xrhmeo  18835  cnrehmeo  18842  evth  18848  reparphti  18886  iscau4  19096  iscmet3lem1  19108  lmle  19118  pjthlem2  19199  ovollb2lem  19244  ovolunlem1a  19252  ovoliunlem1  19258  ovoliun2  19262  ovolscalem1  19269  ovolicc1  19272  ovolicc2lem4  19276  iundisj2  19303  voliunlem1  19304  volsup  19310  ioombl1lem4  19315  uniioovol  19331  uniioombllem3  19337  uniioombllem4  19338  uniioombllem6  19340  vitalilem5  19364  mbfimaopnlem  19407  mbflimsup  19418  mbfi1fseqlem3  19469  iblitg  19520  dvnp1  19671  cpncn  19682  dvlip2  19739  dvfsumlem2  19771  dvfsumlem3  19772  dvfsumrlimge0  19774  dvfsumrlim2  19776  ftc1cn  19787  mpfind  19825  mpfpf1  19831  pf1mpf  19832  elplyd  19981  ply1termlem  19982  ply1term  19983  ply0  19987  plyeq0lem  19989  plyaddlem1  19992  plymullem1  19993  plyaddlem  19994  plymullem  19995  coeeulem  20003  plyco  20020  coeeq2  20021  coefv0  20026  coemulhi  20032  coemulc  20033  plycj  20055  dvply1  20061  vieta1lem2  20088  elqaalem2  20097  dvtaylp  20146  dvntaylp  20147  taylthlem1  20149  taylth  20151  ulmres  20164  ulmshftlem  20165  ulmshft  20166  ulmcau  20171  ulmdvlem1  20176  mtest  20180  mtestbdd  20181  pserulm  20198  psercn2  20199  psercnlem1  20201  psercn  20202  pserdvlem2  20204  abelthlem6  20212  abelth  20217  efif1olem1  20304  efif1olem3  20306  efif1olem4  20307  logcn  20398  advlogexp  20406  efopn  20409  cxpeq  20501  asinsin  20592  atantayl  20637  leibpilem2  20641  birthdaylem2  20651  birthdaylem3  20652  efrlim  20668  emcllem2  20695  emcllem5  20698  emcllem7  20700  harmonicbnd4  20709  fsumharmonic  20710  wilthlem2  20712  wilthlem3  20713  ftalem1  20715  ftalem2  20716  ftalem3  20717  ftalem5  20719  basellem2  20724  basellem3  20725  basellem5  20727  basellem8  20730  ppiprm  20794  ppinprm  20795  chtprm  20796  chtnprm  20797  chpp1  20798  vma1  20809  ppiltx  20820  musum  20836  0sgmppw  20842  1sgmprm  20843  ppiublem2  20847  chtublem  20855  fsumvma2  20858  chpchtsum  20863  logexprlim  20869  bposlem5  20932  lgscllem  20947  lgsval2lem  20950  lgsval4a  20962  lgsneg  20963  lgsdir2lem3  20969  lgsdir2lem5  20971  lgsdir  20974  lgsdilem2  20975  lgsdi  20976  lgsne0  20977  lgseisenlem1  20993  lgsquadlem2  20999  chebbnd1lem1  21023  chtppilimlem1  21027  rplogsumlem2  21039  rpvmasumlem  21041  dchrisumlem1  21043  dchrisumlem2  21044  dchrmusum2  21048  dchrvmasum2lem  21050  dchrvmasumiflem1  21055  dchrisum0flblem1  21062  dchrisum0flblem2  21063  dchrisum0flb  21064  dchrisum0re  21067  dchrisum0lem1b  21069  dchrisum0lem1  21070  dchrisum0lem2a  21071  dchrisum0lem2  21072  dchrisum0lem3  21073  mudivsum  21084  mulogsum  21086  mulog2sumlem2  21089  selberg2lem  21104  logdivbnd  21110  pntrsumo1  21119  pntrsumbnd2  21121  pntrlog2bndlem2  21132  pntrlog2bndlem4  21134  pntrlog2bndlem6a  21136  pntlemj  21157  pntlemf  21159  ostth2lem3  21189  eupares  21538  eupap1  21539  eupath2lem3  21542  eupath2  21543  htthlem  22261  hhsscms  22620  shmodsi  22732  pjoc1i  22774  5oalem1  22997  mayete3i  23071  mayete3iOLD  23072  adj1  23277  iundisj2f  23866  ssnnssfz  23977  iundisj2fi  23984  pnfneige0  24133  indpreima  24211  esumfzf  24248  esumpcvgval  24257  esumpmono  24258  esumcvg  24265  measbase  24340  dya2iocnei  24419  orrvcval4  24494  orrvcoel  24495  orrvccel  24496  ballotlem2  24518  ballotlemfrceq  24558  lgamgulm2  24592  lgamcvglem  24596  lgamcvg2  24611  gamcvg2lem  24615  subfacp1lem1  24637  subfacp1lem5  24642  subfacp1lem6  24643  subfacval2  24645  erdszelem7  24655  cvxscon  24702  cvmliftlem5  24748  cvmliftlem7  24750  cvmliftlem10  24753  cvmliftlem13  24755  relexpsucr  24902  clim2prod  24988  clim2div  24989  ntrivcvgfvn0  24999  ntrivcvgtail  25000  prodeq2ii  25011  prodmolem3  25031  prodmolem2a  25032  fprod  25039  fprodntriv  25040  fprodss  25046  fprodser  25047  fprodcl2lem  25048  fprodmul  25056  fproddiv  25057  fprodabs  25069  fprodefsum  25070  fprodeq0  25071  fprodn0  25075  iprodclim3  25078  iprodmul  25081  fallfacfwd  25112  bdayelon  25351  imageval  25486  eedimeq  25544  axlowdimlem16  25603  bpolysum  25806  bpolydiflem  25807  fsumkthpow  25809  ftc1cnnc  25972  upixp  26115  sdclem2  26130  caushft  26151  ismtyres  26201  rrnmet  26222  rrndstprj1  26223  rrndstprj2  26224  rrncmslem  26225  rrnequiv  26228  iccbnd  26233  mapfzcons  26456  diophren  26558  irrapxlem1  26569  monotuz  26688  acongeq  26732  jm2.26lem3  26756  jm3.1lem2  26773  pw2f1ocnv  26792  psgnunilem4  27082  psgnghm  27099  matbas2i  27138  idomodle  27174  fcnre  27357  refsumcn  27362  rfcnnnub  27368  climsuselem1  27394  stoweidlem11  27421  stoweidlem15  27425  stoweidlem17  27427  stoweidlem20  27430  stoweidlem34  27444  stoweidlem35  27445  stoweidlem46  27456  stoweidlem47  27457  stoweidlem56  27466  stoweidlem59  27469  stoweidlem62  27472  stirlinglem5  27488  stirlinglem14  27497  bnj1172  28701  bnj1245  28714  bnj1311  28724  bnj1450  28750  bnj1501  28767  osumcllem7N  30127  pexmidlem4N  30138  lcfrlem4  31711  lcfrlem5  31712  lcfrlem6  31713  lcfrlem16  31724  lcfrlem38  31746  mapdrvallem2  31811  mapdh8ab  31943  mapdh8ad  31945  mapdh8e  31950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2373  df-clel 2376
  Copyright terms: Public domain W3C validator