Theorem eleqtrdi 2843

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 2835	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  eleqtrrdi  2844  3eltr3g  2849  prid2g  4765  ndmfvrcl  6927  fnwelem  8119  tz7.48-1  8445  brwitnlem  8509  oeeulem  8603  dffi3  9428  cnfcom3lem  9700  ttrclse  9724  alephgeom  10079  fpwwe2lem5  10632  canthwelem  10647  hargch  10670  r1wunlim  10734  eluzel2  12829  fseq1p1m1  13577  fznn0sub2  13610  nn0split  13618  seqp1d  13985  exple1  14143  digit1  14202  bcval5  14280  bcpasc  14283  hashf1  14420  seqcoll  14427  seqcoll2  14428  ccatrn  14541  swrdccat2  14621  cats1un  14673  pfxccatin12lem3  14684  splfv2a  14708  splval2  14709  caubnd  15307  limsupgre  15427  clim2ser  15603  clim2ser2  15604  iserex  15605  isermulc2  15606  iserle  15608  iserge0  15609  climub  15610  climserle  15611  isercolllem2  15614  isercolllem3  15615  isercoll  15616  isercoll2  15617  serf0  15629  iseraltlem2  15631  iseraltlem3  15632  iseralt  15633  sumeq2ii  15641  summolem3  15662  summolem2a  15663  fsum  15668  sum0  15669  fsumcl2lem  15679  fsumadd  15688  isumclim3  15707  isumadd  15715  fsump1i  15717  fsummulc2  15732  fsumrelem  15755  iserabs  15763  cvgcmp  15764  cvgcmpub  15765  cvgcmpce  15766  binom1dif  15781  isumshft  15787  isumsplit  15788  isumrpcl  15791  isumsup2  15794  climcndslem1  15797  climcndslem2  15798  climcnds  15799  arisum2  15809  trireciplem  15810  geoser  15815  pwdif  15816  geolim  15818  geo2lim  15823  cvgrat  15831  mertenslem1  15832  mertenslem2  15833  mertens  15834  clim2prod  15836  clim2div  15837  ntrivcvgfvn0  15847  ntrivcvgtail  15848  prodeq2ii  15859  prodmolem3  15879  prodmolem2a  15880  fprod  15887  fprodntriv  15888  fprodss  15894  fprodser  15895  fprodcl2lem  15896  fprodmul  15906  fproddiv  15907  fprodabs  15920  fprodeq0  15921  fprodn0  15925  iprodclim3  15946  iprodmul  15949  fallfacfwd  15982  0fallfac  15983  binomfallfaclem2  15986  fallfacval4  15989  bpolysum  15999  bpolydiflem  16000  fsumkthpow  16002  efcvgfsum  16031  efcj  16037  fprodefsum  16040  effsumlt  16056  ruclem7  16181  bitsfzolem  16377  bitsfzo  16378  bitsfi  16380  bitsinv1lem  16384  bitsinv1  16385  bitsinvp1  16392  sadcp1  16398  sadadd  16410  sadass  16414  bitsres  16416  smupp1  16423  smuval2  16425  smupval  16431  smueqlem  16433  smumul  16436  algrp1  16513  phiprmpw  16711  crth  16713  phimullem  16714  eulerthlem2  16717  prmdiv  16720  pcpremul  16778  pcmpt  16827  pcfac  16834  pockthlem  16840  pockthg  16841  prmreclem2  16852  prmreclem3  16853  prmreclem4  16854  prmreclem5  16855  prmreclem6  16856  prmrec  16857  1arith  16862  vdwapun  16909  vdwlem1  16916  vdwlem2  16917  vdwlem3  16918  vdwlem6  16921  vdwlem8  16923  vdwlem10  16925  vdw  16929  imasvscafn  17485  oppccatid  17667  oppccomfpropd  17675  brcic  17747  funcoppc  17827  invfuc  17929  hofcl  18214  yonedalem4c  18232  gsumwsubmcl  18720  gsumsgrpccat  18723  gsumwmhm  18728  mulgnnp1  18964  mulgnnsubcl  18968  mulgnn0z  18983  mulgnndir  18985  psgnunilem4  19367  psgnran  19385  sylow1lem1  19468  lsmmod2  19546  lsmdisj2r  19555  efginvrel2  19597  efgsdmi  19602  efgsrel  19604  efgs1b  19606  efgsp1  19607  efgredleme  19613  efgredlemc  19615  efgcpbllemb  19625  frgpuplem  19642  mulgnn0di  19695  frgpnabllem1  19743  lt6abl  19765  cycsubgcyg  19771  gsumval3eu  19774  gsumval3  19777  gsumzcl2  19780  gsumzaddlem  19791  gsumconst  19804  gsumzmhm  19807  gsumzoppg  19814  telgsumfz0s  19861  dprdwd  19883  dprd2da  19914  pgpfaclem1  19953  srgbinom  20056  isirred  20237  lspprid2  20614  lspsnat  20764  lsppratlem1  20766  lsppratlem3  20768  lidl0cl  20841  lidlacl  20842  lidlnegcl  20843  lidlmcl  20846  2idllidld  20872  2idlridld  20873  psgnghm  21139  frlmvscavalb  21331  frlmvplusgscavalb  21332  psrbaglefi  21491  psrbaglefiOLD  21492  psrass23l  21534  psrass23  21536  mplcoe5lem  21600  mpfind  21676  selvval  21687  mhpvscacl  21703  psr1bascl  21730  ply1basf  21732  gsummoncoe1  21835  lply1binom  21837  lply1binomsc  21838  mpfpf1  21877  pf1mpf  21878  evl1scvarpw  21889  matbas2i  21931  matecld  21935  matgsum  21946  mpomatmul  21955  dmatmul  22006  1mavmul  22057  mdetleib2  22097  m1detdiag  22106  marep01ma  22169  smadiadetlem4  22178  slesolinv  22189  pmatcollpw3fi1lem1  22295  chpscmat  22351  chpscmatgsumbin  22353  chp0mat  22355  chpidmat  22356  chfacfisf  22363  chfacfisfcpmat  22364  chfacfpmmulgsum2  22374  cldrcl  22537  ordtbas  22703  iscnp2  22750  dis1stc  23010  ptbasfi  23092  ptpjopn  23123  ptclsg  23126  ptcnp  23133  kqtop  23256  reghmph  23304  ptcmplem2  23564  ptcmplem3  23565  ptcmplem4  23566  tsmslem1  23640  utop2nei  23762  isucn2  23791  cuspcvg  23813  cnextucn  23815  imasdsf1olem  23886  blcvx  24321  xrhmeo  24469  cnrehmeo  24476  evth  24482  reparphti  24520  iscau4  24803  iscmet3lem1  24815  lmle  24825  rrxfsupp  24926  rrxdsfi  24935  pjthlem2  24962  ovollb2lem  25012  ovolunlem1a  25020  ovoliunlem1  25026  ovoliun2  25030  ovolscalem1  25037  ovolicc1  25040  ovolicc2lem4  25044  iundisj2  25073  voliunlem1  25074  volsup  25080  ioombl1lem4  25085  uniioovol  25103  uniioombllem3  25109  uniioombllem4  25110  uniioombllem6  25112  vitalilem5  25136  mbfimaopnlem  25179  mbflimsup  25190  mbfi1fseqlem3  25242  iblitg  25293  dvnp1  25449  cpncn  25460  dvlip2  25519  dvfsumlem2  25551  dvfsumlem3  25552  dvfsumrlimge0  25554  dvfsumrlim2  25556  ftc1cn  25567  elplyd  25723  ply1termlem  25724  ply1term  25725  ply0  25729  plyeq0lem  25731  plyaddlem1  25734  plymullem1  25735  plyaddlem  25736  plymullem  25737  coeeulem  25745  plyco  25762  coeeq2  25763  coefv0  25769  coemulhi  25775  coemulc  25776  plycj  25798  dvply1  25804  vieta1lem2  25831  elqaalem2  25840  dvtaylp  25889  dvntaylp  25890  taylthlem1  25892  taylth  25894  ulmres  25907  ulmshftlem  25908  ulmshft  25909  ulmcau  25914  ulmdvlem1  25919  mtest  25923  mtestbdd  25924  pserulm  25941  psercn2  25942  psercnlem1  25944  psercn  25945  pserdvlem2  25947  abelthlem6  25955  abelth  25960  efif1olem1  26058  efif1olem3  26060  efif1olem4  26061  logcn  26162  advlogexp  26170  efopn  26173  cxpeq  26272  asinsin  26404  atantayl  26449  leibpilem2  26453  birthdaylem2  26464  birthdaylem3  26465  efrlim  26481  emcllem2  26508  emcllem5  26511  emcllem7  26513  harmonicbnd4  26522  fsumharmonic  26523  lgamgulm2  26547  lgamcvglem  26551  lgamcvg2  26566  gamcvg2lem  26570  wilthlem2  26580  wilthlem3  26581  ftalem1  26584  ftalem2  26585  ftalem3  26586  ftalem5  26588  basellem2  26593  basellem3  26594  basellem5  26596  basellem8  26599  ppiprm  26662  ppinprm  26663  chtprm  26664  chtnprm  26665  chpp1  26666  vma1  26677  ppiltx  26688  musum  26702  0sgmppw  26708  1sgmprm  26709  ppiublem2  26713  chtublem  26721  fsumvma2  26724  chpchtsum  26729  logexprlim  26735  bposlem5  26798  lgscllem  26814  lgsval2lem  26817  lgsval4a  26829  lgsneg  26831  lgsdir2lem3  26837  lgsdir2lem5  26839  lgsdir  26842  lgsdilem2  26843  lgsdi  26844  lgsne0  26845  gausslemma2dlem3  26878  lgseisenlem1  26885  lgsquadlem2  26891  chebbnd1lem1  26979  chtppilimlem1  26983  rplogsumlem2  26995  rpvmasumlem  26997  dchrisumlem1  26999  dchrisumlem2  27000  dchrmusum2  27004  dchrvmasum2lem  27006  dchrvmasumiflem1  27011  dchrisum0flblem1  27018  dchrisum0flblem2  27019  dchrisum0flb  27020  dchrisum0re  27023  dchrisum0lem1b  27025  dchrisum0lem1  27026  dchrisum0lem2a  27027  dchrisum0lem2  27028  dchrisum0lem3  27029  mudivsum  27040  mulogsum  27042  mulog2sumlem2  27045  selberg2lem  27060  logdivbnd  27066  pntrsumo1  27075  pntrsumbnd2  27077  pntrlog2bndlem2  27088  pntrlog2bndlem4  27090  pntrlog2bndlem6a  27092  pntlemj  27113  pntlemf  27115  ostth2lem3  27145  madebdayim  27390  oldbdayim  27391  tglngne  27839  ltgseg  27885  eedimeq  28194  axlowdimlem16  28253  ebtwntg  28278  subgruhgredgd  28579  subumgredg2  28580  umgrres1lem  28605  wlkson  28951  wksonproplem  28999  wksonproplemOLD  29000  trlsonfval  29001  pthsonfval  29035  spthson  29036  crctcshwlkn0lem4  29105  crctcshwlkn0lem5  29106  eupth2lems  29529  numclwwlk1lem2foa  29645  numclwlk1lem2  29661  numclwwlk2lem1  29667  htthlem  30208  hhsscms  30569  shmodsi  30680  pjoc1i  30722  5oalem1  30945  mayete3i  31019  adj1  31224  iundisj2f  31859  fmptco1f1o  31895  fcnvgreu  31936  suppovss  31944  ssnnssfz  32036  iundisj2fi  32046  cshw1s2  32162  gsumhashmul  32249  pmtrto1cl  32299  psgnfzto1stlem  32300  fzto1st1  32302  cycpmfv1  32313  cycpmfv2  32314  cycpmco2rn  32325  cycpmco2lem4  32329  cycpmco2lem5  32330  cycpmco2lem6  32331  cyc3evpm  32350  cyc3genpm  32352  cycpmconjslem2  32355  cyc3conja  32357  idomdomd  32415  idomringd  32416  idomrcan  32418  rspsnel  32529  nsgmgc  32568  nsgqusf1olem2  32570  ghmquskerlem1  32573  ghmquskerco  32574  unitpidl1  32587  elrspunsn  32592  mxidlirredi  32632  mxidlirred  32633  opprqusplusg  32648  opprqus0g  32649  opprqusmulr  32650  idlsrgmulrss1  32670  idlsrgmulrss2  32671  ig1pmindeg  32718  ply1degltdimlem  32766  lindsun  32769  fldextfld1  32787  fldextfld2  32788  1smat1  32853  submateqlem2  32857  lmatfval  32863  mdetlap1  32875  madjusmdetlem1  32876  madjusmdetlem2  32877  madjusmdetlem3  32878  madjusmdetlem4  32879  zarclssn  32922  zartopn  32924  zarmxt1  32929  rhmpreimacnlem  32933  rhmpreimacn  32934  pnfneige0  33000  pl1cn  33004  rrhqima  33063  indpreima  33092  esumfzf  33136  esumpcvgval  33145  esumpmono  33146  esumcvg  33153  ldgenpisyslem1  33230  ldgenpisys  33233  measbase  33264  dya2iocnei  33350  oddpwdc  33422  eulerpartlems  33428  eulerpartlemb  33436  sseqf  33460  fibp1  33469  orrvcval4  33532  orrvcoel  33533  orrvccel  33534  ballotlem2  33556  ballotlemfrceq  33596  signsplypnf  33630  signswch  33641  signstf0  33648  signstfvn  33649  signstfvneq0  33652  signstfvcl  33653  signstfveq0  33657  signsvfn  33662  fct2relem  33678  fsum2dsub  33688  reprsuc  33696  reprpmtf1o  33707  breprexplema  33711  breprexplemc  33713  hgt749d  33730  hgt750lemb  33737  tgoldbachgnn  33740  bnj1172  34081  bnj1245  34094  bnj1311  34104  bnj1450  34130  bnj1501  34147  subfacp1lem1  34239  subfacp1lem5  34244  subfacp1lem6  34245  subfacval2  34247  erdszelem7  34257  cvxsconn  34303  cvmliftlem5  34349  cvmliftlem7  34351  cvmliftlem10  34354  cvmliftlem13  34356  mrsubvrs  34582  msubrn  34589  msubco  34591  msubvrs  34620  imageval  34971  fwddifnp1  35206  gg-cnrehmeo  35240  gg-reparphti  35241  gg-dvcnp2  35243  gg-dvmulbr  35244  gg-dvcobr  35245  gg-psercn2  35247  gg-dvfsumlem2  35252  knoppcnlem8  35462  knoppcnlem10  35464  bj-unirel  36018  icoreunrn  36326  istoprelowl  36327  poimirlem3  36577  poimirlem4  36578  poimirlem6  36580  poimirlem7  36581  poimirlem8  36582  poimirlem12  36586  poimirlem15  36589  poimirlem16  36590  poimirlem17  36591  poimirlem18  36592  poimirlem19  36593  poimirlem20  36594  poimirlem21  36595  poimirlem22  36596  poimirlem23  36597  poimirlem24  36598  poimirlem25  36599  poimirlem26  36600  poimirlem27  36601  poimirlem28  36602  poimirlem29  36603  poimirlem31  36605  mblfinlem2  36612  ftc1cnnc  36646  upixp  36683  sdclem2  36696  caushft  36715  ismtyres  36762  rrnmet  36783  rrndstprj1  36784  rrndstprj2  36785  rrncmslem  36786  rrnequiv  36789  iccbnd  36794  osumcllem7N  38919  pexmidlem4N  38930  lcfrlem4  40502  lcfrlem5  40503  lcfrlem6  40504  lcfrlem16  40515  lcfrlem38  40537  mapdrvallem2  40602  mapdh8ab  40734  mapdh8ad  40736  mapdh8e  40741  3factsumint3  40974  aks4d1p1p1  41014  fldhmf1  41041  sticksstones10  41057  metakunt20  41090  evlselv  41241  mhphf2  41252  fz1sump1  41290  sumcubes  41293  prjspnfv01  41448  prjspner01  41449  prjspner1  41450  mapfzcons  41536  diophren  41633  irrapxlem1  41642  monotuz  41762  acongeq  41804  jm2.26lem3  41822  jm3.1lem2  41839  pw2f1ocnv  41858  idomodle  42020  trclfvdecomr  42561  imo72b2lem1  43003  scottelrankd  43088  dvgrat  43153  cvgdvgrat  43154  hashnzfz2  43162  fcnre  43791  refsumcn  43796  rfcnnnub  43802  disjf1o  43969  disjinfi  43970  ssmapsn  43994  ssuzfz  44138  nnsplit  44147  uzssd2  44206  uzublem  44219  fsumsermpt  44374  climsuselem1  44402  limcperiod  44423  sumnnodd  44425  lptioo2cn  44440  lptioo1cn  44441  climresmpt  44454  allbutfifvre  44470  climleltrp  44471  cnrefiisplem  44624  cncfshift  44669  cncfperiod  44674  cncfshiftioo  44687  fperdvper  44714  dvnmptdivc  44733  dvnmul  44738  dvmptfprod  44740  dvnprodlem3  44743  stoweidlem11  44806  stoweidlem15  44810  stoweidlem17  44812  stoweidlem20  44815  stoweidlem34  44829  stoweidlem35  44830  stoweidlem46  44841  stoweidlem47  44842  stoweidlem56  44851  stoweidlem59  44854  stoweidlem62  44857  stirlinglem5  44873  stirlinglem14  44882  dirkertrigeqlem2  44894  dirkertrigeqlem3  44895  fourierdlem11  44913  fourierdlem15  44917  fourierdlem16  44918  fourierdlem21  44923  fourierdlem22  44924  fourierdlem25  44927  fourierdlem48  44949  fourierdlem52  44953  fourierdlem54  44955  fourierdlem58  44959  fourierdlem62  44963  fourierdlem64  44965  fourierdlem65  44966  fourierdlem69  44970  fourierdlem70  44971  fourierdlem71  44972  fourierdlem73  44974  fourierdlem80  44981  fourierdlem81  44982  fourierdlem83  44984  fourierdlem92  44993  fourierdlem93  44994  fourierdlem97  44998  fourierdlem103  45004  fourierdlem104  45005  fourierdlem112  45013  fourierdlem113  45014  fouriercnp  45021  fouriersw  45026  elaa2lem  45028  etransclem4  45033  etransclem7  45036  etransclem10  45039  etransclem14  45043  etransclem15  45044  etransclem24  45053  etransclem25  45054  etransclem31  45060  etransclem32  45061  etransclem35  45064  etransclem44  45073  etransclem46  45075  qndenserrnopnlem  45092  qndenserrn  45094  prsal  45113  salgencntex  45138  subsaliuncl  45153  subsalsal  45154  sge0tsms  45175  sge0fodjrnlem  45211  sge0isum  45222  iundjiunlem  45254  iundjiun  45255  meadjiunlem  45260  meaiunlelem  45263  meaiuninclem  45275  meaiininc2  45283  caragensplit  45295  carageneld  45297  carageniuncllem1  45316  caratheodorylem1  45321  caratheodorylem2  45322  hoicvr  45343  hsphoidmvle2  45380  hsphoidmvle  45381  hoidmv1lelem2  45387  hoidmv1lelem3  45388  hoidmvlelem2  45391  hoiqssbllem2  45418  pimdecfgtioc  45510  pimincfltioc  45511  pimdecfgtioo  45512  pimincfltioo  45513  smflimlem3  45568  smfmullem4  45589  smfsupxr  45611  smflimsuplem2  45616  smflimsuplem5  45619  natlocalincr  45669  elmod2  46117  rng2idl1cntr  46869  ssnn0ssfz  47104  zlmodzxzscm  47112  rmsupp0  47123  lincsum  47188  lincscm  47189  lindslinindimp2lem4  47220  lincresunit3  47240  elbigofrcl  47314  intubeu  47687  unilbeu  47688  postc  47780  setrec1  47814  aacllem  47926