Theorem syl6eleq 2539

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

Step	Hyp	Ref	Expression
1		syl6eleq.1	. 2 |- ( ph -> A e. B )
2		syl6eleq.2	. . 3 |- B = C
3	2	a1i 11	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2531	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1444   e. wcel 1887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-cleq 2444  df-clel 2447

This theorem is referenced by:  syl6eleqr  2540  3eltr3g  2545  prid2g  4079  ndmfvrcl  5890  fnwelem  6911  tz7.48-1  7160  brwitnlem  7209  oeeulem  7302  dffi3  7945  cnfcom3lem  8208  alephgeom  8513  fpwwe2lem6  9060  canthwelem  9075  hargch  9098  r1wunlim  9162  eluzel2  11164  fseq1p1m1  11868  fznn0sub2  11897  nn0split  11906  fz1fzo0m1  11963  exple1  12332  digit1  12406  bcval5  12503  bcpasc  12506  hashf1  12620  seqcoll  12627  seqcoll2  12628  ccatrn  12733  swrdccat1  12813  swrdccat2  12814  cats1un  12832  splfv2a  12863  splval2  12864  caubnd  13421  limsupgre  13542  limsupgreOLD  13543  clim2ser  13718  clim2ser2  13719  iserex  13720  isermulc2  13721  iserle  13723  iserge0  13724  climub  13725  climserle  13726  isercolllem2  13729  isercolllem3  13730  isercoll  13731  isercoll2  13732  serf0  13747  iseraltlem2  13749  iseraltlem3  13750  iseralt  13751  sumeq2ii  13759  summolem3  13780  summolem2a  13781  fsum  13786  sum0  13787  fsumcl2lem  13797  fsumadd  13805  isumclim3  13820  isumadd  13828  fsump1i  13830  fsummulc2  13845  fsumrelem  13867  iserabs  13875  cvgcmp  13876  cvgcmpub  13877  cvgcmpce  13878  binom1dif  13891  isumshft  13897  isumsplit  13898  isumrpcl  13901  isumsup2  13904  climcndslem1  13907  climcndslem2  13908  climcnds  13909  arisum2  13919  trireciplem  13920  geoser  13925  geolim  13926  geo2lim  13931  cvgrat  13939  mertenslem1  13940  mertenslem2  13941  mertens  13942  clim2prod  13944  clim2div  13945  ntrivcvgfvn0  13955  ntrivcvgtail  13956  prodeq2ii  13967  prodmolem3  13987  prodmolem2a  13988  fprod  13995  fprodntriv  13996  fprodss  14002  fprodser  14003  fprodcl2lem  14004  fprodmul  14014  fproddiv  14015  fprodabs  14028  fprodeq0  14029  fprodn0  14033  iprodclim3  14053  iprodmul  14056  fallfacfwd  14089  0fallfac  14090  binomfallfaclem2  14093  fallfacval4  14096  bpolysum  14106  bpolydiflem  14107  fsumkthpow  14109  efcvgfsum  14140  efcj  14146  fprodefsum  14149  effsumlt  14165  ruclem7  14288  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bitsfi  14411  bitsinv1lem  14415  bitsinv1  14416  bitsinvp1  14423  sadcp1  14429  sadadd  14441  sadass  14445  bitsres  14447  smupp1  14454  smuval2  14456  smupval  14462  smueqlem  14464  smumul  14467  algrp1  14533  phiprmpw  14724  crt  14726  phimullem  14727  eulerthlem2  14730  prmdiv  14733  pcpremul  14793  pcmpt  14837  pcfac  14844  pockthlem  14849  pockthg  14850  prmreclem2  14861  prmreclem3  14862  prmreclem4  14863  prmreclem5  14864  prmreclem6  14865  prmrec  14866  1arith  14871  vdwapun  14924  vdwlem1  14931  vdwlem2  14932  vdwlem3  14933  vdwlem6  14936  vdwlem8  14938  vdwlem10  14940  vdw  14944  imasvscafn  15443  xpsfrnel2  15471  oppccatid  15624  oppccomfpropd  15632  brcic  15703  funcoppc  15780  invfuc  15879  hofcl  16144  yonedalem4c  16162  gsumwsubmcl  16622  gsumccat  16625  gsumwmhm  16629  mulgnnp1  16766  mulgnnsubcl  16770  mulgnn0z  16778  mulgnndir  16780  psgnunilem4  17138  psgnran  17156  sylow1lem1  17250  lsmmod2  17326  lsmdisj2r  17335  efginvrel2  17377  efgsdmi  17382  efgsrel  17384  efgs1b  17386  efgsp1  17387  efgredleme  17393  efgredlemc  17395  efgcpbllemb  17405  frgpuplem  17422  mulgnn0di  17466  frgpnabllem1  17509  lt6abl  17529  cycsubgcyg  17535  gsumval3eu  17538  gsumval3  17541  gsumzcl2  17544  gsumzaddlem  17554  gsumconst  17567  gsumzmhm  17570  gsumzoppg  17577  telgsumfz0s  17621  dprdwd  17643  dprd2da  17675  pgpfaclem1  17714  srgbinom  17778  isirred  17927  lspprid2  18221  lspsnat  18368  lsppratlem1  18370  lsppratlem3  18372  lidl0cl  18435  lidlacl  18436  lidlnegcl  18437  lidlmcl  18441  psrbaglefi  18596  psrass23l  18632  psrass23  18634  mplcoe5lem  18691  mpfind  18759  psr1bascl  18793  ply1basf  18795  gsummoncoe1  18898  lply1binom  18900  lply1binomsc  18901  mpfpf1  18939  pf1mpf  18940  evl1scvarpw  18951  psgnghm  19148  matbas2i  19447  matecld  19451  matgsum  19462  mpt2matmul  19471  dmatmul  19522  1mavmul  19573  mdetleib2  19613  m1detdiag  19622  marep01ma  19685  smadiadetlem4  19694  slesolinv  19705  pmatcollpw3fi1lem1  19810  chpscmat  19866  chpscmatgsumbin  19868  chp0mat  19870  chpidmat  19871  chfacfisf  19878  chfacfisfcpmat  19879  chfacfpmmulgsum2  19889  cldrcl  20041  ordtbas  20208  iscnp2  20255  dis1stc  20514  ptbasfi  20596  ptpjopn  20627  ptclsg  20630  ptcnp  20637  kqtop  20760  reghmph  20808  ptcmplem2  21068  ptcmplem3  21069  ptcmplem4  21070  tsmslem1  21143  utop2nei  21265  isucn2  21294  cuspcvg  21316  cnextucn  21318  imasdsf1olem  21388  blcvx  21816  xrhmeo  21974  cnrehmeo  21981  evth  21987  reparphti  22028  iscau4  22249  iscmet3lem1  22261  lmle  22271  rrxfsupp  22356  pjthlem2  22392  ovollb2lem  22441  ovolunlem1a  22449  ovoliunlem1  22455  ovoliun2  22459  ovolscalem1  22466  ovolicc1  22469  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  iundisj2  22502  voliunlem1  22503  volsup  22509  ioombl1lem4  22514  uniioovol  22536  uniioombllem3  22543  uniioombllem4  22544  uniioombllem6  22546  vitalilem5  22570  mbfimaopnlem  22611  mbflimsup  22623  mbflimsupOLD  22624  mbfi1fseqlem3  22675  iblitg  22726  dvnp1  22879  cpncn  22890  dvlip2  22947  dvfsumlem2  22979  dvfsumlem3  22980  dvfsumrlimge0  22982  dvfsumrlim2  22984  ftc1cn  22995  elplyd  23156  ply1termlem  23157  ply1term  23158  ply0  23162  plyeq0lem  23164  plyaddlem1  23167  plymullem1  23168  plyaddlem  23169  plymullem  23170  coeeulem  23178  plyco  23195  coeeq2  23196  coefv0  23202  coemulhi  23208  coemulc  23209  plycj  23231  dvply1  23237  vieta1lem2  23264  elqaalem2  23273  elqaalem2OLD  23276  dvtaylp  23325  dvntaylp  23326  taylthlem1  23328  taylth  23330  ulmres  23343  ulmshftlem  23344  ulmshft  23345  ulmcau  23350  ulmdvlem1  23355  mtest  23359  mtestbdd  23360  pserulm  23377  psercn2  23378  psercnlem1  23380  psercn  23381  pserdvlem2  23383  abelthlem6  23391  abelth  23396  efif1olem1  23491  efif1olem3  23493  efif1olem4  23494  logcn  23592  advlogexp  23600  efopn  23603  cxpeq  23697  asinsin  23818  atantayl  23863  leibpilem2  23867  birthdaylem2  23878  birthdaylem3  23879  efrlim  23895  emcllem2  23922  emcllem5  23925  emcllem7  23927  harmonicbnd4  23936  fsumharmonic  23937  lgamgulm2  23961  lgamcvglem  23965  lgamcvg2  23980  gamcvg2lem  23984  wilthlem2  23994  wilthlem3  23995  ftalem1  23997  ftalem2  23998  ftalem3  23999  ftalem5  24001  ftalem5OLD  24003  basellem2  24008  basellem3  24009  basellem5  24011  basellem8  24014  ppiprm  24078  ppinprm  24079  chtprm  24080  chtnprm  24081  chpp1  24082  vma1  24093  ppiltx  24104  musum  24120  0sgmppw  24126  1sgmprm  24127  ppiublem2  24131  chtublem  24139  fsumvma2  24142  chpchtsum  24147  logexprlim  24153  bposlem5  24216  lgscllem  24231  lgsval2lem  24234  lgsval4a  24246  lgsneg  24247  lgsdir2lem3  24253  lgsdir2lem5  24255  lgsdir  24258  lgsdilem2  24259  lgsdi  24260  lgsne0  24261  lgseisenlem1  24277  lgsquadlem2  24283  chebbnd1lem1  24307  chtppilimlem1  24311  rplogsumlem2  24323  rpvmasumlem  24325  dchrisumlem1  24327  dchrisumlem2  24328  dchrmusum2  24332  dchrvmasum2lem  24334  dchrvmasumiflem1  24339  dchrisum0flblem1  24346  dchrisum0flblem2  24347  dchrisum0flb  24348  dchrisum0re  24351  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2a  24355  dchrisum0lem2  24356  dchrisum0lem3  24357  mudivsum  24368  mulogsum  24370  mulog2sumlem2  24373  selberg2lem  24388  logdivbnd  24394  pntrsumo1  24403  pntrsumbnd2  24405  pntrlog2bndlem2  24416  pntrlog2bndlem4  24418  pntrlog2bndlem6a  24420  pntlemj  24441  pntlemf  24443  ostth2lem3  24473  tglngne  24595  ltgseg  24641  eedimeq  24928  axlowdimlem16  24987  ebtwntg  25012  eupares  25703  eupap1  25704  eupath2lem3  25707  eupath2  25708  htthlem  26570  hhsscms  26930  shmodsi  27042  pjoc1i  27084  5oalem1  27307  mayete3i  27381  adj1  27586  iundisj2f  28200  fcnvgreu  28275  ssnnssfz  28367  iundisj2fi  28373  pmtrto1cl  28612  psgnfzto1stlem  28613  fzto1st1  28615  1smat1  28630  submateqlem2  28634  lmatfval  28640  mdetlap1  28652  madjusmdetlem1  28653  madjusmdetlem2  28654  madjusmdetlem3  28655  madjusmdetlem4  28656  pnfneige0  28757  pl1cn  28761  rrhqima  28818  indpreima  28846  esumfzf  28890  esumpcvgval  28899  esumpmono  28900  esumcvg  28907  ldgenpisyslem1  28985  ldgenpisys  28988  measbase  29019  dya2iocnei  29104  oddpwdc  29187  eulerpartlems  29193  eulerpartlemb  29201  sseqf  29225  fibp1  29234  orrvcval4  29297  orrvcoel  29298  orrvccel  29299  ballotlem2  29321  ballotlemfrceq  29361  ballotlemfrceqOLD  29399  signsplypnf  29439  signswch  29450  signstf0  29457  signstfvn  29458  signstfvneq0  29461  signstfvcl  29462  signstfveq0  29466  signsvfn  29471  bnj1172  29810  bnj1245  29823  bnj1311  29833  bnj1450  29859  bnj1501  29876  subfacp1lem1  29902  subfacp1lem5  29907  subfacp1lem6  29908  subfacval2  29910  erdszelem7  29920  cvxscon  29966  cvmliftlem5  30012  cvmliftlem7  30014  cvmliftlem10  30017  cvmliftlem13  30019  mrsubvrs  30160  msubrn  30167  msubco  30169  msubvrs  30198  bdayelon  30569  imageval  30697  fwddifnp1  30932  icoreunrn  31762  istoprelowl  31763  poimirlem3  31943  poimirlem4  31944  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  poimirlem12  31952  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem18  31958  poimirlem19  31959  poimirlem20  31960  poimirlem21  31961  poimirlem22  31962  poimirlem23  31963  poimirlem24  31964  poimirlem25  31965  poimirlem26  31966  poimirlem27  31967  poimirlem28  31968  poimirlem29  31969  poimirlem31  31971  mblfinlem2  31978  ftc1cnnc  32016  upixp  32056  sdclem2  32071  caushft  32090  ismtyres  32140  rrnmet  32161  rrndstprj1  32162  rrndstprj2  32163  rrncmslem  32164  rrnequiv  32167  iccbnd  32172  osumcllem7N  33527  pexmidlem4N  33538  lcfrlem4  35113  lcfrlem5  35114  lcfrlem6  35115  lcfrlem16  35126  lcfrlem38  35148  mapdrvallem2  35213  mapdh8ab  35345  mapdh8ad  35347  mapdh8e  35352  mapfzcons  35558  diophren  35656  irrapxlem1  35666  monotuz  35789  acongeq  35833  jm2.26lem3  35856  jm3.1lem2  35873  pw2f1ocnv  35892  idomodle  36070  trclfvdecomr  36320  imo72b2lem1  36614  dvgrat  36661  cvgdvgrat  36662  hashnzfz2  36670  fcnre  37346  refsumcn  37351  rfcnnnub  37357  disjf1o  37466  disjinfi  37468  ssuzfz  37572  nnsplit  37581  climsuselem1  37686  limcperiod  37708  sumnnodd  37710  lptioo2cn  37726  lptioo1cn  37727  cncfshift  37751  cncfperiod  37756  cncfshiftioo  37770  fperdvper  37790  dvnmptdivc  37813  dvnmul  37818  dvmptfprod  37820  dvnprodlem3  37823  stoweidlem11  37871  stoweidlem15  37875  stoweidlem17  37877  stoweidlem20  37880  stoweidlem34  37895  stoweidlem35  37896  stoweidlem46  37907  stoweidlem47  37908  stoweidlem56  37917  stoweidlem59  37920  stoweidlem62  37923  stoweidlem62OLD  37924  stirlinglem5  37940  stirlinglem14  37949  dirkertrigeqlem2  37961  dirkertrigeqlem3  37962  fourierdlem11  37980  fourierdlem15  37984  fourierdlem16  37985  fourierdlem21  37990  fourierdlem22  37991  fourierdlem25  37994  fourierdlem48  38018  fourierdlem52  38022  fourierdlem54  38024  fourierdlem58  38028  fourierdlem62  38032  fourierdlem64  38034  fourierdlem65  38035  fourierdlem69  38039  fourierdlem70  38040  fourierdlem71  38041  fourierdlem73  38043  fourierdlem80  38050  fourierdlem81  38051  fourierdlem83  38053  fourierdlem92  38062  fourierdlem93  38063  fourierdlem97  38067  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  fourierdlem113  38083  fouriercnp  38090  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  etransclem4  38103  etransclem7  38106  etransclem10  38109  etransclem14  38113  etransclem15  38114  etransclem24  38123  etransclem25  38124  etransclem31  38130  etransclem32  38131  etransclem35  38134  etransclem44  38143  etransclem46  38145  qndenserrnopnlem  38166  qndenserrn  38168  prsal  38179  salgencntex  38202  sge0tsms  38222  sge0fodjrnlem  38258  sge0isum  38269  iundjiunlem  38297  iundjiun  38298  meadjiunlem  38303  meaiunlelem  38306  caragensplit  38321  carageneld  38323  carageniuncllem1  38342  caratheodorylem1  38347  caratheodorylem2  38348  hoicvr  38370  hsphoidmvle2  38407  hsphoidmvle  38408  hoidmv1lelem2  38414  hoidmv1lelem3  38415  hoidmvlelem2  38418  hoiqssbllem2  38445  elmod2  38724  subgruhgredgd  39356  subumgredg2  39357  umgrres1lem  39377  wlkson  39658  1wlksonproplem  39675  trlsonfval  39676  pthsonfval  39698  ssnn0ssfz  40183  zlmodzxzscm  40191  rmsupp0  40206  lincsum  40275  lincscm  40276  lindslinindimp2lem4  40307  lincresunit3  40327  elbigofrcl  40414  aacllem  40593