Theorem eleqtrdi 2848

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eleqtrrdi  2849  3eltr3g  2854  prid2g  4765  ndmfvrcl  6942  fnwelem  8154  tz7.48-1  8481  brwitnlem  8543  oeeulem  8637  dffi3  9468  cnfcom3lem  9740  ttrclse  9764  alephgeom  10119  fpwwe2lem5  10672  canthwelem  10687  hargch  10710  r1wunlim  10774  eluzel2  12880  fseq1p1m1  13634  fznn0sub2  13671  nn0split  13679  seqp1d  14055  exple1  14212  digit1  14272  bcval5  14353  bcpasc  14356  hashf1  14492  seqcoll  14499  seqcoll2  14500  ccatrn  14623  swrdccat2  14703  cats1un  14755  pfxccatin12lem3  14766  splfv2a  14790  splval2  14791  caubnd  15393  limsupgre  15513  clim2ser  15687  clim2ser2  15688  iserex  15689  isermulc2  15690  iserle  15692  iserge0  15693  climub  15694  climserle  15695  isercolllem2  15698  isercolllem3  15699  isercoll  15700  isercoll2  15701  serf0  15713  iseraltlem2  15715  iseraltlem3  15716  iseralt  15717  sumeq2ii  15725  summolem3  15746  summolem2a  15747  fsum  15752  sum0  15753  fsumcl2lem  15763  fsumadd  15772  isumclim3  15791  isumadd  15799  fsump1i  15801  fsummulc2  15816  fsumrelem  15839  iserabs  15847  cvgcmp  15848  cvgcmpub  15849  cvgcmpce  15850  binom1dif  15865  isumshft  15871  isumsplit  15872  isumrpcl  15875  isumsup2  15878  climcndslem1  15881  climcndslem2  15882  climcnds  15883  arisum2  15893  trireciplem  15894  geoser  15899  pwdif  15900  geolim  15902  geo2lim  15907  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  mertens  15918  clim2prod  15920  clim2div  15921  ntrivcvgfvn0  15931  ntrivcvgtail  15932  prodeq2ii  15943  prodmolem3  15965  prodmolem2a  15966  fprod  15973  fprodntriv  15974  fprodss  15980  fprodser  15981  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodabs  16006  fprodeq0  16007  fprodn0  16011  iprodclim3  16032  iprodmul  16035  fallfacfwd  16068  0fallfac  16069  binomfallfaclem2  16072  fallfacval4  16075  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  efcvgfsum  16118  efcj  16124  fprodefsum  16127  effsumlt  16143  ruclem7  16268  bitsfzolem  16467  bitsfzo  16468  bitsfi  16470  bitsinv1lem  16474  bitsinv1  16475  bitsinvp1  16482  sadcp1  16488  sadadd  16500  sadass  16504  bitsres  16506  smupp1  16513  smuval2  16515  smupval  16521  smueqlem  16523  smumul  16526  algrp1  16607  phiprmpw  16809  crth  16811  phimullem  16812  eulerthlem2  16815  prmdiv  16818  pcpremul  16876  pcmpt  16925  pcfac  16932  pockthlem  16938  pockthg  16939  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  prmrec  16955  1arith  16960  vdwapun  17007  vdwlem1  17014  vdwlem2  17015  vdwlem3  17016  vdwlem6  17019  vdwlem8  17021  vdwlem10  17023  vdw  17027  imasvscafn  17583  oppccatid  17765  oppccomfpropd  17773  brcic  17845  funcoppc  17925  invfuc  18030  hofcl  18315  yonedalem4c  18333  gsumwsubmcl  18862  gsumsgrpccat  18865  gsumwmhm  18870  mulgnnp1  19112  mulgnnsubcl  19116  mulgnn0z  19131  mulgnndir  19133  ghmquskerlem1  19313  ghmquskerco  19314  psgnunilem4  19529  psgnran  19547  sylow1lem1  19630  lsmmod2  19708  lsmdisj2r  19717  efginvrel2  19759  efgsdmi  19764  efgsrel  19766  efgs1b  19768  efgsp1  19769  efgredleme  19775  efgredlemc  19777  efgcpbllemb  19787  frgpuplem  19804  mulgnn0di  19857  frgpnabllem1  19905  lt6abl  19927  cycsubgcyg  19933  gsumval3eu  19936  gsumval3  19939  gsumzcl2  19942  gsumzaddlem  19953  gsumconst  19966  gsumzmhm  19969  gsumzoppg  19976  telgsumfz0s  20023  dprdwd  20045  dprd2da  20076  pgpfaclem1  20115  srgbinom  20248  isirred  20435  idomdomd  20742  idomcringd  20743  lspprid2  21013  lspsnat  21164  lsppratlem1  21166  lsppratlem3  21168  lidl0cl  21247  lidlacl  21248  lidlnegcl  21249  elrspsn  21267  2idllidld  21281  2idlridld  21282  rng2idl1cntr  21332  psgnghm  21615  frlmvscavalb  21807  frlmvplusgscavalb  21808  psrbaglefi  21963  psrass23l  22004  psrass23  22006  mplcoe5lem  22074  mpfind  22148  selvval  22156  mhpvscacl  22175  psr1bascl  22217  ply1basf  22219  gsummoncoe1  22327  lply1binom  22329  lply1binomsc  22330  mpfpf1  22370  pf1mpf  22371  evl1scvarpw  22382  evl1maprhm  22398  matbas2i  22443  matecld  22447  matgsum  22458  mpomatmul  22467  dmatmul  22518  1mavmul  22569  mdetleib2  22609  m1detdiag  22618  marep01ma  22681  smadiadetlem4  22690  slesolinv  22701  pmatcollpw3fi1lem1  22807  chpscmat  22863  chpscmatgsumbin  22865  chp0mat  22867  chpidmat  22868  chfacfisf  22875  chfacfisfcpmat  22876  chfacfpmmulgsum2  22886  cldrcl  23049  ordtbas  23215  iscnp2  23262  dis1stc  23522  ptbasfi  23604  ptpjopn  23635  ptclsg  23638  ptcnp  23645  kqtop  23768  reghmph  23816  ptcmplem2  24076  ptcmplem3  24077  ptcmplem4  24078  tsmslem1  24152  utop2nei  24274  isucn2  24303  cuspcvg  24325  cnextucn  24327  imasdsf1olem  24398  blcvx  24833  xrhmeo  24990  cnrehmeo  24997  cnrehmeoOLD  24998  evth  25004  reparphti  25042  reparphtiOLD  25043  iscau4  25326  iscmet3lem1  25338  lmle  25348  rrxfsupp  25449  rrxdsfi  25458  pjthlem2  25485  ovollb2lem  25536  ovolunlem1a  25544  ovoliunlem1  25550  ovoliun2  25554  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem4  25568  iundisj2  25597  voliunlem1  25598  volsup  25604  ioombl1lem4  25609  uniioovol  25627  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  vitalilem5  25660  mbfimaopnlem  25703  mbflimsup  25714  mbfi1fseqlem3  25766  iblitg  25817  dvcnp2  25969  dvnp1  25975  cpncn  25986  dvmulbr  25989  dvcobr  25997  dvlip2  26048  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumrlimge0  26085  dvfsumrlim2  26087  ftc1cn  26098  elplyd  26255  ply1termlem  26256  ply1term  26257  ply0  26261  plyeq0lem  26263  plyaddlem1  26266  plymullem1  26267  plyaddlem  26268  plymullem  26269  coeeulem  26277  plyco  26294  coeeq2  26295  coefv0  26301  coemulhi  26307  coemulc  26308  plycj  26331  plycjOLD  26333  dvply1  26339  vieta1lem2  26367  elqaalem2  26376  dvtaylp  26426  dvntaylp  26427  taylthlem1  26429  taylth  26432  ulmres  26445  ulmshftlem  26446  ulmshft  26447  ulmcau  26452  ulmdvlem1  26457  mtest  26461  mtestbdd  26462  pserulm  26479  psercn2  26480  psercn2OLD  26481  psercnlem1  26483  psercn  26484  pserdvlem2  26486  abelthlem6  26494  abelth  26499  efif1olem1  26598  efif1olem3  26600  efif1olem4  26601  logcn  26703  advlogexp  26711  efopn  26714  cxpeq  26814  asinsin  26949  atantayl  26994  leibpilem2  26998  birthdaylem2  27009  birthdaylem3  27010  efrlim  27026  efrlimOLD  27027  emcllem2  27054  emcllem5  27057  emcllem7  27059  harmonicbnd4  27068  fsumharmonic  27069  lgamgulm2  27093  lgamcvglem  27097  lgamcvg2  27112  gamcvg2lem  27116  wilthlem2  27126  wilthlem3  27127  ftalem1  27130  ftalem2  27131  ftalem3  27132  ftalem5  27134  basellem2  27139  basellem3  27140  basellem5  27142  basellem8  27145  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  chpp1  27212  vma1  27223  ppiltx  27234  musum  27248  0sgmppw  27256  1sgmprm  27257  ppiublem2  27261  chtublem  27269  fsumvma2  27272  chpchtsum  27277  logexprlim  27283  bposlem5  27346  lgscllem  27362  lgsval2lem  27365  lgsval4a  27377  lgsneg  27379  lgsdir2lem3  27385  lgsdir2lem5  27387  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  gausslemma2dlem3  27426  lgseisenlem1  27433  lgsquadlem2  27439  chebbnd1lem1  27527  chtppilimlem1  27531  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrmusum2  27552  dchrvmasum2lem  27554  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0flb  27568  dchrisum0re  27571  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  mudivsum  27588  mulogsum  27590  mulog2sumlem2  27593  selberg2lem  27608  logdivbnd  27614  pntrsumo1  27623  pntrsumbnd2  27625  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem6a  27640  pntlemj  27661  pntlemf  27663  ostth2lem3  27693  madebdayim  27940  oldbdayim  27941  noseqp1  28311  tglngne  28572  ltgseg  28618  eedimeq  28927  axlowdimlem16  28986  ebtwntg  29011  subgruhgredgd  29315  subumgredg2  29316  umgrres1lem  29341  wlkson  29688  wksonproplem  29736  wksonproplemOLD  29737  trlsonfval  29738  pthsonfval  29772  spthson  29773  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  eupth2lems  30266  numclwwlk1lem2foa  30382  numclwlk1lem2  30398  numclwwlk2lem1  30404  htthlem  30945  hhsscms  31306  shmodsi  31417  pjoc1i  31459  5oalem1  31682  mayete3i  31756  adj1  31961  iundisj2f  32609  fmptco1f1o  32649  fcnvgreu  32689  suppovss  32695  ssnnssfz  32795  iundisj2fi  32804  ccatws1f1o  32920  cshw1s2  32929  gsumhashmul  33046  gsumwrd2dccat  33052  fzo0pmtrlast  33094  wrdpmtrlast  33095  pmtrto1cl  33101  psgnfzto1stlem  33102  fzto1st1  33104  cycpmfv1  33115  cycpmfv2  33116  cycpmco2rn  33127  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cyc3evpm  33152  cyc3genpm  33154  cycpmconjslem2  33157  cyc3conja  33159  elrgspnlem1  33231  elrgspnlem2  33232  erler  33251  idomrcanOLD  33265  nsgmgc  33419  nsgqusf1olem2  33421  unitpidl1  33431  elrspunsn  33436  ssdifidllem  33463  mxidlirredi  33478  mxidlirred  33479  opprqusplusg  33496  opprqus0g  33497  opprqusmulr  33498  idlsrgmulrss1  33518  idlsrgmulrss2  33519  rprmcl  33525  rprmdvds  33526  rprmnz  33527  rprmnunit  33528  rprmasso  33532  rprmirredb  33539  pidufd  33550  1arithufdlem2  33552  1arithufdlem3  33553  zringfrac  33561  ply1dg3rt0irred  33586  m1pmeq  33587  ig1pmindeg  33601  ply1degltdimlem  33649  lindsun  33652  fldextfld1  33676  fldextfld2  33677  rtelextdg2  33732  1smat1  33764  submateqlem2  33768  lmatfval  33774  mdetlap1  33786  madjusmdetlem1  33787  madjusmdetlem2  33788  madjusmdetlem3  33789  madjusmdetlem4  33790  zarclssn  33833  zartopn  33835  zarmxt1  33840  rhmpreimacnlem  33844  rhmpreimacn  33845  pnfneige0  33911  pl1cn  33915  rrhqima  33976  indpreima  34005  esumfzf  34049  esumpcvgval  34058  esumpmono  34059  esumcvg  34066  ldgenpisyslem1  34143  ldgenpisys  34146  measbase  34177  dya2iocnei  34263  oddpwdc  34335  eulerpartlems  34341  eulerpartlemb  34349  sseqf  34373  fibp1  34382  orrvcval4  34445  orrvcoel  34446  orrvccel  34447  ballotlem2  34469  ballotlemfrceq  34509  signsplypnf  34543  signswch  34554  signstf0  34561  signstfvn  34562  signstfvneq0  34565  signstfvcl  34566  signstfveq0  34570  signsvfn  34575  fct2relem  34590  fsum2dsub  34600  reprsuc  34608  reprpmtf1o  34619  breprexplema  34623  breprexplemc  34625  hgt749d  34642  hgt750lemb  34649  tgoldbachgnn  34652  bnj1172  34993  bnj1245  35006  bnj1311  35016  bnj1450  35042  bnj1501  35059  subfacp1lem1  35163  subfacp1lem5  35168  subfacp1lem6  35169  subfacval2  35171  erdszelem7  35181  cvxpconn  35226  cvxsconn  35227  cvmliftlem5  35273  cvmliftlem7  35275  cvmliftlem10  35278  cvmliftlem13  35280  mrsubvrs  35506  msubrn  35513  msubco  35515  msubvrs  35544  r1peuqusdeg1  35627  imageval  35911  fwddifnp1  36146  knoppcnlem8  36482  knoppcnlem10  36484  bj-unirel  37033  icoreunrn  37341  istoprelowl  37342  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  mblfinlem2  37644  ftc1cnnc  37678  upixp  37715  sdclem2  37728  caushft  37747  ismtyres  37794  rrnmet  37815  rrndstprj1  37816  rrndstprj2  37817  rrncmslem  37818  rrnequiv  37821  iccbnd  37826  osumcllem7N  39944  pexmidlem4N  39955  lcfrlem4  41527  lcfrlem5  41528  lcfrlem6  41529  lcfrlem16  41540  lcfrlem38  41562  mapdrvallem2  41627  mapdh8ab  41759  mapdh8ad  41761  mapdh8e  41766  3factsumint3  42004  aks4d1p1p1  42044  fldhmf1  42071  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c1  42097  evl1gprodd  42098  idomnnzpownz  42113  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  sticksstones10  42136  aks6d1c6lem3  42153  aks5lem2  42168  aks5lem3a  42170  unitscyglem5  42180  metakunt20  42205  fz1sump1  42322  sumcubes  42325  evlselv  42573  mhphf2  42584  prjspnfv01  42610  prjspner01  42611  prjspner1  42612  mapfzcons  42703  diophren  42800  irrapxlem1  42809  monotuz  42929  acongeq  42971  jm2.26lem3  42989  jm3.1lem2  43006  pw2f1ocnv  43025  idomodle  43179  trclfvdecomr  43717  imo72b2lem0  44154  imo72b2lem1  44158  scottelrankd  44242  dvgrat  44307  cvgdvgrat  44308  hashnzfz2  44316  fcnre  44962  refsumcn  44967  rfcnnnub  44973  disjf1o  45133  disjinfi  45134  ssmapsn  45158  ssuzfz  45298  nnsplit  45307  uzssd2  45366  uzublem  45379  fsumsermpt  45534  climsuselem1  45562  limcperiod  45583  sumnnodd  45585  lptioo2cn  45600  lptioo1cn  45601  climresmpt  45614  allbutfifvre  45630  climleltrp  45631  cnrefiisplem  45784  cncfshift  45829  cncfperiod  45834  cncfshiftioo  45847  fperdvper  45874  dvnmptdivc  45893  dvnmul  45898  dvmptfprod  45900  dvnprodlem3  45903  stoweidlem11  45966  stoweidlem15  45970  stoweidlem17  45972  stoweidlem20  45975  stoweidlem34  45989  stoweidlem35  45990  stoweidlem46  46001  stoweidlem47  46002  stoweidlem56  46011  stoweidlem59  46014  stoweidlem62  46017  stirlinglem5  46033  stirlinglem14  46042  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  fourierdlem11  46073  fourierdlem15  46077  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem25  46087  fourierdlem48  46109  fourierdlem52  46113  fourierdlem54  46115  fourierdlem58  46119  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem69  46130  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem80  46141  fourierdlem81  46142  fourierdlem83  46144  fourierdlem92  46153  fourierdlem93  46154  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  fouriercnp  46181  fouriersw  46186  elaa2lem  46188  etransclem4  46193  etransclem7  46196  etransclem10  46199  etransclem14  46203  etransclem15  46204  etransclem24  46213  etransclem25  46214  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem44  46233  etransclem46  46235  qndenserrnopnlem  46252  qndenserrn  46254  prsal  46273  salgencntex  46298  subsaliuncl  46313  subsalsal  46314  sge0tsms  46335  sge0fodjrnlem  46371  sge0isum  46382  iundjiunlem  46414  iundjiun  46415  meadjiunlem  46420  meaiunlelem  46423  meaiuninclem  46435  meaiininc2  46443  caragensplit  46455  carageneld  46457  carageniuncllem1  46476  caratheodorylem1  46481  caratheodorylem2  46482  hoicvr  46503  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem2  46551  hoiqssbllem2  46578  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  smflimlem3  46728  smfmullem4  46749  smfsupxr  46771  smflimsuplem2  46776  smflimsuplem5  46779  natlocalincr  46829  elmod2  47294  isuspgrim0lem  47808  ssnn0ssfz  48193  zlmodzxzscm  48201  rmsupp0  48212  lincsum  48274  lincscm  48275  lindslinindimp2lem4  48306  lincresunit3  48326  elbigofrcl  48399  intubeu  48772  unilbeu  48773  postc  48884  setrec1  48921  aacllem  49031