Theorem syl6eleq 2711

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

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  syl6eleqr  2712  3eltr3g  2717  prid2g  4296  ndmfvrcl  6219  fnwelem  7292  tz7.48-1  7538  brwitnlem  7587  oeeulem  7681  dffi3  8337  cnfcom3lem  8600  alephgeom  8905  fpwwe2lem6  9457  canthwelem  9472  hargch  9495  r1wunlim  9559  eluzel2  11692  fseq1p1m1  12414  fznn0sub2  12446  nn0split  12454  fz1fzo0m1  12515  exple1  12920  digit1  12998  bcval5  13105  bcpasc  13108  hashf1  13241  seqcoll  13248  seqcoll2  13249  ccatrn  13372  swrdccat1  13457  swrdccat2  13458  cats1un  13475  splfv2a  13507  splval2  13508  caubnd  14098  limsupgre  14212  clim2ser  14385  clim2ser2  14386  iserex  14387  isermulc2  14388  iserle  14390  iserge0  14391  climub  14392  climserle  14393  isercolllem2  14396  isercolllem3  14397  isercoll  14398  isercoll2  14399  serf0  14411  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  sumeq2ii  14423  summolem3  14445  summolem2a  14446  fsum  14451  sum0  14452  fsumcl2lem  14462  fsumadd  14470  isumclim3  14490  isumadd  14498  fsump1i  14500  fsummulc2  14516  fsumrelem  14539  iserabs  14547  cvgcmp  14548  cvgcmpub  14549  cvgcmpce  14550  binom1dif  14565  isumshft  14571  isumsplit  14572  isumrpcl  14575  isumsup2  14578  climcndslem1  14581  climcndslem2  14582  climcnds  14583  arisum2  14593  trireciplem  14594  geoser  14599  geolim  14601  geo2lim  14606  cvgrat  14615  mertenslem1  14616  mertenslem2  14617  mertens  14618  clim2prod  14620  clim2div  14621  ntrivcvgfvn0  14631  ntrivcvgtail  14632  prodeq2ii  14643  prodmolem3  14663  prodmolem2a  14664  fprod  14671  fprodntriv  14672  fprodss  14678  fprodser  14679  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodabs  14704  fprodeq0  14705  fprodn0  14709  iprodclim3  14731  iprodmul  14734  fallfacfwd  14767  0fallfac  14768  binomfallfaclem2  14771  fallfacval4  14774  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  efcvgfsum  14816  efcj  14822  fprodefsum  14825  effsumlt  14841  ruclem7  14965  bitsfzolem  15156  bitsfzo  15157  bitsfi  15159  bitsinv1lem  15163  bitsinv1  15164  bitsinvp1  15171  sadcp1  15177  sadadd  15189  sadass  15193  bitsres  15195  smupp1  15202  smuval2  15204  smupval  15210  smueqlem  15212  smumul  15215  algrp1  15287  phiprmpw  15481  crth  15483  phimullem  15484  eulerthlem2  15487  prmdiv  15490  pcpremul  15548  pcmpt  15596  pcfac  15603  pockthlem  15609  pockthg  15610  prmreclem2  15621  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  prmrec  15626  1arith  15631  vdwapun  15678  vdwlem1  15685  vdwlem2  15686  vdwlem3  15687  vdwlem6  15690  vdwlem8  15692  vdwlem10  15694  vdw  15698  imasvscafn  16197  xpsfrnel2  16225  oppccatid  16379  oppccomfpropd  16387  brcic  16458  funcoppc  16535  invfuc  16634  hofcl  16899  yonedalem4c  16917  gsumwsubmcl  17375  gsumccat  17378  gsumwmhm  17382  mulgnnp1  17549  mulgnnsubcl  17553  mulgnn0z  17567  mulgnndir  17569  mulgnndirOLD  17570  psgnunilem4  17917  psgnran  17935  sylow1lem1  18013  lsmmod2  18089  lsmdisj2r  18098  efginvrel2  18140  efgsdmi  18145  efgsrel  18147  efgs1b  18149  efgsp1  18150  efgredleme  18156  efgredlemc  18158  efgcpbllemb  18168  frgpuplem  18185  mulgnn0di  18231  frgpnabllem1  18276  lt6abl  18296  cycsubgcyg  18302  gsumval3eu  18305  gsumval3  18308  gsumzcl2  18311  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  telgsumfz0s  18388  dprdwd  18410  dprd2da  18441  pgpfaclem1  18480  srgbinom  18545  isirred  18699  lspprid2  18998  lspsnat  19145  lsppratlem1  19147  lsppratlem3  19149  lidl0cl  19212  lidlacl  19213  lidlnegcl  19214  lidlmcl  19217  psrbaglefi  19372  psrass23l  19408  psrass23  19410  mplcoe5lem  19467  mpfind  19536  psr1bascl  19570  ply1basf  19572  gsummoncoe1  19674  lply1binom  19676  lply1binomsc  19677  mpfpf1  19715  pf1mpf  19716  evl1scvarpw  19727  psgnghm  19926  matbas2i  20228  matecld  20232  matgsum  20243  mpt2matmul  20252  dmatmul  20303  1mavmul  20354  mdetleib2  20394  m1detdiag  20403  marep01ma  20466  smadiadetlem4  20475  slesolinv  20486  pmatcollpw3fi1lem1  20591  chpscmat  20647  chpscmatgsumbin  20649  chp0mat  20651  chpidmat  20652  chfacfisf  20659  chfacfisfcpmat  20660  chfacfpmmulgsum2  20670  cldrcl  20830  ordtbas  20996  iscnp2  21043  dis1stc  21302  ptbasfi  21384  ptpjopn  21415  ptclsg  21418  ptcnp  21425  kqtop  21548  reghmph  21596  ptcmplem2  21857  ptcmplem3  21858  ptcmplem4  21859  tsmslem1  21932  utop2nei  22054  isucn2  22083  cuspcvg  22105  cnextucn  22107  imasdsf1olem  22178  blcvx  22601  xrhmeo  22745  cnrehmeo  22752  evth  22758  reparphti  22797  iscau4  23077  iscmet3lem1  23089  lmle  23099  rrxfsupp  23185  pjthlem2  23209  ovollb2lem  23256  ovolunlem1a  23264  ovoliunlem1  23270  ovoliun2  23274  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem4  23288  iundisj2  23317  voliunlem1  23318  volsup  23324  ioombl1lem4  23329  uniioovol  23347  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  vitalilem5  23381  mbfimaopnlem  23422  mbflimsup  23433  mbfi1fseqlem3  23484  iblitg  23535  dvnp1  23688  cpncn  23699  dvlip2  23758  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumrlimge0  23793  dvfsumrlim2  23795  ftc1cn  23806  elplyd  23958  ply1termlem  23959  ply1term  23960  ply0  23964  plyeq0lem  23966  plyaddlem1  23969  plymullem1  23970  plyaddlem  23971  plymullem  23972  coeeulem  23980  plyco  23997  coeeq2  23998  coefv0  24004  coemulhi  24010  coemulc  24011  plycj  24033  dvply1  24039  vieta1lem2  24066  elqaalem2  24075  dvtaylp  24124  dvntaylp  24125  taylthlem1  24127  taylth  24129  ulmres  24142  ulmshftlem  24143  ulmshft  24144  ulmcau  24149  ulmdvlem1  24154  mtest  24158  mtestbdd  24159  pserulm  24176  psercn2  24177  psercnlem1  24179  psercn  24180  pserdvlem2  24182  abelthlem6  24190  abelth  24195  efif1olem1  24288  efif1olem3  24290  efif1olem4  24291  logcn  24393  advlogexp  24401  efopn  24404  cxpeq  24498  asinsin  24619  atantayl  24664  leibpilem2  24668  birthdaylem2  24679  birthdaylem3  24680  efrlim  24696  emcllem2  24723  emcllem5  24726  emcllem7  24728  harmonicbnd4  24737  fsumharmonic  24738  lgamgulm2  24762  lgamcvglem  24766  lgamcvg2  24781  gamcvg2lem  24785  wilthlem2  24795  wilthlem3  24796  ftalem1  24799  ftalem2  24800  ftalem3  24801  ftalem5  24803  basellem2  24808  basellem3  24809  basellem5  24811  basellem8  24814  ppiprm  24877  ppinprm  24878  chtprm  24879  chtnprm  24880  chpp1  24881  vma1  24892  ppiltx  24903  musum  24917  0sgmppw  24923  1sgmprm  24924  ppiublem2  24928  chtublem  24936  fsumvma2  24939  chpchtsum  24944  logexprlim  24950  bposlem5  25013  lgscllem  25029  lgsval2lem  25032  lgsval4a  25044  lgsneg  25046  lgsdir2lem3  25052  lgsdir2lem5  25054  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  gausslemma2dlem3  25093  lgseisenlem1  25100  lgsquadlem2  25106  chebbnd1lem1  25158  chtppilimlem1  25162  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasum2lem  25185  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0flb  25199  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  mudivsum  25219  mulogsum  25221  mulog2sumlem2  25224  selberg2lem  25239  logdivbnd  25245  pntrsumo1  25254  pntrsumbnd2  25256  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem6a  25271  pntlemj  25292  pntlemf  25294  ostth2lem3  25324  tglngne  25445  ltgseg  25491  eedimeq  25778  axlowdimlem16  25837  ebtwntg  25862  subgruhgredgd  26176  subumgredg2  26177  umgrres1lem  26202  wlkson  26552  wksonproplem  26601  trlsonfval  26602  pthsonfval  26636  spthson  26637  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  eupth2lems  27098  htthlem  27774  hhsscms  28136  shmodsi  28248  pjoc1i  28290  5oalem1  28513  mayete3i  28587  adj1  28792  iundisj2f  29403  fmptco1f1o  29434  fcnvgreu  29472  ssnnssfz  29549  iundisj2fi  29556  pmtrto1cl  29849  psgnfzto1stlem  29850  fzto1st1  29852  1smat1  29870  submateqlem2  29874  lmatfval  29880  mdetlap1  29892  madjusmdetlem1  29893  madjusmdetlem2  29894  madjusmdetlem3  29895  madjusmdetlem4  29896  pnfneige0  29997  pl1cn  30001  rrhqima  30058  indpreima  30087  esumfzf  30131  esumpcvgval  30140  esumpmono  30141  esumcvg  30148  ldgenpisyslem1  30226  ldgenpisys  30229  measbase  30260  dya2iocnei  30344  oddpwdc  30416  eulerpartlems  30422  eulerpartlemb  30430  sseqf  30454  fibp1  30463  orrvcval4  30526  orrvcoel  30527  orrvccel  30528  ballotlem2  30550  ballotlemfrceq  30590  signsplypnf  30627  signswch  30638  signstf0  30645  signstfvn  30646  signstfvneq0  30649  signstfvcl  30650  signstfveq0  30654  signsvfn  30659  fct2relem  30675  fsum2dsub  30685  reprsuc  30693  reprpmtf1o  30704  breprexplema  30708  breprexplemc  30710  hgt749d  30727  hgt750lemb  30734  tgoldbachgnn  30737  bnj1172  31069  bnj1245  31082  bnj1311  31092  bnj1450  31118  bnj1501  31135  subfacp1lem1  31161  subfacp1lem5  31166  subfacp1lem6  31167  subfacval2  31169  erdszelem7  31179  cvxsconn  31225  cvmliftlem5  31271  cvmliftlem7  31273  cvmliftlem10  31276  cvmliftlem13  31278  mrsubvrs  31419  msubrn  31426  msubco  31428  msubvrs  31457  imageval  32037  fwddifnp1  32272  knoppcnlem8  32490  knoppcnlem10  32492  icoreunrn  33207  istoprelowl  33208  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  mblfinlem2  33447  ftc1cnnc  33484  upixp  33524  sdclem2  33538  caushft  33557  ismtyres  33607  rrnmet  33628  rrndstprj1  33629  rrndstprj2  33630  rrncmslem  33631  rrnequiv  33634  iccbnd  33639  osumcllem7N  35248  pexmidlem4N  35259  lcfrlem4  36834  lcfrlem5  36835  lcfrlem6  36836  lcfrlem16  36847  lcfrlem38  36869  mapdrvallem2  36934  mapdh8ab  37066  mapdh8ad  37068  mapdh8e  37073  mapfzcons  37279  diophren  37377  irrapxlem1  37386  monotuz  37506  acongeq  37550  jm2.26lem3  37568  jm3.1lem2  37585  pw2f1ocnv  37604  idomodle  37774  trclfvdecomr  38020  imo72b2lem1  38471  dvgrat  38511  cvgdvgrat  38512  hashnzfz2  38520  fcnre  39184  refsumcn  39189  rfcnnnub  39195  disjf1o  39378  disjinfi  39380  ssmapsn  39408  ssuzfz  39565  nnsplit  39574  uzssd2  39644  uzublem  39657  fsumsermpt  39811  climsuselem1  39839  limcperiod  39860  sumnnodd  39862  lptioo2cn  39877  lptioo1cn  39878  climresmpt  39891  allbutfifvre  39907  climleltrp  39908  cnrefiisplem  40055  cncfshift  40087  cncfperiod  40092  cncfshiftioo  40105  fperdvper  40133  dvnmptdivc  40153  dvnmul  40158  dvmptfprod  40160  dvnprodlem3  40163  stoweidlem11  40228  stoweidlem15  40232  stoweidlem17  40234  stoweidlem20  40237  stoweidlem34  40251  stoweidlem35  40252  stoweidlem46  40263  stoweidlem47  40264  stoweidlem56  40273  stoweidlem59  40276  stoweidlem62  40279  stirlinglem5  40295  stirlinglem14  40304  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  fourierdlem11  40335  fourierdlem15  40339  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem25  40349  fourierdlem48  40371  fourierdlem52  40375  fourierdlem54  40377  fourierdlem58  40381  fourierdlem62  40385  fourierdlem64  40387  fourierdlem65  40388  fourierdlem69  40392  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem80  40403  fourierdlem81  40404  fourierdlem83  40406  fourierdlem92  40415  fourierdlem93  40416  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  fouriercnp  40443  fouriersw  40448  elaa2lem  40450  etransclem4  40455  etransclem7  40458  etransclem10  40461  etransclem14  40465  etransclem15  40466  etransclem24  40475  etransclem25  40476  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem44  40495  etransclem46  40497  qndenserrnopnlem  40517  qndenserrn  40519  prsal  40538  salgencntex  40561  subsaliuncl  40576  subsalsal  40577  sge0tsms  40597  sge0fodjrnlem  40633  sge0isum  40644  iundjiunlem  40676  iundjiun  40677  meadjiunlem  40682  meaiunlelem  40685  meaiuninclem  40697  meaiininc2  40702  caragensplit  40714  carageneld  40716  carageniuncllem1  40735  caratheodorylem1  40740  caratheodorylem2  40741  hoicvr  40762  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmvlelem2  40810  hoiqssbllem2  40837  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  smflimlem3  40981  smfmullem4  41001  smfsupxr  41022  smflimsuplem2  41027  smflimsuplem5  41030  elmod2  41340  pwdif  41501  ssnn0ssfz  42127  zlmodzxzscm  42135  rmsupp0  42149  lincsum  42218  lincscm  42219  lindslinindimp2lem4  42250  lincresunit3  42270  elbigofrcl  42344  setrec1  42438  aacllem  42547