Theorem eleqtrdi 2870

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  eleqtrrdi  2871  3eltr3g  2876  prid2g  4722  ndmfvrcl  6912  fnwelem  8130  tz7.48-1  8435  brwitnlem  8497  oeeulem  8592  dffi3  9404  cnfcom3lem  9685  ttrclse  9709  scottelrankd  9890  alephgeom  10088  fpwwe2lem5  10647  canthwelem  10662  hargch  10685  r1wunlim  10749  eluzel2  12895  fseq1p1m1  13656  fznn0sub2  13693  nn0split  13701  seqp1d  14085  exple1  14244  digit1  14304  bcval5  14385  bcpasc  14388  hashf1  14525  seqcoll  14532  seqcoll2  14533  ccatrn  14658  swrdccat2  14742  cats1un  14793  pfxccatin12lem3  14804  splfv2a  14828  splval2  14829  caubnd  15449  limsupgre  15571  clim2ser  15745  clim2ser2  15746  iserex  15747  isermulc2  15748  iserle  15750  iserge0  15751  climub  15752  climserle  15753  isercolllem2  15756  isercolllem3  15757  isercoll  15758  isercoll2  15759  serf0  15771  iseraltlem2  15773  iseraltlem3  15774  iseralt  15775  sumeq2ii  15783  summolem3  15803  summolem2a  15804  fsum  15809  sum0  15810  fsumcl2lem  15820  fsumadd  15829  isumclim3  15848  isumadd  15856  fsump1i  15858  fsummulc2  15873  fsumrelem  15897  iserabs  15905  cvgcmp  15906  cvgcmpub  15907  cvgcmpce  15908  binom1dif  15925  isumshft  15931  isumsplit  15932  isumrpcl  15935  isumsup2  15938  climcndslem1  15941  climcndslem2  15942  climcnds  15943  arisum2  15953  trireciplem  15954  geoser  15959  pwdif  15960  geolim  15962  geo2lim  15967  cvgrat  15975  mertenslem1  15976  mertenslem2  15977  mertens  15978  clim2prod  15980  clim2div  15981  ntrivcvgfvn0  15991  ntrivcvgtail  15992  prodeq2ii  16003  prodmolem3  16023  prodmolem2a  16024  fprod  16031  fprodntriv  16032  fprodss  16038  fprodser  16039  fprodcl2lem  16040  fprodmul  16050  fproddiv  16051  fprodabs  16064  fprodeq0  16065  fprodn0  16069  iprodclim3  16090  iprodmul  16093  fallfacfwd  16125  0fallfac  16126  binomfallfaclem2  16129  fallfacval4  16132  bpolysum  16142  bpolydiflem  16143  fsumkthpow  16145  efcvgfsum  16175  efcj  16181  fprodefsum  16184  effsumlt  16202  ruclem7  16327  bitsfzolem  16527  bitsfzo  16528  bitsfi  16530  bitsinv1lem  16534  bitsinv1  16535  bitsinvp1  16542  sadcp1  16548  sadadd  16560  sadass  16564  bitsres  16566  smupp1  16573  smuval2  16575  smupval  16581  smueqlem  16583  smumul  16586  algrp1  16667  phiprmpw  16870  crth  16872  phimullem  16873  eulerthlem2  16876  prmdiv  16879  pcpremul  16938  pcmpt  16987  pcfac  16994  pockthlem  17000  pockthg  17001  prmreclem2  17012  prmreclem3  17013  prmreclem4  17014  prmreclem5  17015  prmreclem6  17016  prmrec  17017  1arith  17022  vdwapun  17069  vdwlem1  17076  vdwlem2  17077  vdwlem3  17078  vdwlem6  17081  vdwlem8  17083  vdwlem10  17085  vdw  17089  imasvscafn  17626  oppccatid  17810  oppccomfpropd  17818  brcic  17890  funcoppc  17967  invfuc  18069  hofcl  18350  yonedalem4c  18368  chnccats1  18716  gsumwsubmcl  18949  gsumsgrpccat  18952  gsumwmhm  18957  mulgnnp1  19208  mulgnnsubcl  19212  mulgnn0z  19227  mulgnndir  19229  ghmquskerlem1  19413  ghmquskerco  19414  psgnunilem4  19627  psgnran  19645  sylow1lem1  19728  lsmmod2  19806  lsmdisj2r  19815  efginvrel2  19857  efgsdmi  19862  efgsrel  19864  efgs1b  19866  efgsp1  19867  efgredleme  19873  efgredlemc  19875  efgcpbllemb  19885  frgpuplem  19902  mulgnn0di  19955  frgpnabllem1  20003  lt6abl  20025  cycsubgcyg  20031  gsumval3eu  20034  gsumval3  20037  gsumzcl2  20040  gsumzaddlem  20051  gsumconst  20064  gsumzmhm  20067  gsumzoppg  20074  telgsumfz0s  20121  dprdwd  20143  dprd2da  20174  pgpfaclem1  20213  srgbinom  20373  isirred  20563  idomdomd  20890  idomcringd  20891  lspprid2  21185  lspsnat  21335  lsppratlem1  21337  lsppratlem3  21339  lidl0cl  21411  lidlacl  21412  lidlnegcl  21413  elrspsn  21437  2idllidld  21459  2idlridld  21460  rng2idl1cntr  21511  ssdifidllem  21550  psgnghm  21796  frlmvscavalb  21986  frlmvplusgscavalb  21987  psrbaglefi  22144  psrass23l  22184  psrass23  22186  mplcoe5lem  22258  mpfind  22334  selvval  22339  mhpvscacl  22385  psr1bascl  22428  ply1basf  22430  gsummoncoe1  22536  lply1binom  22538  lply1binomsc  22539  mpfpf1  22579  pf1mpf  22580  evl1scvarpw  22591  evl1maprhm  22607  matbas2i  22647  matecld  22651  matgsum  22662  mpomatmul  22671  dmatmul  22722  1mavmul  22773  mdetleib2  22813  m1detdiag  22822  marep01ma  22885  smadiadetlem4  22894  slesolinv  22908  pmatcollpw3fi1lem1  23014  chpscmat  23070  chpscmatgsumbin  23072  chp0mat  23074  chpidmat  23075  chfacfisf  23082  chfacfisfcpmat  23083  chfacfpmmulgsum2  23093  cldrcl  23254  ordtbas  23420  iscnp2  23467  dis1stc  23728  ptbasfi  23810  ptpjopn  23841  ptclsg  23844  ptcnp  23851  kqtop  23974  reghmph  24022  ptcmplem2  24282  ptcmplem3  24283  ptcmplem4  24284  tsmslem1  24358  utop2nei  24479  isucn2  24507  cuspcvg  24529  cnextucn  24531  imasdsf1olem  24602  blcvx  25027  xrhmeo  25177  cnrehmeo  25184  evth  25190  reparphti  25228  iscau4  25510  iscmet3lem1  25522  lmle  25532  rrxfsupp  25633  rrxdsfi  25642  pjthlem2  25669  ovollb2lem  25719  ovolunlem1a  25727  ovoliunlem1  25733  ovoliun2  25737  ovolscalem1  25744  ovolicc1  25747  ovolicc2lem4  25751  iundisj2  25780  voliunlem1  25781  volsup  25787  ioombl1lem4  25792  uniioovol  25810  uniioombllem3  25816  uniioombllem4  25817  uniioombllem6  25819  vitalilem5  25843  mbfimaopnlem  25886  mbflimsup  25897  mbfi1fseqlem3  25948  iblitg  25999  dvcnp2  26150  dvnp1  26155  cpncn  26166  dvmulbr  26169  dvcobr  26176  dvlip2  26225  dvfsumlem2  26257  dvfsumlem3  26258  dvfsumrlimge0  26260  dvfsumrlim2  26262  ftc1cn  26273  elplyd  26430  ply1termlem  26431  ply1term  26432  ply0  26436  plyeq0lem  26439  plyaddlem1  26442  plymullem1  26443  plyaddlem  26444  plymullem  26445  coeeulem  26453  plyco  26470  coeeq2  26471  coefv0  26477  coemulhi  26483  coemulc  26484  plycj  26506  plycjOLD  26508  dvply1  26517  vieta1lem2  26546  elqaalem2  26555  dvtaylp  26609  dvntaylp  26610  taylthlem1  26612  taylth  26614  ulmres  26627  ulmshftlem  26628  ulmshft  26629  ulmcau  26634  ulmdvlem1  26639  mtest  26643  mtestbdd  26644  pserulm  26661  psercn2  26662  psercnlem1  26664  psercn  26665  pserdvlem2  26667  abelthlem6  26675  abelth  26680  efif1olem1  26782  efif1olem3  26784  efif1olem4  26785  logcn  26887  advlogexp  26895  efopn  26898  cxpeq  26997  asinsin  27132  atantayl  27177  leibpilem2  27181  birthdaylem2  27192  birthdaylem3  27193  efrlim  27209  emcllem2  27236  emcllem5  27239  emcllem7  27241  harmonicbnd4  27250  fsumharmonic  27251  lgamgulm2  27275  lgamcvglem  27279  lgamcvg2  27294  gamcvg2lem  27298  wilthlem2  27308  wilthlem3  27309  ftalem1  27312  ftalem2  27313  ftalem3  27314  ftalem5  27316  basellem2  27321  basellem3  27322  basellem5  27324  basellem8  27327  ppiprm  27390  ppinprm  27391  chtprm  27392  chtnprm  27393  chpp1  27394  vma1  27405  ppiltx  27416  musum  27430  0sgmppw  27437  1sgmprm  27438  ppiublem2  27442  chtublem  27450  fsumvma2  27453  chpchtsum  27458  logexprlim  27464  bposlem5  27527  lgscllem  27543  lgsval2lem  27546  lgsval4a  27558  lgsneg  27560  lgsdir2lem3  27566  lgsdir2lem5  27568  lgsdir  27571  lgsdilem2  27572  lgsdi  27573  lgsne0  27574  gausslemma2dlem3  27607  lgseisenlem1  27614  lgsquadlem2  27620  chebbnd1lem1  27708  chtppilimlem1  27712  rplogsumlem2  27724  rpvmasumlem  27726  dchrisumlem1  27728  dchrisumlem2  27729  dchrmusum2  27733  dchrvmasum2lem  27735  dchrvmasumiflem1  27740  dchrisum0flblem1  27747  dchrisum0flblem2  27748  dchrisum0flb  27749  dchrisum0re  27752  dchrisum0lem1b  27754  dchrisum0lem1  27755  dchrisum0lem2a  27756  dchrisum0lem2  27757  dchrisum0lem3  27758  mudivsum  27769  mulogsum  27771  mulog2sumlem2  27774  selberg2lem  27789  logdivbnd  27795  pntrsumo1  27804  pntrsumbnd2  27806  pntrlog2bndlem2  27817  pntrlog2bndlem4  27819  pntrlog2bndlem6a  27821  pntlemj  27842  pntlemf  27844  ostth2lem3  27874  madebdayim  28156  oldbdayim  28157  newbdayim  28171  cutminmax  28204  noseqp1  28559  tglngne  28895  ltgseg  28941  eedimeq  29358  axlowdimlem16  29417  ebtwntg  29442  subgruhgredgd  29747  subumgredg2  29748  umgrres1lem  29773  wlkson  30117  wksonproplem  30169  trlsonfval  30170  pthsonfval  30208  spthson  30209  crctcshwlkn0lem4  30284  crctcshwlkn0lem5  30285  eupth2lems  30721  numclwwlk1lem2foa  30837  numclwlk1lem2  30853  numclwwlk2lem1  30859  htthlem  31401  hhsscms  31762  shmodsi  31873  pjoc1i  31915  5oalem1  32138  mayete3i  32212  adj1  32417  iundisj2f  33066  fmptco1f1o  33109  fcnvgreu  33148  suppovss  33156  ssnnssfz  33261  nn0diffz0  33268  iundisj2fi  33271  indpreima  33314  ccatws1f1o  33396  cshw1s2  33403  gsumhashmul  33510  gsummulsubdishift1  33511  gsumwrd2dccat  33521  fzo0pmtrlast  33535  wrdpmtrlast  33536  pmtrto1cl  33542  psgnfzto1stlem  33543  fzto1st1  33545  cycpmfv1  33556  cycpmfv2  33557  cycpmco2rn  33568  cycpmco2lem4  33572  cycpmco2lem5  33573  cycpmco2lem6  33574  cyc3evpm  33593  cyc3genpm  33595  cycpmconjslem2  33598  cyc3conja  33600  elrgspnlem1  33685  elrgspnlem2  33686  erler  33708  nsgmgc  33844  nsgqusf1olem2  33846  unitpidl1  33855  elrspunsn  33860  mxidlirredi  33877  mxidlirred  33878  opprqusplusg  33894  opprqus0g  33895  opprqusmulr  33896  idlsrgmulrss1  33924  idlsrgmulrss2  33925  rprmcl  33931  rprmdvds  33932  rprmnz  33933  rprmnunit  33934  rprmasso  33938  rprmirredb  33945  pidufd  33956  1arithufdlem2  33958  1arithufdlem3  33959  zringfrac  33967  ply1dg3rt0irred  33997  m1pmeq  33998  ig1pmindeg  34015  selvply1rhmlem2  34034  selvply1rhmlem4  34036  selvply1rhm0  34039  extvfvvcl  34048  evlextv  34055  psrmonprod  34065  esplysply  34084  esplyind  34088  esplyfvn  34090  vietalem  34092  exsslsb  34110  ply1degltdimlem  34135  lindsun  34138  fldextfld1  34160  fldextfld2  34161  rtelextdg2  34240  cos9thpiminplylem1  34295  1smat1  34317  submateqlem2  34321  lmatfval  34327  mdetlap1  34339  madjusmdetlem1  34340  madjusmdetlem2  34341  madjusmdetlem3  34342  madjusmdetlem4  34343  zarclssn  34386  zartopn  34388  zarmxt1  34393  rhmpreimacnlem  34397  rhmpreimacn  34398  pnfneige0  34464  pl1cn  34468  rrhqima  34527  esumfzf  34582  esumpcvgval  34591  esumpmono  34592  esumcvg  34599  ldgenpisyslem1  34677  ldgenpisys  34680  measbase  34711  dya2iocnei  34796  oddpwdc  34868  eulerpartlems  34874  eulerpartlemb  34882  sseqf  34906  fibp1  34915  orrvcval4  34979  orrvcoel  34980  orrvccel  34981  ballotlem2  35003  ballotlemfrceq  35043  signsplypnf  35061  signswch  35072  signstf0  35079  signstfvn  35080  signstfvneq0  35083  signstfvcl  35084  signstfveq0  35088  signsvfn  35093  fct2relem  35108  fsum2dsub  35118  reprsuc  35126  reprpmtf1o  35137  breprexplema  35141  breprexplemc  35143  hgt749d  35160  hgt750lemb  35167  tgoldbachgnn  35170  bnj1172  35513  bnj1245  35526  bnj1311  35536  bnj1450  35562  bnj1501  35579  r1elcl  35608  subfacp1lem1  35761  subfacp1lem5  35766  subfacp1lem6  35767  subfacval2  35769  erdszelem7  35779  cvxpconn  35824  cvxsconn  35825  cvmliftlem5  35871  cvmliftlem7  35873  cvmliftlem10  35876  cvmliftlem13  35878  mrsubvrs  36104  msubrn  36111  msubco  36113  msubvrs  36142  r1peuqusdeg1  36225  imageval  36510  fwddifnp1  36748  knoppcnlem8  37200  knoppcnlem10  37202  bj-unirel  37798  icoreunrn  38116  istoprelowl  38117  poimirlem3  38375  poimirlem4  38376  poimirlem6  38378  poimirlem7  38379  poimirlem8  38380  poimirlem12  38384  poimirlem15  38387  poimirlem16  38388  poimirlem17  38389  poimirlem18  38390  poimirlem19  38391  poimirlem20  38392  poimirlem21  38393  poimirlem22  38394  poimirlem23  38395  poimirlem24  38396  poimirlem25  38397  poimirlem26  38398  poimirlem27  38399  poimirlem28  38400  poimirlem29  38401  poimirlem31  38403  mblfinlem2  38410  ftc1cnnc  38444  upixp  38482  sdclem2  38495  caushft  38514  ismtyres  38561  rrnmet  38582  rrndstprj1  38583  rrndstprj2  38584  rrncmslem  38585  rrnequiv  38588  iccbnd  38593  osumcllem7N  40838  pexmidlem4N  40849  lcfrlem4  42421  lcfrlem5  42422  lcfrlem6  42423  lcfrlem16  42434  lcfrlem38  42456  mapdrvallem2  42521  mapdh8ab  42653  mapdh8ad  42655  mapdh8e  42660  3factsumint3  42892  aks4d1p1p1  42932  fldhmf1  42959  aks6d1c1p2  42978  aks6d1c1p3  42979  aks6d1c1p7  42982  aks6d1c1p6  42983  aks6d1c1p8  42984  aks6d1c1  42985  evl1gprodd  42986  idomnnzpownz  43001  aks6d1c5lem1  43005  aks6d1c5lem3  43006  aks6d1c5lem2  43007  deg1gprod  43009  sticksstones10  43024  aks6d1c6lem3  43041  aks5lem2  43056  aks5lem3a  43058  unitscyglem5  43068  fz1sump1  43188  sumcubes  43191  evlselv  43438  mhphf2  43447  prjspnfv01  43473  prjspner01  43474  prjspner1  43475  mapfzcons  43564  diophren  43657  irrapxlem1  43666  monotuz  43785  acongeq  43827  jm2.26lem3  43845  jm3.1lem2  43862  pw2f1ocnv  43881  idomodle  44035  trclfvdecomr  44571  imo72b2lem0  45008  imo72b2lem1  45012  dvgrat  45139  cvgdvgrat  45140  hashnzfz2  45148  fcnre  45862  refsumcn  45867  rfcnnnub  45873  disjf1o  46026  disjinfi  46027  ssmapsn  46049  ssuzfz  46182  nnsplit  46191  uzssd2  46248  uzublem  46261  fsumsermpt  46412  climsuselem1  46440  limcperiod  46461  sumnnodd  46463  lptioo2cn  46476  lptioo1cn  46477  climresmpt  46490  allbutfifvre  46506  climleltrp  46507  cnrefiisplem  46660  cncfshift  46705  cncfperiod  46710  cncfshiftioo  46723  fperdvper  46750  dvnmptdivc  46769  dvnmul  46774  dvmptfprod  46776  dvnprodlem3  46779  stoweidlem11  46842  stoweidlem15  46846  stoweidlem17  46848  stoweidlem20  46851  stoweidlem34  46865  stoweidlem35  46866  stoweidlem46  46877  stoweidlem47  46878  stoweidlem56  46887  stoweidlem59  46890  stoweidlem62  46893  stirlinglem5  46909  stirlinglem14  46918  dirkertrigeqlem2  46930  dirkertrigeqlem3  46931  fourierdlem11  46949  fourierdlem15  46953  fourierdlem16  46954  fourierdlem21  46959  fourierdlem22  46960  fourierdlem25  46963  fourierdlem48  46985  fourierdlem49  46986  fourierdlem52  46989  fourierdlem54  46991  fourierdlem58  46995  fourierdlem62  46999  fourierdlem64  47001  fourierdlem65  47002  fourierdlem69  47006  fourierdlem70  47007  fourierdlem71  47008  fourierdlem73  47010  fourierdlem80  47017  fourierdlem81  47018  fourierdlem83  47020  fourierdlem92  47029  fourierdlem93  47030  fourierdlem97  47034  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  fourierdlem113  47050  fouriercnp  47057  fouriersw  47062  elaa2lem  47064  etransclem4  47069  etransclem7  47072  etransclem10  47075  etransclem14  47079  etransclem15  47080  etransclem24  47089  etransclem25  47090  etransclem31  47096  etransclem32  47097  etransclem35  47100  etransclem44  47109  etransclem46  47111  qndenserrnopnlem  47128  qndenserrn  47130  prsal  47149  salgencntex  47174  subsaliuncl  47189  subsalsal  47190  sge0tsms  47211  sge0fodjrnlem  47247  sge0isum  47258  iundjiunlem  47290  iundjiun  47291  meadjiunlem  47296  meaiunlelem  47299  meaiuninclem  47311  meaiininc2  47319  caragensplit  47331  carageneld  47333  carageniuncllem1  47352  caratheodorylem1  47357  caratheodorylem2  47358  hoicvr  47379  hsphoidmvle2  47416  hsphoidmvle  47417  hoidmv1lelem2  47423  hoidmv1lelem3  47424  hoidmvlelem2  47427  hoiqssbllem2  47454  pimdecfgtioc  47546  pimincfltioc  47547  pimdecfgtioo  47548  pimincfltioo  47549  smflimlem3  47604  smfmullem4  47625  smfsupxr  47647  smflimsuplem2  47652  smflimsuplem5  47655  ormklocald  47707  chnerlem1  47713  elmod2  48252  isuspgrim0lem  48812  upgrimtrlslem2  48824  ssnn0ssfz  49282  zlmodzxzscm  49290  rmsupp0  49301  lincsum  49362  lincscm  49363  lindslinindimp2lem4  49394  lincresunit3  49414  elbigofrcl  49483  intubeu  49913  unilbeu  49914  cicrcl2  49972  cic1st2nd  49976  imaf1homlem  50036  oppfrcl  50057  eloppf  50062  imasubc  50080  imaid  50083  oppcuprcl5  50130  oppcup3  50138  uptrlem2  50140  uptrlem3  50141  natoppf  50158  elxpcbasex1ALT  50178  elxpcbasex2ALT  50180  swapf1a  50198  swapf2f1oa  50206  swapfida  50209  cofuswapf1  50223  cofuswapf2  50224  fucoppcco  50338  postc  50498  reldmlan2  50546  reldmran2  50547  lanrcl  50550  ranrcl  50551  setrec1  50620  aacllem  50775  crosspaltd  50802  crossp3d  50803  veronesematbasd  50816  veroquaddetzerod  50822