Theorem eleqtrdi 2849

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eleqtrrdi  2850  3eltr3g  2855  prid2g  4694  ndmfvrcl  6861  fnwelem  8072  tz7.48-1  8373  brwitnlem  8433  oeeulem  8528  dffi3  9335  cnfcom3lem  9616  ttrclse  9640  alephgeom  9996  fpwwe2lem5  10550  canthwelem  10565  hargch  10588  r1wunlim  10652  eluzel2  12785  fseq1p1m1  13544  fznn0sub2  13581  nn0split  13589  seqp1d  13972  exple1  14131  digit1  14191  bcval5  14272  bcpasc  14275  hashf1  14411  seqcoll  14418  seqcoll2  14419  ccatrn  14544  swrdccat2  14624  cats1un  14675  pfxccatin12lem3  14686  splfv2a  14710  splval2  14711  caubnd  15313  limsupgre  15435  clim2ser  15609  clim2ser2  15610  iserex  15611  isermulc2  15612  iserle  15614  iserge0  15615  climub  15616  climserle  15617  isercolllem2  15620  isercolllem3  15621  isercoll  15622  isercoll2  15623  serf0  15635  iseraltlem2  15637  iseraltlem3  15638  iseralt  15639  sumeq2ii  15647  summolem3  15668  summolem2a  15669  fsum  15674  sum0  15675  fsumcl2lem  15685  fsumadd  15694  isumclim3  15713  isumadd  15721  fsump1i  15723  fsummulc2  15738  fsumrelem  15762  iserabs  15770  cvgcmp  15771  cvgcmpub  15772  cvgcmpce  15773  binom1dif  15790  isumshft  15796  isumsplit  15797  isumrpcl  15800  isumsup2  15803  climcndslem1  15806  climcndslem2  15807  climcnds  15808  arisum2  15818  trireciplem  15819  geoser  15824  pwdif  15825  geolim  15827  geo2lim  15832  cvgrat  15840  mertenslem1  15841  mertenslem2  15842  mertens  15843  clim2prod  15845  clim2div  15846  ntrivcvgfvn0  15856  ntrivcvgtail  15857  prodeq2ii  15868  prodmolem3  15890  prodmolem2a  15891  fprod  15898  fprodntriv  15899  fprodss  15905  fprodser  15906  fprodcl2lem  15907  fprodmul  15917  fproddiv  15918  fprodabs  15931  fprodeq0  15932  fprodn0  15936  iprodclim3  15957  iprodmul  15960  fallfacfwd  15993  0fallfac  15994  binomfallfaclem2  15997  fallfacval4  16000  bpolysum  16010  bpolydiflem  16011  fsumkthpow  16013  efcvgfsum  16043  efcj  16049  fprodefsum  16052  effsumlt  16070  ruclem7  16195  bitsfzolem  16395  bitsfzo  16396  bitsfi  16398  bitsinv1lem  16402  bitsinv1  16403  bitsinvp1  16410  sadcp1  16416  sadadd  16428  sadass  16432  bitsres  16434  smupp1  16441  smuval2  16443  smupval  16449  smueqlem  16451  smumul  16454  algrp1  16535  phiprmpw  16738  crth  16740  phimullem  16741  eulerthlem2  16744  prmdiv  16747  pcpremul  16806  pcmpt  16855  pcfac  16862  pockthlem  16868  pockthg  16869  prmreclem2  16880  prmreclem3  16881  prmreclem4  16882  prmreclem5  16883  prmreclem6  16884  prmrec  16885  1arith  16890  vdwapun  16937  vdwlem1  16944  vdwlem2  16945  vdwlem3  16946  vdwlem6  16949  vdwlem8  16951  vdwlem10  16953  vdw  16957  imasvscafn  17493  oppccatid  17677  oppccomfpropd  17685  brcic  17757  funcoppc  17834  invfuc  17936  hofcl  18217  yonedalem4c  18235  chnccats1  18583  gsumwsubmcl  18797  gsumsgrpccat  18800  gsumwmhm  18805  mulgnnp1  19050  mulgnnsubcl  19054  mulgnn0z  19069  mulgnndir  19071  ghmquskerlem1  19250  ghmquskerco  19251  psgnunilem4  19464  psgnran  19482  sylow1lem1  19565  lsmmod2  19643  lsmdisj2r  19652  efginvrel2  19694  efgsdmi  19699  efgsrel  19701  efgs1b  19703  efgsp1  19704  efgredleme  19710  efgredlemc  19712  efgcpbllemb  19722  frgpuplem  19739  mulgnn0di  19792  frgpnabllem1  19840  lt6abl  19862  cycsubgcyg  19868  gsumval3eu  19871  gsumval3  19874  gsumzcl2  19877  gsumzaddlem  19888  gsumconst  19901  gsumzmhm  19904  gsumzoppg  19911  telgsumfz0s  19958  dprdwd  19980  dprd2da  20011  pgpfaclem1  20050  srgbinom  20204  isirred  20391  idomdomd  20699  idomcringd  20700  lspprid2  20989  lspsnat  21139  lsppratlem1  21141  lsppratlem3  21143  lidl0cl  21214  lidlacl  21215  lidlnegcl  21216  elrspsn  21234  2idllidld  21248  2idlridld  21249  rng2idl1cntr  21299  psgnghm  21556  frlmvscavalb  21746  frlmvplusgscavalb  21747  psrbaglefi  21902  psrass23l  21942  psrass23  21944  mplcoe5lem  22016  mpfind  22092  selvval  22097  mhpvscacl  22143  psr1bascl  22186  ply1basf  22188  gsummoncoe1  22295  lply1binom  22297  lply1binomsc  22298  mpfpf1  22338  pf1mpf  22339  evl1scvarpw  22350  evl1maprhm  22366  matbas2i  22406  matecld  22410  matgsum  22421  mpomatmul  22430  dmatmul  22481  1mavmul  22532  mdetleib2  22572  m1detdiag  22581  marep01ma  22644  smadiadetlem4  22653  slesolinv  22664  pmatcollpw3fi1lem1  22770  chpscmat  22826  chpscmatgsumbin  22828  chp0mat  22830  chpidmat  22831  chfacfisf  22838  chfacfisfcpmat  22839  chfacfpmmulgsum2  22849  cldrcl  23010  ordtbas  23176  iscnp2  23223  dis1stc  23483  ptbasfi  23565  ptpjopn  23596  ptclsg  23599  ptcnp  23606  kqtop  23729  reghmph  23777  ptcmplem2  24037  ptcmplem3  24038  ptcmplem4  24039  tsmslem1  24113  utop2nei  24234  isucn2  24262  cuspcvg  24284  cnextucn  24286  imasdsf1olem  24357  blcvx  24782  xrhmeo  24932  cnrehmeo  24939  evth  24945  reparphti  24983  iscau4  25265  iscmet3lem1  25277  lmle  25287  rrxfsupp  25388  rrxdsfi  25397  pjthlem2  25424  ovollb2lem  25474  ovolunlem1a  25482  ovoliunlem1  25488  ovoliun2  25492  ovolscalem1  25499  ovolicc1  25502  ovolicc2lem4  25506  iundisj2  25535  voliunlem1  25536  volsup  25542  ioombl1lem4  25547  uniioovol  25565  uniioombllem3  25571  uniioombllem4  25572  uniioombllem6  25574  vitalilem5  25598  mbfimaopnlem  25641  mbflimsup  25652  mbfi1fseqlem3  25703  iblitg  25754  dvcnp2  25906  dvnp1  25911  cpncn  25922  dvmulbr  25925  dvcobr  25932  dvlip2  25981  dvfsumlem2  26013  dvfsumlem3  26014  dvfsumrlimge0  26016  dvfsumrlim2  26018  ftc1cn  26029  elplyd  26186  ply1termlem  26187  ply1term  26188  ply0  26192  plyeq0lem  26194  plyaddlem1  26197  plymullem1  26198  plyaddlem  26199  plymullem  26200  coeeulem  26208  plyco  26225  coeeq2  26226  coefv0  26232  coemulhi  26238  coemulc  26239  plycj  26261  plycjOLD  26263  dvply1  26269  vieta1lem2  26296  elqaalem2  26305  dvtaylp  26354  dvntaylp  26355  taylthlem1  26357  taylth  26359  ulmres  26372  ulmshftlem  26373  ulmshft  26374  ulmcau  26379  ulmdvlem1  26384  mtest  26388  mtestbdd  26389  pserulm  26406  psercn2  26407  psercnlem1  26409  psercn  26410  pserdvlem2  26412  abelthlem6  26420  abelth  26425  efif1olem1  26525  efif1olem3  26527  efif1olem4  26528  logcn  26630  advlogexp  26638  efopn  26641  cxpeq  26740  asinsin  26875  atantayl  26920  leibpilem2  26924  birthdaylem2  26935  birthdaylem3  26936  efrlim  26952  emcllem2  26979  emcllem5  26982  emcllem7  26984  harmonicbnd4  26993  fsumharmonic  26994  lgamgulm2  27018  lgamcvglem  27022  lgamcvg2  27037  gamcvg2lem  27041  wilthlem2  27051  wilthlem3  27052  ftalem1  27055  ftalem2  27056  ftalem3  27057  ftalem5  27059  basellem2  27064  basellem3  27065  basellem5  27067  basellem8  27070  ppiprm  27133  ppinprm  27134  chtprm  27135  chtnprm  27136  chpp1  27137  vma1  27148  ppiltx  27159  musum  27173  0sgmppw  27180  1sgmprm  27181  ppiublem2  27185  chtublem  27193  fsumvma2  27196  chpchtsum  27201  logexprlim  27207  bposlem5  27270  lgscllem  27286  lgsval2lem  27289  lgsval4a  27301  lgsneg  27303  lgsdir2lem3  27309  lgsdir2lem5  27311  lgsdir  27314  lgsdilem2  27315  lgsdi  27316  lgsne0  27317  gausslemma2dlem3  27350  lgseisenlem1  27357  lgsquadlem2  27363  chebbnd1lem1  27451  chtppilimlem1  27455  rplogsumlem2  27467  rpvmasumlem  27469  dchrisumlem1  27471  dchrisumlem2  27472  dchrmusum2  27476  dchrvmasum2lem  27478  dchrvmasumiflem1  27483  dchrisum0flblem1  27490  dchrisum0flblem2  27491  dchrisum0flb  27492  dchrisum0re  27495  dchrisum0lem1b  27497  dchrisum0lem1  27498  dchrisum0lem2a  27499  dchrisum0lem2  27500  dchrisum0lem3  27501  mudivsum  27512  mulogsum  27514  mulog2sumlem2  27517  selberg2lem  27532  logdivbnd  27538  pntrsumo1  27547  pntrsumbnd2  27549  pntrlog2bndlem2  27560  pntrlog2bndlem4  27562  pntrlog2bndlem6a  27564  pntlemj  27585  pntlemf  27587  ostth2lem3  27617  madebdayim  27899  oldbdayim  27900  newbdayim  27914  cutminmax  27947  noseqp1  28302  tglngne  28637  ltgseg  28683  eedimeq  28986  axlowdimlem16  29045  ebtwntg  29070  subgruhgredgd  29372  subumgredg2  29373  umgrres1lem  29398  wlkson  29742  wksonproplem  29790  trlsonfval  29791  pthsonfval  29827  spthson  29828  crctcshwlkn0lem4  29900  crctcshwlkn0lem5  29901  eupth2lems  30327  numclwwlk1lem2foa  30443  numclwlk1lem2  30459  numclwwlk2lem1  30465  htthlem  31007  hhsscms  31368  shmodsi  31479  pjoc1i  31521  5oalem1  31744  mayete3i  31818  adj1  32023  iundisj2f  32680  fmptco1f1o  32726  fcnvgreu  32765  suppovss  32774  ssnnssfz  32880  nn0diffz0  32887  iundisj2fi  32890  indpreima  32945  ccatws1f1o  33031  cshw1s2  33040  gsumhashmul  33149  gsummulsubdishift1  33150  gsumwrd2dccat  33160  fzo0pmtrlast  33174  wrdpmtrlast  33175  pmtrto1cl  33181  psgnfzto1stlem  33182  fzto1st1  33184  cycpmfv1  33195  cycpmfv2  33196  cycpmco2rn  33207  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cyc3evpm  33232  cyc3genpm  33234  cycpmconjslem2  33237  cyc3conja  33239  elrgspnlem1  33324  elrgspnlem2  33325  erler  33347  idomrcanOLD  33364  nsgmgc  33496  nsgqusf1olem2  33498  unitpidl1  33508  elrspunsn  33513  ssdifidllem  33540  mxidlirredi  33555  mxidlirred  33556  opprqusplusg  33573  opprqus0g  33574  opprqusmulr  33575  idlsrgmulrss1  33603  idlsrgmulrss2  33604  rprmcl  33610  rprmdvds  33611  rprmnz  33612  rprmnunit  33613  rprmasso  33617  rprmirredb  33624  pidufd  33635  1arithufdlem2  33637  1arithufdlem3  33638  zringfrac  33646  ply1dg3rt0irred  33676  m1pmeq  33677  ig1pmindeg  33694  selvply1rhmlem2  33714  selvply1rhmlem4  33716  selvply1rhm0  33719  extvfvvcl  33728  evlextv  33735  psrmonprod  33745  esplysply  33764  esplyind  33768  esplyfvn  33770  vietalem  33772  exsslsb  33790  ply1degltdimlem  33815  lindsun  33818  fldextfld1  33840  fldextfld2  33841  rtelextdg2  33920  cos9thpiminplylem1  33975  1smat1  33997  submateqlem2  34001  lmatfval  34007  mdetlap1  34019  madjusmdetlem1  34020  madjusmdetlem2  34021  madjusmdetlem3  34022  madjusmdetlem4  34023  zarclssn  34066  zartopn  34068  zarmxt1  34073  rhmpreimacnlem  34077  rhmpreimacn  34078  pnfneige0  34144  pl1cn  34148  rrhqima  34207  esumfzf  34262  esumpcvgval  34271  esumpmono  34272  esumcvg  34279  ldgenpisyslem1  34356  ldgenpisys  34359  measbase  34390  dya2iocnei  34475  oddpwdc  34547  eulerpartlems  34553  eulerpartlemb  34561  sseqf  34585  fibp1  34594  orrvcval4  34658  orrvcoel  34659  orrvccel  34660  ballotlem2  34682  ballotlemfrceq  34722  signsplypnf  34743  signswch  34754  signstf0  34761  signstfvn  34762  signstfvneq0  34765  signstfvcl  34766  signstfveq0  34770  signsvfn  34775  fct2relem  34790  fsum2dsub  34800  reprsuc  34808  reprpmtf1o  34819  breprexplema  34823  breprexplemc  34825  hgt749d  34842  hgt750lemb  34849  tgoldbachgnn  34852  bnj1172  35192  bnj1245  35205  bnj1311  35215  bnj1450  35241  bnj1501  35258  r1elcl  35288  subfacp1lem1  35416  subfacp1lem5  35421  subfacp1lem6  35422  subfacval2  35424  erdszelem7  35434  cvxpconn  35479  cvxsconn  35480  cvmliftlem5  35526  cvmliftlem7  35528  cvmliftlem10  35531  cvmliftlem13  35533  mrsubvrs  35759  msubrn  35766  msubco  35768  msubvrs  35797  r1peuqusdeg1  35880  imageval  36165  fwddifnp1  36402  knoppcnlem8  36815  knoppcnlem10  36817  bj-unirel  37413  icoreunrn  37730  istoprelowl  37731  poimirlem3  37999  poimirlem4  38000  poimirlem6  38002  poimirlem7  38003  poimirlem8  38004  poimirlem12  38008  poimirlem15  38011  poimirlem16  38012  poimirlem17  38013  poimirlem18  38014  poimirlem19  38015  poimirlem20  38016  poimirlem21  38017  poimirlem22  38018  poimirlem23  38019  poimirlem24  38020  poimirlem25  38021  poimirlem26  38022  poimirlem27  38023  poimirlem28  38024  poimirlem29  38025  poimirlem31  38027  mblfinlem2  38034  ftc1cnnc  38068  upixp  38105  sdclem2  38118  caushft  38137  ismtyres  38184  rrnmet  38205  rrndstprj1  38206  rrndstprj2  38207  rrncmslem  38208  rrnequiv  38211  iccbnd  38216  osumcllem7N  40463  pexmidlem4N  40474  lcfrlem4  42046  lcfrlem5  42047  lcfrlem6  42048  lcfrlem16  42059  lcfrlem38  42081  mapdrvallem2  42146  mapdh8ab  42278  mapdh8ad  42280  mapdh8e  42285  3factsumint3  42517  aks4d1p1p1  42557  fldhmf1  42584  aks6d1c1p2  42603  aks6d1c1p3  42604  aks6d1c1p7  42607  aks6d1c1p6  42608  aks6d1c1p8  42609  aks6d1c1  42610  evl1gprodd  42611  idomnnzpownz  42626  aks6d1c5lem1  42630  aks6d1c5lem3  42631  aks6d1c5lem2  42632  deg1gprod  42634  sticksstones10  42649  aks6d1c6lem3  42666  aks5lem2  42681  aks5lem3a  42683  unitscyglem5  42693  fz1sump1  42796  sumcubes  42799  evlselv  43048  mhphf2  43057  prjspnfv01  43083  prjspner01  43084  prjspner1  43085  mapfzcons  43174  diophren  43267  irrapxlem1  43276  monotuz  43395  acongeq  43437  jm2.26lem3  43455  jm3.1lem2  43472  pw2f1ocnv  43491  idomodle  43645  trclfvdecomr  44181  imo72b2lem0  44618  imo72b2lem1  44622  scottelrankd  44700  dvgrat  44765  cvgdvgrat  44766  hashnzfz2  44774  fcnre  45482  refsumcn  45487  rfcnnnub  45493  disjf1o  45646  disjinfi  45647  ssmapsn  45669  ssuzfz  45802  nnsplit  45811  uzssd2  45868  uzublem  45881  fsumsermpt  46032  climsuselem1  46060  limcperiod  46081  sumnnodd  46083  lptioo2cn  46096  lptioo1cn  46097  climresmpt  46110  allbutfifvre  46126  climleltrp  46127  cnrefiisplem  46280  cncfshift  46325  cncfperiod  46330  cncfshiftioo  46343  fperdvper  46370  dvnmptdivc  46389  dvnmul  46394  dvmptfprod  46396  dvnprodlem3  46399  stoweidlem11  46462  stoweidlem15  46466  stoweidlem17  46468  stoweidlem20  46471  stoweidlem34  46485  stoweidlem35  46486  stoweidlem46  46497  stoweidlem47  46498  stoweidlem56  46507  stoweidlem59  46510  stoweidlem62  46513  stirlinglem5  46529  stirlinglem14  46538  dirkertrigeqlem2  46550  dirkertrigeqlem3  46551  fourierdlem11  46569  fourierdlem15  46573  fourierdlem16  46574  fourierdlem21  46579  fourierdlem22  46580  fourierdlem25  46583  fourierdlem48  46605  fourierdlem52  46609  fourierdlem54  46611  fourierdlem58  46615  fourierdlem62  46619  fourierdlem64  46621  fourierdlem65  46622  fourierdlem69  46626  fourierdlem70  46627  fourierdlem71  46628  fourierdlem73  46630  fourierdlem80  46637  fourierdlem81  46638  fourierdlem83  46640  fourierdlem92  46649  fourierdlem93  46650  fourierdlem97  46654  fourierdlem103  46660  fourierdlem104  46661  fourierdlem112  46669  fourierdlem113  46670  fouriercnp  46677  fouriersw  46682  elaa2lem  46684  etransclem4  46689  etransclem7  46692  etransclem10  46695  etransclem14  46699  etransclem15  46700  etransclem24  46709  etransclem25  46710  etransclem31  46716  etransclem32  46717  etransclem35  46720  etransclem44  46729  etransclem46  46731  qndenserrnopnlem  46748  qndenserrn  46750  prsal  46769  salgencntex  46794  subsaliuncl  46809  subsalsal  46810  sge0tsms  46831  sge0fodjrnlem  46867  sge0isum  46878  iundjiunlem  46910  iundjiun  46911  meadjiunlem  46916  meaiunlelem  46919  meaiuninclem  46931  meaiininc2  46939  caragensplit  46951  carageneld  46953  carageniuncllem1  46972  caratheodorylem1  46977  caratheodorylem2  46978  hoicvr  46999  hsphoidmvle2  47036  hsphoidmvle  47037  hoidmv1lelem2  47043  hoidmv1lelem3  47044  hoidmvlelem2  47047  hoiqssbllem2  47074  pimdecfgtioc  47166  pimincfltioc  47167  pimdecfgtioo  47168  pimincfltioo  47169  smflimlem3  47224  smfmullem4  47245  smfsupxr  47267  smflimsuplem2  47272  smflimsuplem5  47275  ormklocald  47327  natlocalincr  47329  elmod2  47832  isuspgrim0lem  48392  upgrimtrlslem2  48404  ssnn0ssfz  48848  zlmodzxzscm  48856  rmsupp0  48867  lincsum  48928  lincscm  48929  lindslinindimp2lem4  48960  lincresunit3  48980  elbigofrcl  49049  intubeu  49482  unilbeu  49483  cicrcl2  49541  cic1st2nd  49545  imaf1homlem  49605  oppfrcl  49626  eloppf  49631  imasubc  49649  imaid  49652  oppcuprcl5  49699  oppcup3  49707  uptrlem2  49709  uptrlem3  49710  natoppf  49727  elxpcbasex1ALT  49747  elxpcbasex2ALT  49749  swapf1a  49767  swapf2f1oa  49775  swapfida  49778  cofuswapf1  49792  cofuswapf2  49793  fucoppcco  49907  postc  50067  reldmlan2  50115  reldmran2  50116  lanrcl  50119  ranrcl  50120  setrec1  50189  aacllem  50299