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  4706  ndmfvrcl  6869  fnwelem  8076  tz7.48-1  8377  brwitnlem  8437  oeeulem  8532  dffi3  9339  cnfcom3lem  9619  ttrclse  9643  alephgeom  9999  fpwwe2lem5  10553  canthwelem  10568  hargch  10591  r1wunlim  10655  eluzel2  12788  fseq1p1m1  13547  fznn0sub2  13584  nn0split  13592  seqp1d  13975  exple1  14134  digit1  14194  bcval5  14275  bcpasc  14278  hashf1  14414  seqcoll  14421  seqcoll2  14422  ccatrn  14547  swrdccat2  14627  cats1un  14678  pfxccatin12lem3  14689  splfv2a  14713  splval2  14714  caubnd  15316  limsupgre  15438  clim2ser  15612  clim2ser2  15613  iserex  15614  isermulc2  15615  iserle  15617  iserge0  15618  climub  15619  climserle  15620  isercolllem2  15623  isercolllem3  15624  isercoll  15625  isercoll2  15626  serf0  15638  iseraltlem2  15640  iseraltlem3  15641  iseralt  15642  sumeq2ii  15650  summolem3  15671  summolem2a  15672  fsum  15677  sum0  15678  fsumcl2lem  15688  fsumadd  15697  isumclim3  15716  isumadd  15724  fsump1i  15726  fsummulc2  15741  fsumrelem  15765  iserabs  15773  cvgcmp  15774  cvgcmpub  15775  cvgcmpce  15776  binom1dif  15793  isumshft  15799  isumsplit  15800  isumrpcl  15803  isumsup2  15806  climcndslem1  15809  climcndslem2  15810  climcnds  15811  arisum2  15821  trireciplem  15822  geoser  15827  pwdif  15828  geolim  15830  geo2lim  15835  cvgrat  15843  mertenslem1  15844  mertenslem2  15845  mertens  15846  clim2prod  15848  clim2div  15849  ntrivcvgfvn0  15859  ntrivcvgtail  15860  prodeq2ii  15871  prodmolem3  15893  prodmolem2a  15894  fprod  15901  fprodntriv  15902  fprodss  15908  fprodser  15909  fprodcl2lem  15910  fprodmul  15920  fproddiv  15921  fprodabs  15934  fprodeq0  15935  fprodn0  15939  iprodclim3  15960  iprodmul  15963  fallfacfwd  15996  0fallfac  15997  binomfallfaclem2  16000  fallfacval4  16003  bpolysum  16013  bpolydiflem  16014  fsumkthpow  16016  efcvgfsum  16046  efcj  16052  fprodefsum  16055  effsumlt  16073  ruclem7  16198  bitsfzolem  16398  bitsfzo  16399  bitsfi  16401  bitsinv1lem  16405  bitsinv1  16406  bitsinvp1  16413  sadcp1  16419  sadadd  16431  sadass  16435  bitsres  16437  smupp1  16444  smuval2  16446  smupval  16452  smueqlem  16454  smumul  16457  algrp1  16538  phiprmpw  16741  crth  16743  phimullem  16744  eulerthlem2  16747  prmdiv  16750  pcpremul  16809  pcmpt  16858  pcfac  16865  pockthlem  16871  pockthg  16872  prmreclem2  16883  prmreclem3  16884  prmreclem4  16885  prmreclem5  16886  prmreclem6  16887  prmrec  16888  1arith  16893  vdwapun  16940  vdwlem1  16947  vdwlem2  16948  vdwlem3  16949  vdwlem6  16952  vdwlem8  16954  vdwlem10  16956  vdw  16960  imasvscafn  17496  oppccatid  17680  oppccomfpropd  17688  brcic  17760  funcoppc  17837  invfuc  17939  hofcl  18220  yonedalem4c  18238  chnccats1  18586  gsumwsubmcl  18800  gsumsgrpccat  18803  gsumwmhm  18808  mulgnnp1  19053  mulgnnsubcl  19057  mulgnn0z  19072  mulgnndir  19074  ghmquskerlem1  19253  ghmquskerco  19254  psgnunilem4  19467  psgnran  19485  sylow1lem1  19568  lsmmod2  19646  lsmdisj2r  19655  efginvrel2  19697  efgsdmi  19702  efgsrel  19704  efgs1b  19706  efgsp1  19707  efgredleme  19713  efgredlemc  19715  efgcpbllemb  19725  frgpuplem  19742  mulgnn0di  19795  frgpnabllem1  19843  lt6abl  19865  cycsubgcyg  19871  gsumval3eu  19874  gsumval3  19877  gsumzcl2  19880  gsumzaddlem  19891  gsumconst  19904  gsumzmhm  19907  gsumzoppg  19914  telgsumfz0s  19961  dprdwd  19983  dprd2da  20014  pgpfaclem1  20053  srgbinom  20207  isirred  20394  idomdomd  20698  idomcringd  20699  lspprid2  20988  lspsnat  21139  lsppratlem1  21141  lsppratlem3  21143  lidl0cl  21214  lidlacl  21215  lidlnegcl  21216  elrspsn  21234  2idllidld  21248  2idlridld  21249  rng2idl1cntr  21299  psgnghm  21574  frlmvscavalb  21764  frlmvplusgscavalb  21765  psrbaglefi  21920  psrass23l  21959  psrass23  21961  mplcoe5lem  22031  mpfind  22107  selvval  22115  mhpvscacl  22134  psr1bascl  22178  ply1basf  22180  gsummoncoe1  22287  lply1binom  22289  lply1binomsc  22290  mpfpf1  22330  pf1mpf  22331  evl1scvarpw  22342  evl1maprhm  22358  matbas2i  22401  matecld  22405  matgsum  22416  mpomatmul  22425  dmatmul  22476  1mavmul  22527  mdetleib2  22567  m1detdiag  22576  marep01ma  22639  smadiadetlem4  22648  slesolinv  22659  pmatcollpw3fi1lem1  22765  chpscmat  22821  chpscmatgsumbin  22823  chp0mat  22825  chpidmat  22826  chfacfisf  22833  chfacfisfcpmat  22834  chfacfpmmulgsum2  22844  cldrcl  23005  ordtbas  23171  iscnp2  23218  dis1stc  23478  ptbasfi  23560  ptpjopn  23591  ptclsg  23594  ptcnp  23601  kqtop  23724  reghmph  23772  ptcmplem2  24032  ptcmplem3  24033  ptcmplem4  24034  tsmslem1  24108  utop2nei  24229  isucn2  24257  cuspcvg  24279  cnextucn  24281  imasdsf1olem  24352  blcvx  24777  xrhmeo  24927  cnrehmeo  24934  evth  24940  reparphti  24978  iscau4  25260  iscmet3lem1  25272  lmle  25282  rrxfsupp  25383  rrxdsfi  25392  pjthlem2  25419  ovollb2lem  25469  ovolunlem1a  25477  ovoliunlem1  25483  ovoliun2  25487  ovolscalem1  25494  ovolicc1  25497  ovolicc2lem4  25501  iundisj2  25530  voliunlem1  25531  volsup  25537  ioombl1lem4  25542  uniioovol  25560  uniioombllem3  25566  uniioombllem4  25567  uniioombllem6  25569  vitalilem5  25593  mbfimaopnlem  25636  mbflimsup  25647  mbfi1fseqlem3  25698  iblitg  25749  dvcnp2  25901  dvnp1  25906  cpncn  25917  dvmulbr  25920  dvcobr  25927  dvlip2  25976  dvfsumlem2  26008  dvfsumlem3  26009  dvfsumrlimge0  26011  dvfsumrlim2  26013  ftc1cn  26024  elplyd  26181  ply1termlem  26182  ply1term  26183  ply0  26187  plyeq0lem  26189  plyaddlem1  26192  plymullem1  26193  plyaddlem  26194  plymullem  26195  coeeulem  26203  plyco  26220  coeeq2  26221  coefv0  26227  coemulhi  26233  coemulc  26234  plycj  26256  plycjOLD  26258  dvply1  26264  vieta1lem2  26292  elqaalem2  26301  dvtaylp  26351  dvntaylp  26352  taylthlem1  26354  taylth  26357  ulmres  26370  ulmshftlem  26371  ulmshft  26372  ulmcau  26377  ulmdvlem1  26382  mtest  26386  mtestbdd  26387  pserulm  26404  psercn2  26405  psercnlem1  26407  psercn  26408  pserdvlem2  26410  abelthlem6  26418  abelth  26423  efif1olem1  26523  efif1olem3  26525  efif1olem4  26526  logcn  26628  advlogexp  26636  efopn  26639  cxpeq  26738  asinsin  26873  atantayl  26918  leibpilem2  26922  birthdaylem2  26933  birthdaylem3  26934  efrlim  26950  efrlimOLD  26951  emcllem2  26978  emcllem5  26981  emcllem7  26983  harmonicbnd4  26992  fsumharmonic  26993  lgamgulm2  27017  lgamcvglem  27021  lgamcvg2  27036  gamcvg2lem  27040  wilthlem2  27050  wilthlem3  27051  ftalem1  27054  ftalem2  27055  ftalem3  27056  ftalem5  27058  basellem2  27063  basellem3  27064  basellem5  27066  basellem8  27069  ppiprm  27132  ppinprm  27133  chtprm  27134  chtnprm  27135  chpp1  27136  vma1  27147  ppiltx  27158  musum  27172  0sgmppw  27179  1sgmprm  27180  ppiublem2  27184  chtublem  27192  fsumvma2  27195  chpchtsum  27200  logexprlim  27206  bposlem5  27269  lgscllem  27285  lgsval2lem  27288  lgsval4a  27300  lgsneg  27302  lgsdir2lem3  27308  lgsdir2lem5  27310  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  gausslemma2dlem3  27349  lgseisenlem1  27356  lgsquadlem2  27362  chebbnd1lem1  27450  chtppilimlem1  27454  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasum2lem  27477  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0flb  27491  dchrisum0re  27494  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  mudivsum  27511  mulogsum  27513  mulog2sumlem2  27516  selberg2lem  27531  logdivbnd  27537  pntrsumo1  27546  pntrsumbnd2  27548  pntrlog2bndlem2  27559  pntrlog2bndlem4  27561  pntrlog2bndlem6a  27563  pntlemj  27584  pntlemf  27586  ostth2lem3  27616  madebdayim  27898  oldbdayim  27899  newbdayim  27913  cutminmax  27946  noseqp1  28301  tglngne  28636  ltgseg  28682  eedimeq  28985  axlowdimlem16  29044  ebtwntg  29069  subgruhgredgd  29371  subumgredg2  29372  umgrres1lem  29397  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  32679  fmptco1f1o  32725  fcnvgreu  32764  suppovss  32773  ssnnssfz  32879  nn0diffz0  32886  iundisj2fi  32889  indpreima  32944  ccatws1f1o  33030  cshw1s2  33039  gsumhashmul  33147  gsummulsubdishift1  33148  gsumwrd2dccat  33158  fzo0pmtrlast  33172  wrdpmtrlast  33173  pmtrto1cl  33179  psgnfzto1stlem  33180  fzto1st1  33182  cycpmfv1  33193  cycpmfv2  33194  cycpmco2rn  33205  cycpmco2lem4  33209  cycpmco2lem5  33210  cycpmco2lem6  33211  cyc3evpm  33230  cyc3genpm  33232  cycpmconjslem2  33235  cyc3conja  33237  elrgspnlem1  33322  elrgspnlem2  33323  erler  33345  idomrcanOLD  33362  nsgmgc  33491  nsgqusf1olem2  33493  unitpidl1  33503  elrspunsn  33508  ssdifidllem  33535  mxidlirredi  33550  mxidlirred  33551  opprqusplusg  33568  opprqus0g  33569  opprqusmulr  33570  idlsrgmulrss1  33590  idlsrgmulrss2  33591  rprmcl  33597  rprmdvds  33598  rprmnz  33599  rprmnunit  33600  rprmasso  33604  rprmirredb  33611  pidufd  33622  1arithufdlem2  33624  1arithufdlem3  33625  zringfrac  33633  ply1dg3rt0irred  33663  m1pmeq  33664  ig1pmindeg  33681  extvfvvcl  33698  evlextv  33705  psrmonprod  33715  esplysply  33734  esplyind  33738  esplyfvn  33740  vietalem  33742  exsslsb  33760  ply1degltdimlem  33786  lindsun  33789  fldextfld1  33811  fldextfld2  33812  rtelextdg2  33891  cos9thpiminplylem1  33946  1smat1  33968  submateqlem2  33972  lmatfval  33978  mdetlap1  33990  madjusmdetlem1  33991  madjusmdetlem2  33992  madjusmdetlem3  33993  madjusmdetlem4  33994  zarclssn  34037  zartopn  34039  zarmxt1  34044  rhmpreimacnlem  34048  rhmpreimacn  34049  pnfneige0  34115  pl1cn  34119  rrhqima  34178  esumfzf  34233  esumpcvgval  34242  esumpmono  34243  esumcvg  34250  ldgenpisyslem1  34327  ldgenpisys  34330  measbase  34361  dya2iocnei  34446  oddpwdc  34518  eulerpartlems  34524  eulerpartlemb  34532  sseqf  34556  fibp1  34565  orrvcval4  34629  orrvcoel  34630  orrvccel  34631  ballotlem2  34653  ballotlemfrceq  34693  signsplypnf  34714  signswch  34725  signstf0  34732  signstfvn  34733  signstfvneq0  34736  signstfvcl  34737  signstfveq0  34741  signsvfn  34746  fct2relem  34761  fsum2dsub  34771  reprsuc  34779  reprpmtf1o  34790  breprexplema  34794  breprexplemc  34796  hgt749d  34813  hgt750lemb  34820  tgoldbachgnn  34823  bnj1172  35163  bnj1245  35176  bnj1311  35186  bnj1450  35212  bnj1501  35229  r1elcl  35261  subfacp1lem1  35381  subfacp1lem5  35386  subfacp1lem6  35387  subfacval2  35389  erdszelem7  35399  cvxpconn  35444  cvxsconn  35445  cvmliftlem5  35491  cvmliftlem7  35493  cvmliftlem10  35496  cvmliftlem13  35498  mrsubvrs  35724  msubrn  35731  msubco  35733  msubvrs  35762  r1peuqusdeg1  35845  imageval  36130  fwddifnp1  36367  knoppcnlem8  36780  knoppcnlem10  36782  bj-unirel  37378  icoreunrn  37693  istoprelowl  37694  poimirlem3  37962  poimirlem4  37963  poimirlem6  37965  poimirlem7  37966  poimirlem8  37967  poimirlem12  37971  poimirlem15  37974  poimirlem16  37975  poimirlem17  37976  poimirlem18  37977  poimirlem19  37978  poimirlem20  37979  poimirlem21  37980  poimirlem22  37981  poimirlem23  37982  poimirlem24  37983  poimirlem25  37984  poimirlem26  37985  poimirlem27  37986  poimirlem28  37987  poimirlem29  37988  poimirlem31  37990  mblfinlem2  37997  ftc1cnnc  38031  upixp  38068  sdclem2  38081  caushft  38100  ismtyres  38147  rrnmet  38168  rrndstprj1  38169  rrndstprj2  38170  rrncmslem  38171  rrnequiv  38174  iccbnd  38179  osumcllem7N  40426  pexmidlem4N  40437  lcfrlem4  42009  lcfrlem5  42010  lcfrlem6  42011  lcfrlem16  42022  lcfrlem38  42044  mapdrvallem2  42109  mapdh8ab  42241  mapdh8ad  42243  mapdh8e  42248  3factsumint3  42480  aks4d1p1p1  42520  fldhmf1  42547  aks6d1c1p2  42566  aks6d1c1p3  42567  aks6d1c1p7  42570  aks6d1c1p6  42571  aks6d1c1p8  42572  aks6d1c1  42573  evl1gprodd  42574  idomnnzpownz  42589  aks6d1c5lem1  42593  aks6d1c5lem3  42594  aks6d1c5lem2  42595  deg1gprod  42597  sticksstones10  42612  aks6d1c6lem3  42629  aks5lem2  42644  aks5lem3a  42646  unitscyglem5  42656  fz1sump1  42760  sumcubes  42763  evlselv  43038  mhphf2  43049  prjspnfv01  43075  prjspner01  43076  prjspner1  43077  mapfzcons  43166  diophren  43263  irrapxlem1  43272  monotuz  43391  acongeq  43433  jm2.26lem3  43451  jm3.1lem2  43468  pw2f1ocnv  43487  idomodle  43641  trclfvdecomr  44177  imo72b2lem0  44614  imo72b2lem1  44618  scottelrankd  44696  dvgrat  44761  cvgdvgrat  44762  hashnzfz2  44770  fcnre  45478  refsumcn  45483  rfcnnnub  45489  disjf1o  45643  disjinfi  45644  ssmapsn  45667  ssuzfz  45801  nnsplit  45810  uzssd2  45867  uzublem  45880  fsumsermpt  46031  climsuselem1  46059  limcperiod  46080  sumnnodd  46082  lptioo2cn  46095  lptioo1cn  46096  climresmpt  46109  allbutfifvre  46125  climleltrp  46126  cnrefiisplem  46279  cncfshift  46324  cncfperiod  46329  cncfshiftioo  46342  fperdvper  46369  dvnmptdivc  46388  dvnmul  46393  dvmptfprod  46395  dvnprodlem3  46398  stoweidlem11  46461  stoweidlem15  46465  stoweidlem17  46467  stoweidlem20  46470  stoweidlem34  46484  stoweidlem35  46485  stoweidlem46  46496  stoweidlem47  46497  stoweidlem56  46506  stoweidlem59  46509  stoweidlem62  46512  stirlinglem5  46528  stirlinglem14  46537  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  fourierdlem11  46568  fourierdlem15  46572  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem25  46582  fourierdlem48  46604  fourierdlem52  46608  fourierdlem54  46610  fourierdlem58  46614  fourierdlem62  46618  fourierdlem64  46620  fourierdlem65  46621  fourierdlem69  46625  fourierdlem70  46626  fourierdlem71  46627  fourierdlem73  46629  fourierdlem80  46636  fourierdlem81  46637  fourierdlem83  46639  fourierdlem92  46648  fourierdlem93  46649  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  fouriercnp  46676  fouriersw  46681  elaa2lem  46683  etransclem4  46688  etransclem7  46691  etransclem10  46694  etransclem14  46698  etransclem15  46699  etransclem24  46708  etransclem25  46709  etransclem31  46715  etransclem32  46716  etransclem35  46719  etransclem44  46728  etransclem46  46730  qndenserrnopnlem  46747  qndenserrn  46749  prsal  46768  salgencntex  46793  subsaliuncl  46808  subsalsal  46809  sge0tsms  46830  sge0fodjrnlem  46866  sge0isum  46877  iundjiunlem  46909  iundjiun  46910  meadjiunlem  46915  meaiunlelem  46918  meaiuninclem  46930  meaiininc2  46938  caragensplit  46950  carageneld  46952  carageniuncllem1  46971  caratheodorylem1  46976  caratheodorylem2  46977  hoicvr  46998  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmvlelem2  47046  hoiqssbllem2  47073  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  smflimlem3  47223  smfmullem4  47244  smfsupxr  47266  smflimsuplem2  47271  smflimsuplem5  47274  ormklocald  47324  natlocalincr  47326  elmod2  47825  isuspgrim0lem  48385  upgrimtrlslem2  48397  ssnn0ssfz  48841  zlmodzxzscm  48849  rmsupp0  48860  lincsum  48921  lincscm  48922  lindslinindimp2lem4  48953  lincresunit3  48973  elbigofrcl  49042  intubeu  49475  unilbeu  49476  cicrcl2  49534  cic1st2nd  49538  imaf1homlem  49598  oppfrcl  49619  eloppf  49624  imasubc  49642  imaid  49645  oppcuprcl5  49692  oppcup3  49700  uptrlem2  49702  uptrlem3  49703  natoppf  49720  elxpcbasex1ALT  49740  elxpcbasex2ALT  49742  swapf1a  49760  swapf2f1oa  49768  swapfida  49771  cofuswapf1  49785  cofuswapf2  49786  fucoppcco  49900  postc  50060  reldmlan2  50108  reldmran2  50109  lanrcl  50112  ranrcl  50113  setrec1  50182  aacllem  50292