Theorem eleqtrdi 2847

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleqtrrdi  2848  3eltr3g  2853  prid2g  4719  ndmfvrcl  6868  fnwelem  8075  tz7.48-1  8376  brwitnlem  8436  oeeulem  8531  dffi3  9338  cnfcom3lem  9616  ttrclse  9640  alephgeom  9996  fpwwe2lem5  10550  canthwelem  10565  hargch  10588  r1wunlim  10652  eluzel2  12760  fseq1p1m1  13518  fznn0sub2  13555  nn0split  13563  seqp1d  13945  exple1  14104  digit1  14164  bcval5  14245  bcpasc  14248  hashf1  14384  seqcoll  14391  seqcoll2  14392  ccatrn  14517  swrdccat2  14597  cats1un  14648  pfxccatin12lem3  14659  splfv2a  14683  splval2  14684  caubnd  15286  limsupgre  15408  clim2ser  15582  clim2ser2  15583  iserex  15584  isermulc2  15585  iserle  15587  iserge0  15588  climub  15589  climserle  15590  isercolllem2  15593  isercolllem3  15594  isercoll  15595  isercoll2  15596  serf0  15608  iseraltlem2  15610  iseraltlem3  15611  iseralt  15612  sumeq2ii  15620  summolem3  15641  summolem2a  15642  fsum  15647  sum0  15648  fsumcl2lem  15658  fsumadd  15667  isumclim3  15686  isumadd  15694  fsump1i  15696  fsummulc2  15711  fsumrelem  15734  iserabs  15742  cvgcmp  15743  cvgcmpub  15744  cvgcmpce  15745  binom1dif  15760  isumshft  15766  isumsplit  15767  isumrpcl  15770  isumsup2  15773  climcndslem1  15776  climcndslem2  15777  climcnds  15778  arisum2  15788  trireciplem  15789  geoser  15794  pwdif  15795  geolim  15797  geo2lim  15802  cvgrat  15810  mertenslem1  15811  mertenslem2  15812  mertens  15813  clim2prod  15815  clim2div  15816  ntrivcvgfvn0  15826  ntrivcvgtail  15827  prodeq2ii  15838  prodmolem3  15860  prodmolem2a  15861  fprod  15868  fprodntriv  15869  fprodss  15875  fprodser  15876  fprodcl2lem  15877  fprodmul  15887  fproddiv  15888  fprodabs  15901  fprodeq0  15902  fprodn0  15906  iprodclim3  15927  iprodmul  15930  fallfacfwd  15963  0fallfac  15964  binomfallfaclem2  15967  fallfacval4  15970  bpolysum  15980  bpolydiflem  15981  fsumkthpow  15983  efcvgfsum  16013  efcj  16019  fprodefsum  16022  effsumlt  16040  ruclem7  16165  bitsfzolem  16365  bitsfzo  16366  bitsfi  16368  bitsinv1lem  16372  bitsinv1  16373  bitsinvp1  16380  sadcp1  16386  sadadd  16398  sadass  16402  bitsres  16404  smupp1  16411  smuval2  16413  smupval  16419  smueqlem  16421  smumul  16424  algrp1  16505  phiprmpw  16707  crth  16709  phimullem  16710  eulerthlem2  16713  prmdiv  16716  pcpremul  16775  pcmpt  16824  pcfac  16831  pockthlem  16837  pockthg  16838  prmreclem2  16849  prmreclem3  16850  prmreclem4  16851  prmreclem5  16852  prmreclem6  16853  prmrec  16854  1arith  16859  vdwapun  16906  vdwlem1  16913  vdwlem2  16914  vdwlem3  16915  vdwlem6  16918  vdwlem8  16920  vdwlem10  16922  vdw  16926  imasvscafn  17462  oppccatid  17646  oppccomfpropd  17654  brcic  17726  funcoppc  17803  invfuc  17905  hofcl  18186  yonedalem4c  18204  chnccats1  18552  gsumwsubmcl  18766  gsumsgrpccat  18769  gsumwmhm  18774  mulgnnp1  19016  mulgnnsubcl  19020  mulgnn0z  19035  mulgnndir  19037  ghmquskerlem1  19216  ghmquskerco  19217  psgnunilem4  19430  psgnran  19448  sylow1lem1  19531  lsmmod2  19609  lsmdisj2r  19618  efginvrel2  19660  efgsdmi  19665  efgsrel  19667  efgs1b  19669  efgsp1  19670  efgredleme  19676  efgredlemc  19678  efgcpbllemb  19688  frgpuplem  19705  mulgnn0di  19758  frgpnabllem1  19806  lt6abl  19828  cycsubgcyg  19834  gsumval3eu  19837  gsumval3  19840  gsumzcl2  19843  gsumzaddlem  19854  gsumconst  19867  gsumzmhm  19870  gsumzoppg  19877  telgsumfz0s  19924  dprdwd  19946  dprd2da  19977  pgpfaclem1  20016  srgbinom  20170  isirred  20359  idomdomd  20663  idomcringd  20664  lspprid2  20953  lspsnat  21104  lsppratlem1  21106  lsppratlem3  21108  lidl0cl  21179  lidlacl  21180  lidlnegcl  21181  elrspsn  21199  2idllidld  21213  2idlridld  21214  rng2idl1cntr  21264  psgnghm  21539  frlmvscavalb  21729  frlmvplusgscavalb  21730  psrbaglefi  21886  psrass23l  21926  psrass23  21928  mplcoe5lem  21998  mpfind  22074  selvval  22082  mhpvscacl  22101  psr1bascl  22145  ply1basf  22147  gsummoncoe1  22256  lply1binom  22258  lply1binomsc  22259  mpfpf1  22299  pf1mpf  22300  evl1scvarpw  22311  evl1maprhm  22327  matbas2i  22370  matecld  22374  matgsum  22385  mpomatmul  22394  dmatmul  22445  1mavmul  22496  mdetleib2  22536  m1detdiag  22545  marep01ma  22608  smadiadetlem4  22617  slesolinv  22628  pmatcollpw3fi1lem1  22734  chpscmat  22790  chpscmatgsumbin  22792  chp0mat  22794  chpidmat  22795  chfacfisf  22802  chfacfisfcpmat  22803  chfacfpmmulgsum2  22813  cldrcl  22974  ordtbas  23140  iscnp2  23187  dis1stc  23447  ptbasfi  23529  ptpjopn  23560  ptclsg  23563  ptcnp  23570  kqtop  23693  reghmph  23741  ptcmplem2  24001  ptcmplem3  24002  ptcmplem4  24003  tsmslem1  24077  utop2nei  24198  isucn2  24226  cuspcvg  24248  cnextucn  24250  imasdsf1olem  24321  blcvx  24746  xrhmeo  24904  cnrehmeo  24911  cnrehmeoOLD  24912  evth  24918  reparphti  24956  reparphtiOLD  24957  iscau4  25239  iscmet3lem1  25251  lmle  25261  rrxfsupp  25362  rrxdsfi  25371  pjthlem2  25398  ovollb2lem  25449  ovolunlem1a  25457  ovoliunlem1  25463  ovoliun2  25467  ovolscalem1  25474  ovolicc1  25477  ovolicc2lem4  25481  iundisj2  25510  voliunlem1  25511  volsup  25517  ioombl1lem4  25522  uniioovol  25540  uniioombllem3  25546  uniioombllem4  25547  uniioombllem6  25549  vitalilem5  25573  mbfimaopnlem  25616  mbflimsup  25627  mbfi1fseqlem3  25678  iblitg  25729  dvcnp2  25881  dvnp1  25887  cpncn  25898  dvmulbr  25901  dvcobr  25909  dvlip2  25960  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem3  25995  dvfsumrlimge0  25997  dvfsumrlim2  25999  ftc1cn  26010  elplyd  26167  ply1termlem  26168  ply1term  26169  ply0  26173  plyeq0lem  26175  plyaddlem1  26178  plymullem1  26179  plyaddlem  26180  plymullem  26181  coeeulem  26189  plyco  26206  coeeq2  26207  coefv0  26213  coemulhi  26219  coemulc  26220  plycj  26243  plycjOLD  26245  dvply1  26251  vieta1lem2  26279  elqaalem2  26288  dvtaylp  26338  dvntaylp  26339  taylthlem1  26341  taylth  26344  ulmres  26357  ulmshftlem  26358  ulmshft  26359  ulmcau  26364  ulmdvlem1  26369  mtest  26373  mtestbdd  26374  pserulm  26391  psercn2  26392  psercn2OLD  26393  psercnlem1  26395  psercn  26396  pserdvlem2  26398  abelthlem6  26406  abelth  26411  efif1olem1  26511  efif1olem3  26513  efif1olem4  26514  logcn  26616  advlogexp  26624  efopn  26627  cxpeq  26727  asinsin  26862  atantayl  26907  leibpilem2  26911  birthdaylem2  26922  birthdaylem3  26923  efrlim  26939  efrlimOLD  26940  emcllem2  26967  emcllem5  26970  emcllem7  26972  harmonicbnd4  26981  fsumharmonic  26982  lgamgulm2  27006  lgamcvglem  27010  lgamcvg2  27025  gamcvg2lem  27029  wilthlem2  27039  wilthlem3  27040  ftalem1  27043  ftalem2  27044  ftalem3  27045  ftalem5  27047  basellem2  27052  basellem3  27053  basellem5  27055  basellem8  27058  ppiprm  27121  ppinprm  27122  chtprm  27123  chtnprm  27124  chpp1  27125  vma1  27136  ppiltx  27147  musum  27161  0sgmppw  27169  1sgmprm  27170  ppiublem2  27174  chtublem  27182  fsumvma2  27185  chpchtsum  27190  logexprlim  27196  bposlem5  27259  lgscllem  27275  lgsval2lem  27278  lgsval4a  27290  lgsneg  27292  lgsdir2lem3  27298  lgsdir2lem5  27300  lgsdir  27303  lgsdilem2  27304  lgsdi  27305  lgsne0  27306  gausslemma2dlem3  27339  lgseisenlem1  27346  lgsquadlem2  27352  chebbnd1lem1  27440  chtppilimlem1  27444  rplogsumlem2  27456  rpvmasumlem  27458  dchrisumlem1  27460  dchrisumlem2  27461  dchrmusum2  27465  dchrvmasum2lem  27467  dchrvmasumiflem1  27472  dchrisum0flblem1  27479  dchrisum0flblem2  27480  dchrisum0flb  27481  dchrisum0re  27484  dchrisum0lem1b  27486  dchrisum0lem1  27487  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0lem3  27490  mudivsum  27501  mulogsum  27503  mulog2sumlem2  27506  selberg2lem  27521  logdivbnd  27527  pntrsumo1  27536  pntrsumbnd2  27538  pntrlog2bndlem2  27549  pntrlog2bndlem4  27551  pntrlog2bndlem6a  27553  pntlemj  27574  pntlemf  27576  ostth2lem3  27606  madebdayim  27888  oldbdayim  27889  newbdayim  27903  cutminmax  27936  noseqp1  28291  tglngne  28626  ltgseg  28672  eedimeq  28975  axlowdimlem16  29034  ebtwntg  29059  subgruhgredgd  29361  subumgredg2  29362  umgrres1lem  29387  wlkson  29732  wksonproplem  29780  trlsonfval  29781  pthsonfval  29817  spthson  29818  crctcshwlkn0lem4  29890  crctcshwlkn0lem5  29891  eupth2lems  30317  numclwwlk1lem2foa  30433  numclwlk1lem2  30449  numclwwlk2lem1  30455  htthlem  30996  hhsscms  31357  shmodsi  31468  pjoc1i  31510  5oalem1  31733  mayete3i  31807  adj1  32012  iundisj2f  32668  fmptco1f1o  32714  fcnvgreu  32753  suppovss  32762  ssnnssfz  32869  nn0diffz0  32876  iundisj2fi  32879  indpreima  32949  ccatws1f1o  33035  cshw1s2  33044  gsumhashmul  33152  gsummulsubdishift1  33153  gsumwrd2dccat  33162  fzo0pmtrlast  33176  wrdpmtrlast  33177  pmtrto1cl  33183  psgnfzto1stlem  33184  fzto1st1  33186  cycpmfv1  33197  cycpmfv2  33198  cycpmco2rn  33209  cycpmco2lem4  33213  cycpmco2lem5  33214  cycpmco2lem6  33215  cyc3evpm  33234  cyc3genpm  33236  cycpmconjslem2  33239  cyc3conja  33241  elrgspnlem1  33326  elrgspnlem2  33327  erler  33349  idomrcanOLD  33366  nsgmgc  33495  nsgqusf1olem2  33497  unitpidl1  33507  elrspunsn  33512  ssdifidllem  33539  mxidlirredi  33554  mxidlirred  33555  opprqusplusg  33572  opprqus0g  33573  opprqusmulr  33574  idlsrgmulrss1  33594  idlsrgmulrss2  33595  rprmcl  33601  rprmdvds  33602  rprmnz  33603  rprmnunit  33604  rprmasso  33608  rprmirredb  33615  pidufd  33626  1arithufdlem2  33628  1arithufdlem3  33629  zringfrac  33637  ply1dg3rt0irred  33667  m1pmeq  33668  ig1pmindeg  33685  extvfvvcl  33702  evlextv  33709  esplysply  33731  esplyind  33733  esplyfvn  33735  vietalem  33737  exsslsb  33755  ply1degltdimlem  33781  lindsun  33784  fldextfld1  33806  fldextfld2  33807  rtelextdg2  33886  cos9thpiminplylem1  33941  1smat1  33963  submateqlem2  33967  lmatfval  33973  mdetlap1  33985  madjusmdetlem1  33986  madjusmdetlem2  33987  madjusmdetlem3  33988  madjusmdetlem4  33989  zarclssn  34032  zartopn  34034  zarmxt1  34039  rhmpreimacnlem  34043  rhmpreimacn  34044  pnfneige0  34110  pl1cn  34114  rrhqima  34173  esumfzf  34228  esumpcvgval  34237  esumpmono  34238  esumcvg  34245  ldgenpisyslem1  34322  ldgenpisys  34325  measbase  34356  dya2iocnei  34441  oddpwdc  34513  eulerpartlems  34519  eulerpartlemb  34527  sseqf  34551  fibp1  34560  orrvcval4  34624  orrvcoel  34625  orrvccel  34626  ballotlem2  34648  ballotlemfrceq  34688  signsplypnf  34709  signswch  34720  signstf0  34727  signstfvn  34728  signstfvneq0  34731  signstfvcl  34732  signstfveq0  34736  signsvfn  34741  fct2relem  34756  fsum2dsub  34766  reprsuc  34774  reprpmtf1o  34785  breprexplema  34789  breprexplemc  34791  hgt749d  34808  hgt750lemb  34815  tgoldbachgnn  34818  bnj1172  35159  bnj1245  35172  bnj1311  35182  bnj1450  35208  bnj1501  35225  r1elcl  35256  subfacp1lem1  35375  subfacp1lem5  35380  subfacp1lem6  35381  subfacval2  35383  erdszelem7  35393  cvxpconn  35438  cvxsconn  35439  cvmliftlem5  35485  cvmliftlem7  35487  cvmliftlem10  35490  cvmliftlem13  35492  mrsubvrs  35718  msubrn  35725  msubco  35727  msubvrs  35756  r1peuqusdeg1  35839  imageval  36124  fwddifnp1  36361  knoppcnlem8  36702  knoppcnlem10  36704  bj-unirel  37254  icoreunrn  37566  istoprelowl  37567  poimirlem3  37826  poimirlem4  37827  poimirlem6  37829  poimirlem7  37830  poimirlem8  37831  poimirlem12  37835  poimirlem15  37838  poimirlem16  37839  poimirlem17  37840  poimirlem18  37841  poimirlem19  37842  poimirlem20  37843  poimirlem21  37844  poimirlem22  37845  poimirlem23  37846  poimirlem24  37847  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  poimirlem29  37852  poimirlem31  37854  mblfinlem2  37861  ftc1cnnc  37895  upixp  37932  sdclem2  37945  caushft  37964  ismtyres  38011  rrnmet  38032  rrndstprj1  38033  rrndstprj2  38034  rrncmslem  38035  rrnequiv  38038  iccbnd  38043  osumcllem7N  40290  pexmidlem4N  40301  lcfrlem4  41873  lcfrlem5  41874  lcfrlem6  41875  lcfrlem16  41886  lcfrlem38  41908  mapdrvallem2  41973  mapdh8ab  42105  mapdh8ad  42107  mapdh8e  42112  3factsumint3  42345  aks4d1p1p1  42385  fldhmf1  42412  aks6d1c1p2  42431  aks6d1c1p3  42432  aks6d1c1p7  42435  aks6d1c1p6  42436  aks6d1c1p8  42437  aks6d1c1  42438  evl1gprodd  42439  idomnnzpownz  42454  aks6d1c5lem1  42458  aks6d1c5lem3  42459  aks6d1c5lem2  42460  deg1gprod  42462  sticksstones10  42477  aks6d1c6lem3  42494  aks5lem2  42509  aks5lem3a  42511  unitscyglem5  42521  fz1sump1  42632  sumcubes  42635  evlselv  42897  mhphf2  42908  prjspnfv01  42934  prjspner01  42935  prjspner1  42936  mapfzcons  43025  diophren  43122  irrapxlem1  43131  monotuz  43250  acongeq  43292  jm2.26lem3  43310  jm3.1lem2  43327  pw2f1ocnv  43346  idomodle  43500  trclfvdecomr  44036  imo72b2lem0  44473  imo72b2lem1  44477  scottelrankd  44555  dvgrat  44620  cvgdvgrat  44621  hashnzfz2  44629  fcnre  45337  refsumcn  45342  rfcnnnub  45348  disjf1o  45502  disjinfi  45503  ssmapsn  45527  ssuzfz  45661  nnsplit  45670  uzssd2  45728  uzublem  45741  fsumsermpt  45892  climsuselem1  45920  limcperiod  45941  sumnnodd  45943  lptioo2cn  45956  lptioo1cn  45957  climresmpt  45970  allbutfifvre  45986  climleltrp  45987  cnrefiisplem  46140  cncfshift  46185  cncfperiod  46190  cncfshiftioo  46203  fperdvper  46230  dvnmptdivc  46249  dvnmul  46254  dvmptfprod  46256  dvnprodlem3  46259  stoweidlem11  46322  stoweidlem15  46326  stoweidlem17  46328  stoweidlem20  46331  stoweidlem34  46345  stoweidlem35  46346  stoweidlem46  46357  stoweidlem47  46358  stoweidlem56  46367  stoweidlem59  46370  stoweidlem62  46373  stirlinglem5  46389  stirlinglem14  46398  dirkertrigeqlem2  46410  dirkertrigeqlem3  46411  fourierdlem11  46429  fourierdlem15  46433  fourierdlem16  46434  fourierdlem21  46439  fourierdlem22  46440  fourierdlem25  46443  fourierdlem48  46465  fourierdlem52  46469  fourierdlem54  46471  fourierdlem58  46475  fourierdlem62  46479  fourierdlem64  46481  fourierdlem65  46482  fourierdlem69  46486  fourierdlem70  46487  fourierdlem71  46488  fourierdlem73  46490  fourierdlem80  46497  fourierdlem81  46498  fourierdlem83  46500  fourierdlem92  46509  fourierdlem93  46510  fourierdlem97  46514  fourierdlem103  46520  fourierdlem104  46521  fourierdlem112  46529  fourierdlem113  46530  fouriercnp  46537  fouriersw  46542  elaa2lem  46544  etransclem4  46549  etransclem7  46552  etransclem10  46555  etransclem14  46559  etransclem15  46560  etransclem24  46569  etransclem25  46570  etransclem31  46576  etransclem32  46577  etransclem35  46580  etransclem44  46589  etransclem46  46591  qndenserrnopnlem  46608  qndenserrn  46610  prsal  46629  salgencntex  46654  subsaliuncl  46669  subsalsal  46670  sge0tsms  46691  sge0fodjrnlem  46727  sge0isum  46738  iundjiunlem  46770  iundjiun  46771  meadjiunlem  46776  meaiunlelem  46779  meaiuninclem  46791  meaiininc2  46799  caragensplit  46811  carageneld  46813  carageniuncllem1  46832  caratheodorylem1  46837  caratheodorylem2  46838  hoicvr  46859  hsphoidmvle2  46896  hsphoidmvle  46897  hoidmv1lelem2  46903  hoidmv1lelem3  46904  hoidmvlelem2  46907  hoiqssbllem2  46934  pimdecfgtioc  47026  pimincfltioc  47027  pimdecfgtioo  47028  pimincfltioo  47029  smflimlem3  47084  smfmullem4  47105  smfsupxr  47127  smflimsuplem2  47132  smflimsuplem5  47135  ormklocald  47185  natlocalincr  47187  elmod2  47668  isuspgrim0lem  48206  upgrimtrlslem2  48218  ssnn0ssfz  48662  zlmodzxzscm  48670  rmsupp0  48681  lincsum  48742  lincscm  48743  lindslinindimp2lem4  48774  lincresunit3  48794  elbigofrcl  48863  intubeu  49296  unilbeu  49297  cicrcl2  49355  cic1st2nd  49359  imaf1homlem  49419  oppfrcl  49440  eloppf  49445  imasubc  49463  imaid  49466  oppcuprcl5  49513  oppcup3  49521  uptrlem2  49523  uptrlem3  49524  natoppf  49541  elxpcbasex1ALT  49561  elxpcbasex2ALT  49563  swapf1a  49581  swapf2f1oa  49589  swapfida  49592  cofuswapf1  49606  cofuswapf2  49607  fucoppcco  49721  postc  49881  reldmlan2  49929  reldmran2  49930  lanrcl  49933  ranrcl  49934  setrec1  50003  aacllem  50113