Theorem eleqtrdi 2873

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2143

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is used by:  eleqtrrdi  2874  3eltr3g  2879  prid2g  4727  ndmfvrcl  6914  fnwelem  8123  tz7.48-1  8426  brwitnlem  8488  oeeulem  8583  dffi3  9387  cnfcom3lem  9668  ttrclse  9692  scottelrankd  9873  alephgeom  10071  fpwwe2lem5  10624  canthwelem  10639  hargch  10662  r1wunlim  10726  eluzel2  12871  fseq1p1m1  13631  fznn0sub2  13668  nn0split  13676  seqp1d  14059  exple1  14218  digit1  14278  bcval5  14359  bcpasc  14362  hashf1  14499  seqcoll  14506  seqcoll2  14507  ccatrn  14632  swrdccat2  14712  cats1un  14763  pfxccatin12lem3  14774  splfv2a  14798  splval2  14799  caubnd  15415  limsupgre  15537  clim2ser  15711  clim2ser2  15712  iserex  15713  isermulc2  15714  iserle  15716  iserge0  15717  climub  15718  climserle  15719  isercolllem2  15722  isercolllem3  15723  isercoll  15724  isercoll2  15725  serf0  15737  iseraltlem2  15739  iseraltlem3  15740  iseralt  15741  sumeq2ii  15749  summolem3  15770  summolem2a  15771  fsum  15776  sum0  15777  fsumcl2lem  15787  fsumadd  15796  isumclim3  15815  isumadd  15823  fsump1i  15825  fsummulc2  15840  fsumrelem  15864  iserabs  15872  cvgcmp  15873  cvgcmpub  15874  cvgcmpce  15875  binom1dif  15892  isumshft  15898  isumsplit  15899  isumrpcl  15902  isumsup2  15905  climcndslem1  15908  climcndslem2  15909  climcnds  15910  arisum2  15920  trireciplem  15921  geoser  15926  pwdif  15927  geolim  15929  geo2lim  15934  cvgrat  15942  mertenslem1  15943  mertenslem2  15944  mertens  15945  clim2prod  15947  clim2div  15948  ntrivcvgfvn0  15958  ntrivcvgtail  15959  prodeq2ii  15970  prodmolem3  15992  prodmolem2a  15993  fprod  16000  fprodntriv  16001  fprodss  16007  fprodser  16008  fprodcl2lem  16009  fprodmul  16019  fproddiv  16020  fprodabs  16033  fprodeq0  16034  fprodn0  16038  iprodclim3  16059  iprodmul  16062  fallfacfwd  16094  0fallfac  16095  binomfallfaclem2  16098  fallfacval4  16101  bpolysum  16111  bpolydiflem  16112  fsumkthpow  16114  efcvgfsum  16144  efcj  16150  fprodefsum  16153  effsumlt  16171  ruclem7  16296  bitsfzolem  16496  bitsfzo  16497  bitsfi  16499  bitsinv1lem  16503  bitsinv1  16504  bitsinvp1  16511  sadcp1  16517  sadadd  16529  sadass  16533  bitsres  16535  smupp1  16542  smuval2  16544  smupval  16550  smueqlem  16552  smumul  16555  algrp1  16636  phiprmpw  16839  crth  16841  phimullem  16842  eulerthlem2  16845  prmdiv  16848  pcpremul  16907  pcmpt  16956  pcfac  16963  pockthlem  16969  pockthg  16970  prmreclem2  16981  prmreclem3  16982  prmreclem4  16983  prmreclem5  16984  prmreclem6  16985  prmrec  16986  1arith  16991  vdwapun  17038  vdwlem1  17045  vdwlem2  17046  vdwlem3  17047  vdwlem6  17050  vdwlem8  17052  vdwlem10  17054  vdw  17058  imasvscafn  17595  oppccatid  17779  oppccomfpropd  17787  brcic  17859  funcoppc  17936  invfuc  18038  hofcl  18319  yonedalem4c  18337  chnccats1  18685  gsumwsubmcl  18900  gsumsgrpccat  18903  gsumwmhm  18908  mulgnnp1  19152  mulgnnsubcl  19156  mulgnn0z  19171  mulgnndir  19173  ghmquskerlem1  19357  ghmquskerco  19358  psgnunilem4  19571  psgnran  19589  sylow1lem1  19672  lsmmod2  19750  lsmdisj2r  19759  efginvrel2  19801  efgsdmi  19806  efgsrel  19808  efgs1b  19810  efgsp1  19811  efgredleme  19817  efgredlemc  19819  efgcpbllemb  19829  frgpuplem  19846  mulgnn0di  19899  frgpnabllem1  19947  lt6abl  19969  cycsubgcyg  19975  gsumval3eu  19978  gsumval3  19981  gsumzcl2  19984  gsumzaddlem  19995  gsumconst  20008  gsumzmhm  20011  gsumzoppg  20018  telgsumfz0s  20065  dprdwd  20087  dprd2da  20118  pgpfaclem1  20157  srgbinom  20317  isirred  20506  idomdomd  20833  idomcringd  20834  lspprid2  21128  lspsnat  21278  lsppratlem1  21280  lsppratlem3  21282  lidl0cl  21354  lidlacl  21355  lidlnegcl  21356  elrspsn  21380  2idllidld  21402  2idlridld  21403  rng2idl1cntr  21454  ssdifidllem  21493  psgnghm  21739  frlmvscavalb  21929  frlmvplusgscavalb  21930  psrbaglefi  22085  psrass23l  22125  psrass23  22127  mplcoe5lem  22199  mpfind  22275  selvval  22280  mhpvscacl  22326  psr1bascl  22369  ply1basf  22371  gsummoncoe1  22477  lply1binom  22479  lply1binomsc  22480  mpfpf1  22520  pf1mpf  22521  evl1scvarpw  22532  evl1maprhm  22548  matbas2i  22588  matecld  22592  matgsum  22603  mpomatmul  22612  dmatmul  22663  1mavmul  22714  mdetleib2  22754  m1detdiag  22763  marep01ma  22826  smadiadetlem4  22835  slesolinv  22846  pmatcollpw3fi1lem1  22952  chpscmat  23008  chpscmatgsumbin  23010  chp0mat  23012  chpidmat  23013  chfacfisf  23020  chfacfisfcpmat  23021  chfacfpmmulgsum2  23031  cldrcl  23192  ordtbas  23358  iscnp2  23405  dis1stc  23665  ptbasfi  23747  ptpjopn  23778  ptclsg  23781  ptcnp  23788  kqtop  23911  reghmph  23959  ptcmplem2  24219  ptcmplem3  24220  ptcmplem4  24221  tsmslem1  24295  utop2nei  24416  isucn2  24444  cuspcvg  24466  cnextucn  24468  imasdsf1olem  24539  blcvx  24964  xrhmeo  25114  cnrehmeo  25121  evth  25127  reparphti  25165  iscau4  25447  iscmet3lem1  25459  lmle  25469  rrxfsupp  25570  rrxdsfi  25579  pjthlem2  25606  ovollb2lem  25656  ovolunlem1a  25664  ovoliunlem1  25670  ovoliun2  25674  ovolscalem1  25681  ovolicc1  25684  ovolicc2lem4  25688  iundisj2  25717  voliunlem1  25718  volsup  25724  ioombl1lem4  25729  uniioovol  25747  uniioombllem3  25753  uniioombllem4  25754  uniioombllem6  25756  vitalilem5  25780  mbfimaopnlem  25823  mbflimsup  25834  mbfi1fseqlem3  25885  iblitg  25936  dvcnp2  26088  dvnp1  26093  cpncn  26104  dvmulbr  26107  dvcobr  26114  dvlip2  26163  dvfsumlem2  26195  dvfsumlem3  26196  dvfsumrlimge0  26198  dvfsumrlim2  26200  ftc1cn  26211  elplyd  26368  ply1termlem  26369  ply1term  26370  ply0  26374  plyeq0lem  26376  plyaddlem1  26379  plymullem1  26380  plyaddlem  26381  plymullem  26382  coeeulem  26390  plyco  26407  coeeq2  26408  coefv0  26414  coemulhi  26420  coemulc  26421  plycj  26443  plycjOLD  26445  dvply1  26454  vieta1lem2  26481  elqaalem2  26490  dvtaylp  26542  dvntaylp  26543  taylthlem1  26545  taylth  26547  ulmres  26560  ulmshftlem  26561  ulmshft  26562  ulmcau  26567  ulmdvlem1  26572  mtest  26576  mtestbdd  26577  pserulm  26594  psercn2  26595  psercnlem1  26597  psercn  26598  pserdvlem2  26600  abelthlem6  26608  abelth  26613  efif1olem1  26716  efif1olem3  26718  efif1olem4  26719  logcn  26821  advlogexp  26829  efopn  26832  cxpeq  26931  asinsin  27066  atantayl  27111  leibpilem2  27115  birthdaylem2  27126  birthdaylem3  27127  efrlim  27143  emcllem2  27170  emcllem5  27173  emcllem7  27175  harmonicbnd4  27184  fsumharmonic  27185  lgamgulm2  27209  lgamcvglem  27213  lgamcvg2  27228  gamcvg2lem  27232  wilthlem2  27242  wilthlem3  27243  ftalem1  27246  ftalem2  27247  ftalem3  27248  ftalem5  27250  basellem2  27255  basellem3  27256  basellem5  27258  basellem8  27261  ppiprm  27324  ppinprm  27325  chtprm  27326  chtnprm  27327  chpp1  27328  vma1  27339  ppiltx  27350  musum  27364  0sgmppw  27371  1sgmprm  27372  ppiublem2  27376  chtublem  27384  fsumvma2  27387  chpchtsum  27392  logexprlim  27398  bposlem5  27461  lgscllem  27477  lgsval2lem  27480  lgsval4a  27492  lgsneg  27494  lgsdir2lem3  27500  lgsdir2lem5  27502  lgsdir  27505  lgsdilem2  27506  lgsdi  27507  lgsne0  27508  gausslemma2dlem3  27541  lgseisenlem1  27548  lgsquadlem2  27554  chebbnd1lem1  27642  chtppilimlem1  27646  rplogsumlem2  27658  rpvmasumlem  27660  dchrisumlem1  27662  dchrisumlem2  27663  dchrmusum2  27667  dchrvmasum2lem  27669  dchrvmasumiflem1  27674  dchrisum0flblem1  27681  dchrisum0flblem2  27682  dchrisum0flb  27683  dchrisum0re  27686  dchrisum0lem1b  27688  dchrisum0lem1  27689  dchrisum0lem2a  27690  dchrisum0lem2  27691  dchrisum0lem3  27692  mudivsum  27703  mulogsum  27705  mulog2sumlem2  27708  selberg2lem  27723  logdivbnd  27729  pntrsumo1  27738  pntrsumbnd2  27740  pntrlog2bndlem2  27751  pntrlog2bndlem4  27753  pntrlog2bndlem6a  27755  pntlemj  27776  pntlemf  27778  ostth2lem3  27808  madebdayim  28090  oldbdayim  28091  newbdayim  28105  cutminmax  28138  noseqp1  28493  tglngne  28828  ltgseg  28874  eedimeq  29257  axlowdimlem16  29316  ebtwntg  29341  subgruhgredgd  29643  subumgredg2  29644  umgrres1lem  29669  wlkson  30013  wksonproplem  30061  trlsonfval  30062  pthsonfval  30098  spthson  30099  crctcshwlkn0lem4  30171  crctcshwlkn0lem5  30172  eupth2lems  30598  numclwwlk1lem2foa  30714  numclwlk1lem2  30730  numclwwlk2lem1  30736  htthlem  31278  hhsscms  31639  shmodsi  31750  pjoc1i  31792  5oalem1  32015  mayete3i  32089  adj1  32294  iundisj2f  32944  fmptco1f1o  32987  fcnvgreu  33026  suppovss  33035  ssnnssfz  33141  nn0diffz0  33148  iundisj2fi  33151  indpreima  33194  ccatws1f1o  33280  cshw1s2  33289  gsumhashmul  33396  gsummulsubdishift1  33397  gsumwrd2dccat  33407  fzo0pmtrlast  33421  wrdpmtrlast  33422  pmtrto1cl  33428  psgnfzto1stlem  33429  fzto1st1  33431  cycpmfv1  33442  cycpmfv2  33443  cycpmco2rn  33454  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cyc3evpm  33479  cyc3genpm  33481  cycpmconjslem2  33484  cyc3conja  33486  elrgspnlem1  33571  elrgspnlem2  33572  erler  33594  nsgmgc  33730  nsgqusf1olem2  33732  unitpidl1  33741  elrspunsn  33746  mxidlirredi  33763  mxidlirred  33764  opprqusplusg  33780  opprqus0g  33781  opprqusmulr  33782  idlsrgmulrss1  33810  idlsrgmulrss2  33811  rprmcl  33817  rprmdvds  33818  rprmnz  33819  rprmnunit  33820  rprmasso  33824  rprmirredb  33831  pidufd  33842  1arithufdlem2  33844  1arithufdlem3  33845  zringfrac  33853  ply1dg3rt0irred  33883  m1pmeq  33884  ig1pmindeg  33901  selvply1rhmlem2  33920  selvply1rhmlem4  33922  selvply1rhm0  33925  extvfvvcl  33934  evlextv  33941  psrmonprod  33951  esplysply  33970  esplyind  33974  esplyfvn  33976  vietalem  33978  exsslsb  33996  ply1degltdimlem  34021  lindsun  34024  fldextfld1  34046  fldextfld2  34047  rtelextdg2  34126  cos9thpiminplylem1  34181  1smat1  34203  submateqlem2  34207  lmatfval  34213  mdetlap1  34225  madjusmdetlem1  34226  madjusmdetlem2  34227  madjusmdetlem3  34228  madjusmdetlem4  34229  zarclssn  34272  zartopn  34274  zarmxt1  34279  rhmpreimacnlem  34283  rhmpreimacn  34284  pnfneige0  34350  pl1cn  34354  rrhqima  34413  esumfzf  34468  esumpcvgval  34477  esumpmono  34478  esumcvg  34485  ldgenpisyslem1  34562  ldgenpisys  34565  measbase  34596  dya2iocnei  34681  oddpwdc  34753  eulerpartlems  34759  eulerpartlemb  34767  sseqf  34791  fibp1  34800  orrvcval4  34864  orrvcoel  34865  orrvccel  34866  ballotlem2  34888  ballotlemfrceq  34928  signsplypnf  34946  signswch  34957  signstf0  34964  signstfvn  34965  signstfvneq0  34968  signstfvcl  34969  signstfveq0  34973  signsvfn  34978  fct2relem  34993  fsum2dsub  35003  reprsuc  35011  reprpmtf1o  35022  breprexplema  35026  breprexplemc  35028  hgt749d  35045  hgt750lemb  35052  tgoldbachgnn  35055  bnj1172  35398  bnj1245  35411  bnj1311  35421  bnj1450  35447  bnj1501  35464  r1elcl  35500  subfacp1lem1  35679  subfacp1lem5  35684  subfacp1lem6  35685  subfacval2  35687  erdszelem7  35697  cvxpconn  35742  cvxsconn  35743  cvmliftlem5  35789  cvmliftlem7  35791  cvmliftlem10  35794  cvmliftlem13  35796  mrsubvrs  36022  msubrn  36029  msubco  36031  msubvrs  36060  r1peuqusdeg1  36143  imageval  36428  fwddifnp1  36665  knoppcnlem8  37117  knoppcnlem10  37119  bj-unirel  37715  icoreunrn  38033  istoprelowl  38034  poimirlem3  38302  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem12  38311  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  poimirlem29  38328  poimirlem31  38330  mblfinlem2  38337  ftc1cnnc  38371  upixp  38408  sdclem2  38421  caushft  38440  ismtyres  38487  rrnmet  38508  rrndstprj1  38509  rrndstprj2  38510  rrncmslem  38511  rrnequiv  38514  iccbnd  38519  osumcllem7N  40764  pexmidlem4N  40775  lcfrlem4  42347  lcfrlem5  42348  lcfrlem6  42349  lcfrlem16  42360  lcfrlem38  42382  mapdrvallem2  42447  mapdh8ab  42579  mapdh8ad  42581  mapdh8e  42586  3factsumint3  42818  aks4d1p1p1  42858  fldhmf1  42885  aks6d1c1p2  42904  aks6d1c1p3  42905  aks6d1c1p7  42908  aks6d1c1p6  42909  aks6d1c1p8  42910  aks6d1c1  42911  evl1gprodd  42912  idomnnzpownz  42927  aks6d1c5lem1  42931  aks6d1c5lem3  42932  aks6d1c5lem2  42933  deg1gprod  42935  sticksstones10  42950  aks6d1c6lem3  42967  aks5lem2  42982  aks5lem3a  42984  unitscyglem5  42994  fz1sump1  43099  sumcubes  43102  evlselv  43349  mhphf2  43358  prjspnfv01  43384  prjspner01  43385  prjspner1  43386  mapfzcons  43475  diophren  43568  irrapxlem1  43577  monotuz  43696  acongeq  43738  jm2.26lem3  43756  jm3.1lem2  43773  pw2f1ocnv  43792  idomodle  43946  trclfvdecomr  44482  imo72b2lem0  44919  imo72b2lem1  44923  dvgrat  45050  cvgdvgrat  45051  hashnzfz2  45059  fcnre  45773  refsumcn  45778  rfcnnnub  45784  disjf1o  45937  disjinfi  45938  ssmapsn  45960  ssuzfz  46093  nnsplit  46102  uzssd2  46159  uzublem  46172  fsumsermpt  46323  climsuselem1  46351  limcperiod  46372  sumnnodd  46374  lptioo2cn  46387  lptioo1cn  46388  climresmpt  46401  allbutfifvre  46417  climleltrp  46418  cnrefiisplem  46571  cncfshift  46616  cncfperiod  46621  cncfshiftioo  46634  fperdvper  46661  dvnmptdivc  46680  dvnmul  46685  dvmptfprod  46687  dvnprodlem3  46690  stoweidlem11  46753  stoweidlem15  46757  stoweidlem17  46759  stoweidlem20  46762  stoweidlem34  46776  stoweidlem35  46777  stoweidlem46  46788  stoweidlem47  46789  stoweidlem56  46798  stoweidlem59  46801  stoweidlem62  46804  stirlinglem5  46820  stirlinglem14  46829  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  fourierdlem11  46860  fourierdlem15  46864  fourierdlem16  46865  fourierdlem21  46870  fourierdlem22  46871  fourierdlem25  46874  fourierdlem48  46896  fourierdlem49  46897  fourierdlem52  46900  fourierdlem54  46902  fourierdlem58  46906  fourierdlem62  46910  fourierdlem64  46912  fourierdlem65  46913  fourierdlem69  46917  fourierdlem70  46918  fourierdlem71  46919  fourierdlem73  46921  fourierdlem80  46928  fourierdlem81  46929  fourierdlem83  46931  fourierdlem92  46940  fourierdlem93  46941  fourierdlem97  46945  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  fourierdlem113  46961  fouriercnp  46968  fouriersw  46973  elaa2lem  46975  etransclem4  46980  etransclem7  46983  etransclem10  46986  etransclem14  46990  etransclem15  46991  etransclem24  47000  etransclem25  47001  etransclem31  47007  etransclem32  47008  etransclem35  47011  etransclem44  47020  etransclem46  47022  qndenserrnopnlem  47039  qndenserrn  47041  prsal  47060  salgencntex  47085  subsaliuncl  47100  subsalsal  47101  sge0tsms  47122  sge0fodjrnlem  47158  sge0isum  47169  iundjiunlem  47201  iundjiun  47202  meadjiunlem  47207  meaiunlelem  47210  meaiuninclem  47222  meaiininc2  47230  caragensplit  47242  carageneld  47244  carageniuncllem1  47263  caratheodorylem1  47268  caratheodorylem2  47269  hoicvr  47290  hsphoidmvle2  47327  hsphoidmvle  47328  hoidmv1lelem2  47334  hoidmv1lelem3  47335  hoidmvlelem2  47338  hoiqssbllem2  47365  pimdecfgtioc  47457  pimincfltioc  47458  pimdecfgtioo  47459  pimincfltioo  47460  smflimlem3  47515  smfmullem4  47536  smfsupxr  47558  smflimsuplem2  47563  smflimsuplem5  47566  ormklocald  47618  natlocalincr  47620  elmod2  48126  isuspgrim0lem  48686  upgrimtrlslem2  48698  ssnn0ssfz  49157  zlmodzxzscm  49165  rmsupp0  49176  lincsum  49237  lincscm  49238  lindslinindimp2lem4  49269  lincresunit3  49289  elbigofrcl  49358  intubeu  49790  unilbeu  49791  cicrcl2  49849  cic1st2nd  49853  imaf1homlem  49913  oppfrcl  49934  eloppf  49939  imasubc  49957  imaid  49960  oppcuprcl5  50007  oppcup3  50015  uptrlem2  50017  uptrlem3  50018  natoppf  50035  elxpcbasex1ALT  50055  elxpcbasex2ALT  50057  swapf1a  50075  swapf2f1oa  50083  swapfida  50086  cofuswapf1  50100  cofuswapf2  50101  fucoppcco  50215  postc  50375  reldmlan2  50423  reldmran2  50424  lanrcl  50427  ranrcl  50428  setrec1  50497  aacllem  50649  crosspalti  50675  crossp3i  50676