Theorem syl6eleq 2528

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 2514	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434

This theorem is referenced by:  syl6eleqr  2529  prid2g  3977  ndmfvrcl  5710  fnwelem  6682  tz7.48-1  6890  brwitnlem  6939  oeeulem  7032  dffi3  7673  cnfcom3lem  7928  cnfcom3lemOLD  7936  alephgeom  8244  fpwwe2lem6  8794  canthwelem  8809  hargch  8832  r1wunlim  8896  eluzel2  10858  fznn0sub2  11480  fseq1p1m1  11526  exple1  11915  digit1  11990  bcval5  12086  bcpasc  12089  hashf1  12202  seqcoll  12208  seqcoll2  12209  swrdccat1  12343  swrdccat2  12344  cats1un  12362  splfv2a  12390  splval2  12391  caubnd  12838  limsupgre  12951  clim2ser  13124  clim2ser2  13125  iserex  13126  isermulc2  13127  iserle  13129  iserge0  13130  climub  13131  climserle  13132  isercolllem2  13135  isercolllem3  13136  isercoll  13137  isercoll2  13138  serf0  13150  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  sumeq2ii  13162  summolem3  13183  summolem2a  13184  fsum  13189  sum0  13190  fsumcl2lem  13200  fsumadd  13207  isumclim3  13218  isumadd  13226  fsump1i  13228  fsummulc2  13243  fsumrelem  13262  iserabs  13270  cvgcmp  13271  cvgcmpub  13272  cvgcmpce  13273  binom1dif  13288  isumshft  13294  isumsplit  13295  isumrpcl  13298  isumsup2  13301  climcndslem1  13304  climcndslem2  13305  climcnds  13306  arisum2  13315  trireciplem  13316  geoser  13321  geolim  13322  geo2lim  13327  cvgrat  13335  mertenslem1  13336  mertenslem2  13337  mertens  13338  efcvgfsum  13363  efcj  13369  effsumlt  13387  ruclem7  13510  bitsfzolem  13622  bitsfzo  13623  bitsfi  13625  bitsinv1lem  13629  bitsinv1  13630  bitsinvp1  13637  sadcp1  13643  sadadd  13655  sadass  13659  bitsres  13661  smupp1  13668  smuval2  13670  smupval  13676  smueqlem  13678  smumul  13681  algrp1  13741  phiprmpw  13843  crt  13845  phimullem  13846  eulerthlem2  13849  prmdiv  13852  pcpremul  13902  pcmpt  13946  pcfac  13953  pockthlem  13958  pockthg  13959  prmreclem2  13970  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  prmreclem6  13974  prmrec  13975  1arith  13980  vdwapun  14027  vdwlem1  14034  vdwlem2  14035  vdwlem3  14036  vdwlem6  14039  vdwlem8  14041  vdwlem10  14043  vdw  14047  imasvscafn  14467  xpsfrnel2  14495  oppccatid  14650  oppccomfpropd  14658  funcoppc  14777  invfuc  14876  hofcl  15061  yonedalem4c  15079  gsumwsubmcl  15507  gsumccat  15510  gsumwmhm  15514  mulgnnp1  15626  mulgnnsubcl  15630  mulgnn0z  15638  mulgnndir  15640  psgnunilem4  15994  psgnran  16012  sylow1lem1  16088  lsmmod2  16164  lsmdisj2r  16173  efginvrel2  16215  efgsdmi  16220  efgsrel  16222  efgs1b  16224  efgsp1  16225  efgredleme  16231  efgredlemc  16233  efgcpbllemb  16243  frgpuplem  16260  mulgnn0di  16304  frgpnabllem1  16342  lt6abl  16362  cycsubgcyg  16368  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzcl2  16380  gsumzclOLD  16384  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzoppg  16430  gsumzoppgOLD  16431  dprd2da  16529  pgpfaclem1  16570  srgbinom  16631  isirred  16779  lspprid2  17056  lspsnat  17203  lsppratlem1  17205  lsppratlem3  17207  lidl0cl  17271  lidlacl  17272  lidlnegcl  17273  lidlmcl  17276  psrbaglefi  17418  psrbaglefiOLD  17419  psrass23  17459  mpfind  17597  psr1bascl  17631  ply1basf  17633  mpfpf1  17760  pf1mpf  17761  evl1scvarpw  17772  psgnghm  17985  matbas2i  18298  1mavmul  18334  mdetleib2  18374  marep01ma  18441  smadiadetlem4  18450  slesolinv  18461  cldrcl  18605  ordtbas  18771  iscnp2  18818  dis1stc  19078  ptbasfi  19129  ptpjopn  19160  ptclsg  19163  ptcnp  19170  kqtop  19293  reghmph  19341  ptcmplem2  19600  ptcmplem3  19601  ptcmplem4  19602  tsmslem1  19674  utop2nei  19800  isucn2  19829  cuspcvg  19851  cnextucn  19853  imasdsf1olem  19923  blcvx  20350  xrhmeo  20493  cnrehmeo  20500  evth  20506  reparphti  20544  iscau4  20765  iscmet3lem1  20777  lmle  20787  rrxfsupp  20876  pjthlem2  20900  ovollb2lem  20946  ovolunlem1a  20954  ovoliunlem1  20960  ovoliun2  20964  ovolscalem1  20971  ovolicc1  20974  ovolicc2lem4  20978  iundisj2  21005  voliunlem1  21006  volsup  21012  ioombl1lem4  21017  uniioovol  21034  uniioombllem3  21040  uniioombllem4  21041  uniioombllem6  21043  vitalilem5  21067  mbfimaopnlem  21108  mbflimsup  21119  mbfi1fseqlem3  21170  iblitg  21221  dvnp1  21374  cpncn  21385  dvlip2  21442  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumrlimge0  21477  dvfsumrlim2  21479  ftc1cn  21490  elplyd  21645  ply1termlem  21646  ply1term  21647  ply0  21651  plyeq0lem  21653  plyaddlem1  21656  plymullem1  21657  plyaddlem  21658  plymullem  21659  coeeulem  21667  plyco  21684  coeeq2  21685  coefv0  21690  coemulhi  21696  coemulc  21697  plycj  21719  dvply1  21725  vieta1lem2  21752  elqaalem2  21761  dvtaylp  21810  dvntaylp  21811  taylthlem1  21813  taylth  21815  ulmres  21828  ulmshftlem  21829  ulmshft  21830  ulmcau  21835  ulmdvlem1  21840  mtest  21844  mtestbdd  21845  pserulm  21862  psercn2  21863  psercnlem1  21865  psercn  21866  pserdvlem2  21868  abelthlem6  21876  abelth  21881  efif1olem1  21973  efif1olem3  21975  efif1olem4  21976  logcn  22067  advlogexp  22075  efopn  22078  cxpeq  22170  asinsin  22262  atantayl  22307  leibpilem2  22311  birthdaylem2  22321  birthdaylem3  22322  efrlim  22338  emcllem2  22365  emcllem5  22368  emcllem7  22370  harmonicbnd4  22379  fsumharmonic  22380  wilthlem2  22382  wilthlem3  22383  ftalem1  22385  ftalem2  22386  ftalem3  22387  ftalem5  22389  basellem2  22394  basellem3  22395  basellem5  22397  basellem8  22400  ppiprm  22464  ppinprm  22465  chtprm  22466  chtnprm  22467  chpp1  22468  vma1  22479  ppiltx  22490  musum  22506  0sgmppw  22512  1sgmprm  22513  ppiublem2  22517  chtublem  22525  fsumvma2  22528  chpchtsum  22533  logexprlim  22539  bposlem5  22602  lgscllem  22617  lgsval2lem  22620  lgsval4a  22632  lgsneg  22633  lgsdir2lem3  22639  lgsdir2lem5  22641  lgsdir  22644  lgsdilem2  22645  lgsdi  22646  lgsne0  22647  lgseisenlem1  22663  lgsquadlem2  22669  chebbnd1lem1  22693  chtppilimlem1  22697  rplogsumlem2  22709  rpvmasumlem  22711  dchrisumlem1  22713  dchrisumlem2  22714  dchrmusum2  22718  dchrvmasum2lem  22720  dchrvmasumiflem1  22725  dchrisum0flblem1  22732  dchrisum0flblem2  22733  dchrisum0flb  22734  dchrisum0re  22737  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  mudivsum  22754  mulogsum  22756  mulog2sumlem2  22759  selberg2lem  22774  logdivbnd  22780  pntrsumo1  22789  pntrsumbnd2  22791  pntrlog2bndlem2  22802  pntrlog2bndlem4  22804  pntrlog2bndlem6a  22806  pntlemj  22827  pntlemf  22829  ostth2lem3  22859  tglngne  22958  eedimeq  23095  axlowdimlem16  23154  ebtwntg  23179  eupares  23547  eupap1  23548  eupath2lem3  23551  eupath2  23552  htthlem  24270  hhsscms  24631  shmodsi  24743  pjoc1i  24785  5oalem1  25008  mayete3i  25082  mayete3iOLD  25083  adj1  25288  iundisj2f  25883  fcnvgreu  25942  ssnnssfz  26027  iundisj2fi  26032  pnfneige0  26333  pl1cn  26337  indpreima  26433  esumfzf  26470  esumpcvgval  26479  esumpmono  26480  esumcvg  26487  measbase  26563  dya2iocnei  26649  oddpwdc  26689  eulerpartlems  26695  eulerpartlemb  26703  sseqf  26727  fibp1  26736  orrvcval4  26799  orrvcoel  26800  orrvccel  26801  ballotlem2  26823  ballotlemfrceq  26863  signsplypnf  26903  signswch  26914  signstf0  26921  signstfvn  26922  signstfvneq0  26925  signstfvcl  26926  signstfveq0  26930  signsvfn  26935  lgamgulm2  26974  lgamcvglem  26978  lgamcvg2  26993  gamcvg2lem  26997  subfacp1lem1  27019  subfacp1lem5  27024  subfacp1lem6  27025  subfacval2  27027  erdszelem7  27037  cvxscon  27084  cvmliftlem5  27130  cvmliftlem7  27132  cvmliftlem10  27135  cvmliftlem13  27137  relexpsucr  27283  clim2prod  27354  clim2div  27355  ntrivcvgfvn0  27365  ntrivcvgtail  27366  prodeq2ii  27377  prodmolem3  27397  prodmolem2a  27398  fprod  27405  fprodntriv  27406  fprodss  27412  fprodser  27413  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodabs  27435  fprodefsum  27436  fprodeq0  27437  fprodn0  27441  iprodclim3  27451  iprodmul  27454  fallfacfwd  27490  0fallfac  27491  binomfallfaclem2  27494  fallfacval4  27497  bdayelon  27772  imageval  27912  bpolysum  28147  bpolydiflem  28148  fsumkthpow  28150  mblfinlem2  28382  ftc1cnnc  28419  upixp  28576  sdclem2  28591  caushft  28610  ismtyres  28660  rrnmet  28681  rrndstprj1  28682  rrndstprj2  28683  rrncmslem  28684  rrnequiv  28687  iccbnd  28692  mapfzcons  29005  diophren  29105  irrapxlem1  29116  monotuz  29235  acongeq  29279  jm2.26lem3  29303  jm3.1lem2  29320  pw2f1ocnv  29339  idomodle  29514  fcnre  29700  refsumcn  29705  rfcnnnub  29711  climsuselem1  29733  stoweidlem11  29759  stoweidlem15  29763  stoweidlem17  29765  stoweidlem20  29768  stoweidlem34  29782  stoweidlem35  29783  stoweidlem46  29794  stoweidlem47  29795  stoweidlem56  29804  stoweidlem59  29807  stoweidlem62  29810  stirlinglem5  29826  stirlinglem14  29835  ssnn0ssfz  30693  zlmodzxzscm  30705  rmsupp0  30732  psrass23l  30763  lply1binom  30774  lply1binomsc  30775  matgsum  30785  dmatmul  30799  dmatmulcl  30802  dmatcrng  30804  scmatmulcl  30809  scmatcrng  30811  pmatcollpw1lem4  30817  pmatcollpw1  30819  pmatcollpw2  30821  m1detdiag  30823  lincsum  30852  lincscm  30853  lindslinindimp2lem4  30884  lincresunit3  30904  bnj1172  31879  bnj1245  31892  bnj1311  31902  bnj1450  31928  bnj1501  31945  osumcllem7N  33446  pexmidlem4N  33457  lcfrlem4  35030  lcfrlem5  35031  lcfrlem6  35032  lcfrlem16  35043  lcfrlem38  35065  mapdrvallem2  35130  mapdh8ab  35262  mapdh8ad  35264  mapdh8e  35269