Theorem eleqtrdi 2838

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-clel 2805

This theorem is referenced by:  eleqtrrdi  2839  3eltr3g  2844  prid2g  4761  ndmfvrcl  6927  fnwelem  8130  tz7.48-1  8457  brwitnlem  8521  oeeulem  8615  dffi3  9448  cnfcom3lem  9720  ttrclse  9744  alephgeom  10099  fpwwe2lem5  10652  canthwelem  10667  hargch  10690  r1wunlim  10754  eluzel2  12851  fseq1p1m1  13601  fznn0sub2  13634  nn0split  13642  seqp1d  14009  exple1  14166  digit1  14225  bcval5  14303  bcpasc  14306  hashf1  14444  seqcoll  14451  seqcoll2  14452  ccatrn  14565  swrdccat2  14645  cats1un  14697  pfxccatin12lem3  14708  splfv2a  14732  splval2  14733  caubnd  15331  limsupgre  15451  clim2ser  15627  clim2ser2  15628  iserex  15629  isermulc2  15630  iserle  15632  iserge0  15633  climub  15634  climserle  15635  isercolllem2  15638  isercolllem3  15639  isercoll  15640  isercoll2  15641  serf0  15653  iseraltlem2  15655  iseraltlem3  15656  iseralt  15657  sumeq2ii  15665  summolem3  15686  summolem2a  15687  fsum  15692  sum0  15693  fsumcl2lem  15703  fsumadd  15712  isumclim3  15731  isumadd  15739  fsump1i  15741  fsummulc2  15756  fsumrelem  15779  iserabs  15787  cvgcmp  15788  cvgcmpub  15789  cvgcmpce  15790  binom1dif  15805  isumshft  15811  isumsplit  15812  isumrpcl  15815  isumsup2  15818  climcndslem1  15821  climcndslem2  15822  climcnds  15823  arisum2  15833  trireciplem  15834  geoser  15839  pwdif  15840  geolim  15842  geo2lim  15847  cvgrat  15855  mertenslem1  15856  mertenslem2  15857  mertens  15858  clim2prod  15860  clim2div  15861  ntrivcvgfvn0  15871  ntrivcvgtail  15872  prodeq2ii  15883  prodmolem3  15903  prodmolem2a  15904  fprod  15911  fprodntriv  15912  fprodss  15918  fprodser  15919  fprodcl2lem  15920  fprodmul  15930  fproddiv  15931  fprodabs  15944  fprodeq0  15945  fprodn0  15949  iprodclim3  15970  iprodmul  15973  fallfacfwd  16006  0fallfac  16007  binomfallfaclem2  16010  fallfacval4  16013  bpolysum  16023  bpolydiflem  16024  fsumkthpow  16026  efcvgfsum  16056  efcj  16062  fprodefsum  16065  effsumlt  16081  ruclem7  16206  bitsfzolem  16402  bitsfzo  16403  bitsfi  16405  bitsinv1lem  16409  bitsinv1  16410  bitsinvp1  16417  sadcp1  16423  sadadd  16435  sadass  16439  bitsres  16441  smupp1  16448  smuval2  16450  smupval  16456  smueqlem  16458  smumul  16461  algrp1  16538  phiprmpw  16738  crth  16740  phimullem  16741  eulerthlem2  16744  prmdiv  16747  pcpremul  16805  pcmpt  16854  pcfac  16861  pockthlem  16867  pockthg  16868  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  prmrec  16884  1arith  16889  vdwapun  16936  vdwlem1  16943  vdwlem2  16944  vdwlem3  16945  vdwlem6  16948  vdwlem8  16950  vdwlem10  16952  vdw  16956  imasvscafn  17512  oppccatid  17694  oppccomfpropd  17702  brcic  17774  funcoppc  17854  invfuc  17959  hofcl  18244  yonedalem4c  18262  gsumwsubmcl  18782  gsumsgrpccat  18785  gsumwmhm  18790  mulgnnp1  19030  mulgnnsubcl  19034  mulgnn0z  19049  mulgnndir  19051  ghmquskerlem1  19227  ghmquskerco  19228  psgnunilem4  19445  psgnran  19463  sylow1lem1  19546  lsmmod2  19624  lsmdisj2r  19633  efginvrel2  19675  efgsdmi  19680  efgsrel  19682  efgs1b  19684  efgsp1  19685  efgredleme  19691  efgredlemc  19693  efgcpbllemb  19703  frgpuplem  19720  mulgnn0di  19773  frgpnabllem1  19821  lt6abl  19843  cycsubgcyg  19849  gsumval3eu  19852  gsumval3  19855  gsumzcl2  19858  gsumzaddlem  19869  gsumconst  19882  gsumzmhm  19885  gsumzoppg  19892  telgsumfz0s  19939  dprdwd  19961  dprd2da  19992  pgpfaclem1  20031  srgbinom  20164  isirred  20351  lspprid2  20875  lspsnat  21026  lsppratlem1  21028  lsppratlem3  21030  lidl0cl  21109  lidlacl  21110  lidlnegcl  21111  2idllidld  21141  2idlridld  21142  rng2idl1cntr  21188  idomdomd  21248  idomringd  21249  psgnghm  21505  frlmvscavalb  21697  frlmvplusgscavalb  21698  psrbaglefi  21858  psrbaglefiOLD  21859  psrass23l  21903  psrass23  21905  mplcoe5lem  21970  mpfind  22046  selvval  22054  mhpvscacl  22071  psr1bascl  22112  ply1basf  22114  gsummoncoe1  22220  lply1binom  22222  lply1binomsc  22223  mpfpf1  22263  pf1mpf  22264  evl1scvarpw  22275  matbas2i  22317  matecld  22321  matgsum  22332  mpomatmul  22341  dmatmul  22392  1mavmul  22443  mdetleib2  22483  m1detdiag  22492  marep01ma  22555  smadiadetlem4  22564  slesolinv  22575  pmatcollpw3fi1lem1  22681  chpscmat  22737  chpscmatgsumbin  22739  chp0mat  22741  chpidmat  22742  chfacfisf  22749  chfacfisfcpmat  22750  chfacfpmmulgsum2  22760  cldrcl  22923  ordtbas  23089  iscnp2  23136  dis1stc  23396  ptbasfi  23478  ptpjopn  23509  ptclsg  23512  ptcnp  23519  kqtop  23642  reghmph  23690  ptcmplem2  23950  ptcmplem3  23951  ptcmplem4  23952  tsmslem1  24026  utop2nei  24148  isucn2  24177  cuspcvg  24199  cnextucn  24201  imasdsf1olem  24272  blcvx  24707  xrhmeo  24864  cnrehmeo  24871  cnrehmeoOLD  24872  evth  24878  reparphti  24916  reparphtiOLD  24917  iscau4  25200  iscmet3lem1  25212  lmle  25222  rrxfsupp  25323  rrxdsfi  25332  pjthlem2  25359  ovollb2lem  25410  ovolunlem1a  25418  ovoliunlem1  25424  ovoliun2  25428  ovolscalem1  25435  ovolicc1  25438  ovolicc2lem4  25442  iundisj2  25471  voliunlem1  25472  volsup  25478  ioombl1lem4  25483  uniioovol  25501  uniioombllem3  25507  uniioombllem4  25508  uniioombllem6  25510  vitalilem5  25534  mbfimaopnlem  25577  mbflimsup  25588  mbfi1fseqlem3  25640  iblitg  25691  dvcnp2  25842  dvnp1  25848  cpncn  25859  dvmulbr  25862  dvcobr  25870  dvlip2  25921  dvfsumlem2  25954  dvfsumlem2OLD  25955  dvfsumlem3  25956  dvfsumrlimge0  25958  dvfsumrlim2  25960  ftc1cn  25971  elplyd  26129  ply1termlem  26130  ply1term  26131  ply0  26135  plyeq0lem  26137  plyaddlem1  26140  plymullem1  26141  plyaddlem  26142  plymullem  26143  coeeulem  26151  plyco  26168  coeeq2  26169  coefv0  26175  coemulhi  26181  coemulc  26182  plycj  26205  dvply1  26211  vieta1lem2  26239  elqaalem2  26248  dvtaylp  26298  dvntaylp  26299  taylthlem1  26301  taylth  26304  ulmres  26317  ulmshftlem  26318  ulmshft  26319  ulmcau  26324  ulmdvlem1  26329  mtest  26333  mtestbdd  26334  pserulm  26351  psercn2  26352  psercn2OLD  26353  psercnlem1  26355  psercn  26356  pserdvlem2  26358  abelthlem6  26366  abelth  26371  efif1olem1  26469  efif1olem3  26471  efif1olem4  26472  logcn  26574  advlogexp  26582  efopn  26585  cxpeq  26685  asinsin  26817  atantayl  26862  leibpilem2  26866  birthdaylem2  26877  birthdaylem3  26878  efrlim  26894  efrlimOLD  26895  emcllem2  26922  emcllem5  26925  emcllem7  26927  harmonicbnd4  26936  fsumharmonic  26937  lgamgulm2  26961  lgamcvglem  26965  lgamcvg2  26980  gamcvg2lem  26984  wilthlem2  26994  wilthlem3  26995  ftalem1  26998  ftalem2  26999  ftalem3  27000  ftalem5  27002  basellem2  27007  basellem3  27008  basellem5  27010  basellem8  27013  ppiprm  27076  ppinprm  27077  chtprm  27078  chtnprm  27079  chpp1  27080  vma1  27091  ppiltx  27102  musum  27116  0sgmppw  27124  1sgmprm  27125  ppiublem2  27129  chtublem  27137  fsumvma2  27140  chpchtsum  27145  logexprlim  27151  bposlem5  27214  lgscllem  27230  lgsval2lem  27233  lgsval4a  27245  lgsneg  27247  lgsdir2lem3  27253  lgsdir2lem5  27255  lgsdir  27258  lgsdilem2  27259  lgsdi  27260  lgsne0  27261  gausslemma2dlem3  27294  lgseisenlem1  27301  lgsquadlem2  27307  chebbnd1lem1  27395  chtppilimlem1  27399  rplogsumlem2  27411  rpvmasumlem  27413  dchrisumlem1  27415  dchrisumlem2  27416  dchrmusum2  27420  dchrvmasum2lem  27422  dchrvmasumiflem1  27427  dchrisum0flblem1  27434  dchrisum0flblem2  27435  dchrisum0flb  27436  dchrisum0re  27439  dchrisum0lem1b  27441  dchrisum0lem1  27442  dchrisum0lem2a  27443  dchrisum0lem2  27444  dchrisum0lem3  27445  mudivsum  27456  mulogsum  27458  mulog2sumlem2  27461  selberg2lem  27476  logdivbnd  27482  pntrsumo1  27491  pntrsumbnd2  27493  pntrlog2bndlem2  27504  pntrlog2bndlem4  27506  pntrlog2bndlem6a  27508  pntlemj  27529  pntlemf  27531  ostth2lem3  27561  madebdayim  27807  oldbdayim  27808  noseqp1  28157  tglngne  28347  ltgseg  28393  eedimeq  28702  axlowdimlem16  28761  ebtwntg  28786  subgruhgredgd  29090  subumgredg2  29091  umgrres1lem  29116  wlkson  29463  wksonproplem  29511  wksonproplemOLD  29512  trlsonfval  29513  pthsonfval  29547  spthson  29548  crctcshwlkn0lem4  29617  crctcshwlkn0lem5  29618  eupth2lems  30041  numclwwlk1lem2foa  30157  numclwlk1lem2  30173  numclwwlk2lem1  30179  htthlem  30720  hhsscms  31081  shmodsi  31192  pjoc1i  31234  5oalem1  31457  mayete3i  31531  adj1  31736  iundisj2f  32373  fmptco1f1o  32411  fcnvgreu  32452  suppovss  32458  ssnnssfz  32549  iundisj2fi  32559  cshw1s2  32675  gsumhashmul  32764  pmtrto1cl  32814  psgnfzto1stlem  32815  fzto1st1  32817  cycpmfv1  32828  cycpmfv2  32829  cycpmco2rn  32840  cycpmco2lem4  32844  cycpmco2lem5  32845  cycpmco2lem6  32846  cyc3evpm  32865  cyc3genpm  32867  cycpmconjslem2  32870  cyc3conja  32872  idomrcan  32943  erler  32973  zringfrac  32990  rspsnel  33077  nsgmgc  33116  nsgqusf1olem2  33118  unitpidl1  33129  elrspunsn  33134  mxidlirredi  33174  mxidlirred  33175  opprqusplusg  33190  opprqus0g  33191  opprqusmulr  33192  idlsrgmulrss1  33212  idlsrgmulrss2  33213  m1pmeq  33246  ig1pmindeg  33258  ply1degltdimlem  33306  lindsun  33309  fldextfld1  33327  fldextfld2  33328  1smat1  33395  submateqlem2  33399  lmatfval  33405  mdetlap1  33417  madjusmdetlem1  33418  madjusmdetlem2  33419  madjusmdetlem3  33420  madjusmdetlem4  33421  zarclssn  33464  zartopn  33466  zarmxt1  33471  rhmpreimacnlem  33475  rhmpreimacn  33476  pnfneige0  33542  pl1cn  33546  rrhqima  33605  indpreima  33634  esumfzf  33678  esumpcvgval  33687  esumpmono  33688  esumcvg  33695  ldgenpisyslem1  33772  ldgenpisys  33775  measbase  33806  dya2iocnei  33892  oddpwdc  33964  eulerpartlems  33970  eulerpartlemb  33978  sseqf  34002  fibp1  34011  orrvcval4  34074  orrvcoel  34075  orrvccel  34076  ballotlem2  34098  ballotlemfrceq  34138  signsplypnf  34172  signswch  34183  signstf0  34190  signstfvn  34191  signstfvneq0  34194  signstfvcl  34195  signstfveq0  34199  signsvfn  34204  fct2relem  34219  fsum2dsub  34229  reprsuc  34237  reprpmtf1o  34248  breprexplema  34252  breprexplemc  34254  hgt749d  34271  hgt750lemb  34278  tgoldbachgnn  34281  bnj1172  34622  bnj1245  34635  bnj1311  34645  bnj1450  34671  bnj1501  34688  subfacp1lem1  34779  subfacp1lem5  34784  subfacp1lem6  34785  subfacval2  34787  erdszelem7  34797  cvxpconn  34842  cvxsconn  34843  cvmliftlem5  34889  cvmliftlem7  34891  cvmliftlem10  34894  cvmliftlem13  34896  mrsubvrs  35122  msubrn  35129  msubco  35131  msubvrs  35160  imageval  35516  fwddifnp1  35751  knoppcnlem8  35965  knoppcnlem10  35967  bj-unirel  36520  icoreunrn  36828  istoprelowl  36829  poimirlem3  37085  poimirlem4  37086  poimirlem6  37088  poimirlem7  37089  poimirlem8  37090  poimirlem12  37094  poimirlem15  37097  poimirlem16  37098  poimirlem17  37099  poimirlem18  37100  poimirlem19  37101  poimirlem20  37102  poimirlem21  37103  poimirlem22  37104  poimirlem23  37105  poimirlem24  37106  poimirlem25  37107  poimirlem26  37108  poimirlem27  37109  poimirlem28  37110  poimirlem29  37111  poimirlem31  37113  mblfinlem2  37120  ftc1cnnc  37154  upixp  37191  sdclem2  37204  caushft  37223  ismtyres  37270  rrnmet  37291  rrndstprj1  37292  rrndstprj2  37293  rrncmslem  37294  rrnequiv  37297  iccbnd  37302  osumcllem7N  39424  pexmidlem4N  39435  lcfrlem4  41007  lcfrlem5  41008  lcfrlem6  41009  lcfrlem16  41020  lcfrlem38  41042  mapdrvallem2  41107  mapdh8ab  41239  mapdh8ad  41241  mapdh8e  41246  3factsumint3  41483  aks4d1p1p1  41523  fldhmf1  41550  aks6d1c1p2  41565  aks6d1c1p3  41566  aks6d1c1p7  41569  aks6d1c1p6  41570  aks6d1c1p8  41571  aks6d1c1  41572  evl1gprodd  41573  idomnnzpownz  41587  aks6d1c5lem1  41591  aks6d1c5lem3  41592  aks6d1c5lem2  41593  deg1gprod  41596  sticksstones10  41611  aks6d1c6lem3  41628  metakunt20  41648  evlselv  41792  mhphf2  41803  fz1sump1  41842  sumcubes  41845  prjspnfv01  42020  prjspner01  42021  prjspner1  42022  mapfzcons  42108  diophren  42205  irrapxlem1  42214  monotuz  42334  acongeq  42376  jm2.26lem3  42394  jm3.1lem2  42411  pw2f1ocnv  42430  idomodle  42591  trclfvdecomr  43130  imo72b2lem1  43571  scottelrankd  43656  dvgrat  43721  cvgdvgrat  43722  hashnzfz2  43730  fcnre  44359  refsumcn  44364  rfcnnnub  44370  disjf1o  44536  disjinfi  44537  ssmapsn  44561  ssuzfz  44703  nnsplit  44712  uzssd2  44771  uzublem  44784  fsumsermpt  44939  climsuselem1  44967  limcperiod  44988  sumnnodd  44990  lptioo2cn  45005  lptioo1cn  45006  climresmpt  45019  allbutfifvre  45035  climleltrp  45036  cnrefiisplem  45189  cncfshift  45234  cncfperiod  45239  cncfshiftioo  45252  fperdvper  45279  dvnmptdivc  45298  dvnmul  45303  dvmptfprod  45305  dvnprodlem3  45308  stoweidlem11  45371  stoweidlem15  45375  stoweidlem17  45377  stoweidlem20  45380  stoweidlem34  45394  stoweidlem35  45395  stoweidlem46  45406  stoweidlem47  45407  stoweidlem56  45416  stoweidlem59  45419  stoweidlem62  45422  stirlinglem5  45438  stirlinglem14  45447  dirkertrigeqlem2  45459  dirkertrigeqlem3  45460  fourierdlem11  45478  fourierdlem15  45482  fourierdlem16  45483  fourierdlem21  45488  fourierdlem22  45489  fourierdlem25  45492  fourierdlem48  45514  fourierdlem52  45518  fourierdlem54  45520  fourierdlem58  45524  fourierdlem62  45528  fourierdlem64  45530  fourierdlem65  45531  fourierdlem69  45535  fourierdlem70  45536  fourierdlem71  45537  fourierdlem73  45539  fourierdlem80  45546  fourierdlem81  45547  fourierdlem83  45549  fourierdlem92  45558  fourierdlem93  45559  fourierdlem97  45563  fourierdlem103  45569  fourierdlem104  45570  fourierdlem112  45578  fourierdlem113  45579  fouriercnp  45586  fouriersw  45591  elaa2lem  45593  etransclem4  45598  etransclem7  45601  etransclem10  45604  etransclem14  45608  etransclem15  45609  etransclem24  45618  etransclem25  45619  etransclem31  45625  etransclem32  45626  etransclem35  45629  etransclem44  45638  etransclem46  45640  qndenserrnopnlem  45657  qndenserrn  45659  prsal  45678  salgencntex  45703  subsaliuncl  45718  subsalsal  45719  sge0tsms  45740  sge0fodjrnlem  45776  sge0isum  45787  iundjiunlem  45819  iundjiun  45820  meadjiunlem  45825  meaiunlelem  45828  meaiuninclem  45840  meaiininc2  45848  caragensplit  45860  carageneld  45862  carageniuncllem1  45881  caratheodorylem1  45886  caratheodorylem2  45887  hoicvr  45908  hsphoidmvle2  45945  hsphoidmvle  45946  hoidmv1lelem2  45952  hoidmv1lelem3  45953  hoidmvlelem2  45956  hoiqssbllem2  45983  pimdecfgtioc  46075  pimincfltioc  46076  pimdecfgtioo  46077  pimincfltioo  46078  smflimlem3  46133  smfmullem4  46154  smfsupxr  46176  smflimsuplem2  46181  smflimsuplem5  46184  natlocalincr  46234  elmod2  46682  isuspgrim0lem  47141  ssnn0ssfz  47385  zlmodzxzscm  47393  rmsupp0  47404  lincsum  47469  lincscm  47470  lindslinindimp2lem4  47501  lincresunit3  47521  elbigofrcl  47595  intubeu  47967  unilbeu  47968  postc  48060  setrec1  48094  aacllem  48206