Theorem eleqtrdi 2854

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eleqtrdi.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrdi.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrdi

Step	Hyp	Ref	Expression
1		eleqtrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrdi.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2846	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleqtrrdi  2855  3eltr3g  2860  prid2g  4786  ndmfvrcl  6956  fnwelem  8172  tz7.48-1  8499  brwitnlem  8563  oeeulem  8657  dffi3  9500  cnfcom3lem  9772  ttrclse  9796  alephgeom  10151  fpwwe2lem5  10704  canthwelem  10719  hargch  10742  r1wunlim  10806  eluzel2  12908  fseq1p1m1  13658  fznn0sub2  13692  nn0split  13700  seqp1d  14069  exple1  14226  digit1  14286  bcval5  14367  bcpasc  14370  hashf1  14506  seqcoll  14513  seqcoll2  14514  ccatrn  14637  swrdccat2  14717  cats1un  14769  pfxccatin12lem3  14780  splfv2a  14804  splval2  14805  caubnd  15407  limsupgre  15527  clim2ser  15703  clim2ser2  15704  iserex  15705  isermulc2  15706  iserle  15708  iserge0  15709  climub  15710  climserle  15711  isercolllem2  15714  isercolllem3  15715  isercoll  15716  isercoll2  15717  serf0  15729  iseraltlem2  15731  iseraltlem3  15732  iseralt  15733  sumeq2ii  15741  summolem3  15762  summolem2a  15763  fsum  15768  sum0  15769  fsumcl2lem  15779  fsumadd  15788  isumclim3  15807  isumadd  15815  fsump1i  15817  fsummulc2  15832  fsumrelem  15855  iserabs  15863  cvgcmp  15864  cvgcmpub  15865  cvgcmpce  15866  binom1dif  15881  isumshft  15887  isumsplit  15888  isumrpcl  15891  isumsup2  15894  climcndslem1  15897  climcndslem2  15898  climcnds  15899  arisum2  15909  trireciplem  15910  geoser  15915  pwdif  15916  geolim  15918  geo2lim  15923  cvgrat  15931  mertenslem1  15932  mertenslem2  15933  mertens  15934  clim2prod  15936  clim2div  15937  ntrivcvgfvn0  15947  ntrivcvgtail  15948  prodeq2ii  15959  prodmolem3  15981  prodmolem2a  15982  fprod  15989  fprodntriv  15990  fprodss  15996  fprodser  15997  fprodcl2lem  15998  fprodmul  16008  fproddiv  16009  fprodabs  16022  fprodeq0  16023  fprodn0  16027  iprodclim3  16048  iprodmul  16051  fallfacfwd  16084  0fallfac  16085  binomfallfaclem2  16088  fallfacval4  16091  bpolysum  16101  bpolydiflem  16102  fsumkthpow  16104  efcvgfsum  16134  efcj  16140  fprodefsum  16143  effsumlt  16159  ruclem7  16284  bitsfzolem  16480  bitsfzo  16481  bitsfi  16483  bitsinv1lem  16487  bitsinv1  16488  bitsinvp1  16495  sadcp1  16501  sadadd  16513  sadass  16517  bitsres  16519  smupp1  16526  smuval2  16528  smupval  16534  smueqlem  16536  smumul  16539  algrp1  16621  phiprmpw  16823  crth  16825  phimullem  16826  eulerthlem2  16829  prmdiv  16832  pcpremul  16890  pcmpt  16939  pcfac  16946  pockthlem  16952  pockthg  16953  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  prmrec  16969  1arith  16974  vdwapun  17021  vdwlem1  17028  vdwlem2  17029  vdwlem3  17030  vdwlem6  17033  vdwlem8  17035  vdwlem10  17037  vdw  17041  imasvscafn  17597  oppccatid  17779  oppccomfpropd  17787  brcic  17859  funcoppc  17939  invfuc  18044  hofcl  18329  yonedalem4c  18347  gsumwsubmcl  18872  gsumsgrpccat  18875  gsumwmhm  18880  mulgnnp1  19122  mulgnnsubcl  19126  mulgnn0z  19141  mulgnndir  19143  ghmquskerlem1  19323  ghmquskerco  19324  psgnunilem4  19539  psgnran  19557  sylow1lem1  19640  lsmmod2  19718  lsmdisj2r  19727  efginvrel2  19769  efgsdmi  19774  efgsrel  19776  efgs1b  19778  efgsp1  19779  efgredleme  19785  efgredlemc  19787  efgcpbllemb  19797  frgpuplem  19814  mulgnn0di  19867  frgpnabllem1  19915  lt6abl  19937  cycsubgcyg  19943  gsumval3eu  19946  gsumval3  19949  gsumzcl2  19952  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  telgsumfz0s  20033  dprdwd  20055  dprd2da  20086  pgpfaclem1  20125  srgbinom  20258  isirred  20445  idomdomd  20748  idomcringd  20749  lspprid2  21019  lspsnat  21170  lsppratlem1  21172  lsppratlem3  21174  lidl0cl  21253  lidlacl  21254  lidlnegcl  21255  elrspsn  21273  2idllidld  21287  2idlridld  21288  rng2idl1cntr  21338  psgnghm  21621  frlmvscavalb  21813  frlmvplusgscavalb  21814  psrbaglefi  21969  psrass23l  22010  psrass23  22012  mplcoe5lem  22080  mpfind  22154  selvval  22162  mhpvscacl  22181  psr1bascl  22223  ply1basf  22225  gsummoncoe1  22333  lply1binom  22335  lply1binomsc  22336  mpfpf1  22376  pf1mpf  22377  evl1scvarpw  22388  evl1maprhm  22404  matbas2i  22449  matecld  22453  matgsum  22464  mpomatmul  22473  dmatmul  22524  1mavmul  22575  mdetleib2  22615  m1detdiag  22624  marep01ma  22687  smadiadetlem4  22696  slesolinv  22707  pmatcollpw3fi1lem1  22813  chpscmat  22869  chpscmatgsumbin  22871  chp0mat  22873  chpidmat  22874  chfacfisf  22881  chfacfisfcpmat  22882  chfacfpmmulgsum2  22892  cldrcl  23055  ordtbas  23221  iscnp2  23268  dis1stc  23528  ptbasfi  23610  ptpjopn  23641  ptclsg  23644  ptcnp  23651  kqtop  23774  reghmph  23822  ptcmplem2  24082  ptcmplem3  24083  ptcmplem4  24084  tsmslem1  24158  utop2nei  24280  isucn2  24309  cuspcvg  24331  cnextucn  24333  imasdsf1olem  24404  blcvx  24839  xrhmeo  24996  cnrehmeo  25003  cnrehmeoOLD  25004  evth  25010  reparphti  25048  reparphtiOLD  25049  iscau4  25332  iscmet3lem1  25344  lmle  25354  rrxfsupp  25455  rrxdsfi  25464  pjthlem2  25491  ovollb2lem  25542  ovolunlem1a  25550  ovoliunlem1  25556  ovoliun2  25560  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem4  25574  iundisj2  25603  voliunlem1  25604  volsup  25610  ioombl1lem4  25615  uniioovol  25633  uniioombllem3  25639  uniioombllem4  25640  uniioombllem6  25642  vitalilem5  25666  mbfimaopnlem  25709  mbflimsup  25720  mbfi1fseqlem3  25772  iblitg  25823  dvcnp2  25975  dvnp1  25981  cpncn  25992  dvmulbr  25995  dvcobr  26003  dvlip2  26054  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumrlimge0  26091  dvfsumrlim2  26093  ftc1cn  26104  elplyd  26261  ply1termlem  26262  ply1term  26263  ply0  26267  plyeq0lem  26269  plyaddlem1  26272  plymullem1  26273  plyaddlem  26274  plymullem  26275  coeeulem  26283  plyco  26300  coeeq2  26301  coefv0  26307  coemulhi  26313  coemulc  26314  plycj  26337  dvply1  26343  vieta1lem2  26371  elqaalem2  26380  dvtaylp  26430  dvntaylp  26431  taylthlem1  26433  taylth  26436  ulmres  26449  ulmshftlem  26450  ulmshft  26451  ulmcau  26456  ulmdvlem1  26461  mtest  26465  mtestbdd  26466  pserulm  26483  psercn2  26484  psercn2OLD  26485  psercnlem1  26487  psercn  26488  pserdvlem2  26490  abelthlem6  26498  abelth  26503  efif1olem1  26602  efif1olem3  26604  efif1olem4  26605  logcn  26707  advlogexp  26715  efopn  26718  cxpeq  26818  asinsin  26953  atantayl  26998  leibpilem2  27002  birthdaylem2  27013  birthdaylem3  27014  efrlim  27030  efrlimOLD  27031  emcllem2  27058  emcllem5  27061  emcllem7  27063  harmonicbnd4  27072  fsumharmonic  27073  lgamgulm2  27097  lgamcvglem  27101  lgamcvg2  27116  gamcvg2lem  27120  wilthlem2  27130  wilthlem3  27131  ftalem1  27134  ftalem2  27135  ftalem3  27136  ftalem5  27138  basellem2  27143  basellem3  27144  basellem5  27146  basellem8  27149  ppiprm  27212  ppinprm  27213  chtprm  27214  chtnprm  27215  chpp1  27216  vma1  27227  ppiltx  27238  musum  27252  0sgmppw  27260  1sgmprm  27261  ppiublem2  27265  chtublem  27273  fsumvma2  27276  chpchtsum  27281  logexprlim  27287  bposlem5  27350  lgscllem  27366  lgsval2lem  27369  lgsval4a  27381  lgsneg  27383  lgsdir2lem3  27389  lgsdir2lem5  27391  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  gausslemma2dlem3  27430  lgseisenlem1  27437  lgsquadlem2  27443  chebbnd1lem1  27531  chtppilimlem1  27535  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrmusum2  27556  dchrvmasum2lem  27558  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0flb  27572  dchrisum0re  27575  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0lem3  27581  mudivsum  27592  mulogsum  27594  mulog2sumlem2  27597  selberg2lem  27612  logdivbnd  27618  pntrsumo1  27627  pntrsumbnd2  27629  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntrlog2bndlem6a  27644  pntlemj  27665  pntlemf  27667  ostth2lem3  27697  madebdayim  27944  oldbdayim  27945  noseqp1  28315  tglngne  28576  ltgseg  28622  eedimeq  28931  axlowdimlem16  28990  ebtwntg  29015  subgruhgredgd  29319  subumgredg2  29320  umgrres1lem  29345  wlkson  29692  wksonproplem  29740  wksonproplemOLD  29741  trlsonfval  29742  pthsonfval  29776  spthson  29777  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  eupth2lems  30270  numclwwlk1lem2foa  30386  numclwlk1lem2  30402  numclwwlk2lem1  30408  htthlem  30949  hhsscms  31310  shmodsi  31421  pjoc1i  31463  5oalem1  31686  mayete3i  31760  adj1  31965  iundisj2f  32612  fmptco1f1o  32652  fcnvgreu  32691  suppovss  32697  ssnnssfz  32792  iundisj2fi  32802  ccatws1f1o  32918  cshw1s2  32927  gsumhashmul  33040  fzo0pmtrlast  33085  wrdpmtrlast  33086  pmtrto1cl  33092  psgnfzto1stlem  33093  fzto1st1  33095  cycpmfv1  33106  cycpmfv2  33107  cycpmco2rn  33118  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cyc3evpm  33143  cyc3genpm  33145  cycpmconjslem2  33148  cyc3conja  33150  erler  33237  idomrcanOLD  33251  nsgmgc  33405  nsgqusf1olem2  33407  unitpidl1  33417  elrspunsn  33422  ssdifidllem  33449  mxidlirredi  33464  mxidlirred  33465  opprqusplusg  33482  opprqus0g  33483  opprqusmulr  33484  idlsrgmulrss1  33504  idlsrgmulrss2  33505  rprmcl  33511  rprmdvds  33512  rprmnz  33513  rprmnunit  33514  rprmasso  33518  rprmirredb  33525  pidufd  33536  1arithufdlem2  33538  1arithufdlem3  33539  zringfrac  33547  ply1dg3rt0irred  33572  m1pmeq  33573  ig1pmindeg  33587  ply1degltdimlem  33635  lindsun  33638  fldextfld1  33662  fldextfld2  33663  rtelextdg2  33718  1smat1  33750  submateqlem2  33754  lmatfval  33760  mdetlap1  33772  madjusmdetlem1  33773  madjusmdetlem2  33774  madjusmdetlem3  33775  madjusmdetlem4  33776  zarclssn  33819  zartopn  33821  zarmxt1  33826  rhmpreimacnlem  33830  rhmpreimacn  33831  pnfneige0  33897  pl1cn  33901  rrhqima  33960  indpreima  33989  esumfzf  34033  esumpcvgval  34042  esumpmono  34043  esumcvg  34050  ldgenpisyslem1  34127  ldgenpisys  34130  measbase  34161  dya2iocnei  34247  oddpwdc  34319  eulerpartlems  34325  eulerpartlemb  34333  sseqf  34357  fibp1  34366  orrvcval4  34429  orrvcoel  34430  orrvccel  34431  ballotlem2  34453  ballotlemfrceq  34493  signsplypnf  34527  signswch  34538  signstf0  34545  signstfvn  34546  signstfvneq0  34549  signstfvcl  34550  signstfveq0  34554  signsvfn  34559  fct2relem  34574  fsum2dsub  34584  reprsuc  34592  reprpmtf1o  34603  breprexplema  34607  breprexplemc  34609  hgt749d  34626  hgt750lemb  34633  tgoldbachgnn  34636  bnj1172  34977  bnj1245  34990  bnj1311  35000  bnj1450  35026  bnj1501  35043  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  subfacval2  35155  erdszelem7  35165  cvxpconn  35210  cvxsconn  35211  cvmliftlem5  35257  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  mrsubvrs  35490  msubrn  35497  msubco  35499  msubvrs  35528  r1peuqusdeg1  35611  imageval  35894  fwddifnp1  36129  knoppcnlem8  36466  knoppcnlem10  36468  bj-unirel  37017  icoreunrn  37325  istoprelowl  37326  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  mblfinlem2  37618  ftc1cnnc  37652  upixp  37689  sdclem2  37702  caushft  37721  ismtyres  37768  rrnmet  37789  rrndstprj1  37790  rrndstprj2  37791  rrncmslem  37792  rrnequiv  37795  iccbnd  37800  osumcllem7N  39919  pexmidlem4N  39930  lcfrlem4  41502  lcfrlem5  41503  lcfrlem6  41504  lcfrlem16  41515  lcfrlem38  41537  mapdrvallem2  41602  mapdh8ab  41734  mapdh8ad  41736  mapdh8e  41741  3factsumint3  41980  aks4d1p1p1  42020  fldhmf1  42047  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1p8  42072  aks6d1c1  42073  evl1gprodd  42074  idomnnzpownz  42089  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c5lem2  42095  deg1gprod  42097  sticksstones10  42112  aks6d1c6lem3  42129  aks5lem2  42144  aks5lem3a  42146  unitscyglem5  42156  metakunt20  42181  fz1sump1  42298  sumcubes  42301  evlselv  42542  mhphf2  42553  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  mapfzcons  42672  diophren  42769  irrapxlem1  42778  monotuz  42898  acongeq  42940  jm2.26lem3  42958  jm3.1lem2  42975  pw2f1ocnv  42994  idomodle  43152  trclfvdecomr  43690  imo72b2lem1  44131  scottelrankd  44216  dvgrat  44281  cvgdvgrat  44282  hashnzfz2  44290  fcnre  44925  refsumcn  44930  rfcnnnub  44936  disjf1o  45098  disjinfi  45099  ssmapsn  45123  ssuzfz  45264  nnsplit  45273  uzssd2  45332  uzublem  45345  fsumsermpt  45500  climsuselem1  45528  limcperiod  45549  sumnnodd  45551  lptioo2cn  45566  lptioo1cn  45567  climresmpt  45580  allbutfifvre  45596  climleltrp  45597  cnrefiisplem  45750  cncfshift  45795  cncfperiod  45800  cncfshiftioo  45813  fperdvper  45840  dvnmptdivc  45859  dvnmul  45864  dvmptfprod  45866  dvnprodlem3  45869  stoweidlem11  45932  stoweidlem15  45936  stoweidlem17  45938  stoweidlem20  45941  stoweidlem34  45955  stoweidlem35  45956  stoweidlem46  45967  stoweidlem47  45968  stoweidlem56  45977  stoweidlem59  45980  stoweidlem62  45983  stirlinglem5  45999  stirlinglem14  46008  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  fourierdlem11  46039  fourierdlem15  46043  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem25  46053  fourierdlem48  46075  fourierdlem52  46079  fourierdlem54  46081  fourierdlem58  46085  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem69  46096  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem80  46107  fourierdlem81  46108  fourierdlem83  46110  fourierdlem92  46119  fourierdlem93  46120  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  fouriercnp  46147  fouriersw  46152  elaa2lem  46154  etransclem4  46159  etransclem7  46162  etransclem10  46165  etransclem14  46169  etransclem15  46170  etransclem24  46179  etransclem25  46180  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem44  46199  etransclem46  46201  qndenserrnopnlem  46218  qndenserrn  46220  prsal  46239  salgencntex  46264  subsaliuncl  46279  subsalsal  46280  sge0tsms  46301  sge0fodjrnlem  46337  sge0isum  46348  iundjiunlem  46380  iundjiun  46381  meadjiunlem  46386  meaiunlelem  46389  meaiuninclem  46401  meaiininc2  46409  caragensplit  46421  carageneld  46423  carageniuncllem1  46442  caratheodorylem1  46447  caratheodorylem2  46448  hoicvr  46469  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem2  46517  hoiqssbllem2  46544  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  smflimlem3  46694  smfmullem4  46715  smfsupxr  46737  smflimsuplem2  46742  smflimsuplem5  46745  natlocalincr  46795  elmod2  47244  isuspgrim0lem  47755  ssnn0ssfz  48074  zlmodzxzscm  48082  rmsupp0  48093  lincsum  48158  lincscm  48159  lindslinindimp2lem4  48190  lincresunit3  48210  elbigofrcl  48284  intubeu  48656  unilbeu  48657  postc  48749  setrec1  48783  aacllem  48895