Theorem eleqtrdi 2846

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 2838	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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleqtrrdi  2847  3eltr3g  2852  prid2g  4705  ndmfvrcl  6873  fnwelem  8081  tz7.48-1  8382  brwitnlem  8442  oeeulem  8537  dffi3  9344  cnfcom3lem  9624  ttrclse  9648  alephgeom  10004  fpwwe2lem5  10558  canthwelem  10573  hargch  10596  r1wunlim  10660  eluzel2  12793  fseq1p1m1  13552  fznn0sub2  13589  nn0split  13597  seqp1d  13980  exple1  14139  digit1  14199  bcval5  14280  bcpasc  14283  hashf1  14419  seqcoll  14426  seqcoll2  14427  ccatrn  14552  swrdccat2  14632  cats1un  14683  pfxccatin12lem3  14694  splfv2a  14718  splval2  14719  caubnd  15321  limsupgre  15443  clim2ser  15617  clim2ser2  15618  iserex  15619  isermulc2  15620  iserle  15622  iserge0  15623  climub  15624  climserle  15625  isercolllem2  15628  isercolllem3  15629  isercoll  15630  isercoll2  15631  serf0  15643  iseraltlem2  15645  iseraltlem3  15646  iseralt  15647  sumeq2ii  15655  summolem3  15676  summolem2a  15677  fsum  15682  sum0  15683  fsumcl2lem  15693  fsumadd  15702  isumclim3  15721  isumadd  15729  fsump1i  15731  fsummulc2  15746  fsumrelem  15770  iserabs  15778  cvgcmp  15779  cvgcmpub  15780  cvgcmpce  15781  binom1dif  15798  isumshft  15804  isumsplit  15805  isumrpcl  15808  isumsup2  15811  climcndslem1  15814  climcndslem2  15815  climcnds  15816  arisum2  15826  trireciplem  15827  geoser  15832  pwdif  15833  geolim  15835  geo2lim  15840  cvgrat  15848  mertenslem1  15849  mertenslem2  15850  mertens  15851  clim2prod  15853  clim2div  15854  ntrivcvgfvn0  15864  ntrivcvgtail  15865  prodeq2ii  15876  prodmolem3  15898  prodmolem2a  15899  fprod  15906  fprodntriv  15907  fprodss  15913  fprodser  15914  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodabs  15939  fprodeq0  15940  fprodn0  15944  iprodclim3  15965  iprodmul  15968  fallfacfwd  16001  0fallfac  16002  binomfallfaclem2  16005  fallfacval4  16008  bpolysum  16018  bpolydiflem  16019  fsumkthpow  16021  efcvgfsum  16051  efcj  16057  fprodefsum  16060  effsumlt  16078  ruclem7  16203  bitsfzolem  16403  bitsfzo  16404  bitsfi  16406  bitsinv1lem  16410  bitsinv1  16411  bitsinvp1  16418  sadcp1  16424  sadadd  16436  sadass  16440  bitsres  16442  smupp1  16449  smuval2  16451  smupval  16457  smueqlem  16459  smumul  16462  algrp1  16543  phiprmpw  16746  crth  16748  phimullem  16749  eulerthlem2  16752  prmdiv  16755  pcpremul  16814  pcmpt  16863  pcfac  16870  pockthlem  16876  pockthg  16877  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  prmrec  16893  1arith  16898  vdwapun  16945  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  vdw  16965  imasvscafn  17501  oppccatid  17685  oppccomfpropd  17693  brcic  17765  funcoppc  17842  invfuc  17944  hofcl  18225  yonedalem4c  18243  chnccats1  18591  gsumwsubmcl  18805  gsumsgrpccat  18808  gsumwmhm  18813  mulgnnp1  19058  mulgnnsubcl  19062  mulgnn0z  19077  mulgnndir  19079  ghmquskerlem1  19258  ghmquskerco  19259  psgnunilem4  19472  psgnran  19490  sylow1lem1  19573  lsmmod2  19651  lsmdisj2r  19660  efginvrel2  19702  efgsdmi  19707  efgsrel  19709  efgs1b  19711  efgsp1  19712  efgredleme  19718  efgredlemc  19720  efgcpbllemb  19730  frgpuplem  19747  mulgnn0di  19800  frgpnabllem1  19848  lt6abl  19870  cycsubgcyg  19876  gsumval3eu  19879  gsumval3  19882  gsumzcl2  19885  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  telgsumfz0s  19966  dprdwd  19988  dprd2da  20019  pgpfaclem1  20058  srgbinom  20212  isirred  20399  idomdomd  20703  idomcringd  20704  lspprid2  20993  lspsnat  21143  lsppratlem1  21145  lsppratlem3  21147  lidl0cl  21218  lidlacl  21219  lidlnegcl  21220  elrspsn  21238  2idllidld  21252  2idlridld  21253  rng2idl1cntr  21303  psgnghm  21560  frlmvscavalb  21750  frlmvplusgscavalb  21751  psrbaglefi  21906  psrass23l  21945  psrass23  21947  mplcoe5lem  22017  mpfind  22093  selvval  22101  mhpvscacl  22120  psr1bascl  22164  ply1basf  22166  gsummoncoe1  22273  lply1binom  22275  lply1binomsc  22276  mpfpf1  22316  pf1mpf  22317  evl1scvarpw  22328  evl1maprhm  22344  matbas2i  22387  matecld  22391  matgsum  22402  mpomatmul  22411  dmatmul  22462  1mavmul  22513  mdetleib2  22553  m1detdiag  22562  marep01ma  22625  smadiadetlem4  22634  slesolinv  22645  pmatcollpw3fi1lem1  22751  chpscmat  22807  chpscmatgsumbin  22809  chp0mat  22811  chpidmat  22812  chfacfisf  22819  chfacfisfcpmat  22820  chfacfpmmulgsum2  22830  cldrcl  22991  ordtbas  23157  iscnp2  23204  dis1stc  23464  ptbasfi  23546  ptpjopn  23577  ptclsg  23580  ptcnp  23587  kqtop  23710  reghmph  23758  ptcmplem2  24018  ptcmplem3  24019  ptcmplem4  24020  tsmslem1  24094  utop2nei  24215  isucn2  24243  cuspcvg  24265  cnextucn  24267  imasdsf1olem  24338  blcvx  24763  xrhmeo  24913  cnrehmeo  24920  evth  24926  reparphti  24964  iscau4  25246  iscmet3lem1  25258  lmle  25268  rrxfsupp  25369  rrxdsfi  25378  pjthlem2  25405  ovollb2lem  25455  ovolunlem1a  25463  ovoliunlem1  25469  ovoliun2  25473  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem4  25487  iundisj2  25516  voliunlem1  25517  volsup  25523  ioombl1lem4  25528  uniioovol  25546  uniioombllem3  25552  uniioombllem4  25553  uniioombllem6  25555  vitalilem5  25579  mbfimaopnlem  25622  mbflimsup  25633  mbfi1fseqlem3  25684  iblitg  25735  dvcnp2  25887  dvnp1  25892  cpncn  25903  dvmulbr  25906  dvcobr  25913  dvlip2  25962  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumrlimge0  25997  dvfsumrlim2  25999  ftc1cn  26010  elplyd  26167  ply1termlem  26168  ply1term  26169  ply0  26173  plyeq0lem  26175  plyaddlem1  26178  plymullem1  26179  plyaddlem  26180  plymullem  26181  coeeulem  26189  plyco  26206  coeeq2  26207  coefv0  26213  coemulhi  26219  coemulc  26220  plycj  26242  plycjOLD  26244  dvply1  26250  vieta1lem2  26277  elqaalem2  26286  dvtaylp  26335  dvntaylp  26336  taylthlem1  26338  taylth  26340  ulmres  26353  ulmshftlem  26354  ulmshft  26355  ulmcau  26360  ulmdvlem1  26365  mtest  26369  mtestbdd  26370  pserulm  26387  psercn2  26388  psercnlem1  26390  psercn  26391  pserdvlem2  26393  abelthlem6  26401  abelth  26406  efif1olem1  26506  efif1olem3  26508  efif1olem4  26509  logcn  26611  advlogexp  26619  efopn  26622  cxpeq  26721  asinsin  26856  atantayl  26901  leibpilem2  26905  birthdaylem2  26916  birthdaylem3  26917  efrlim  26933  emcllem2  26960  emcllem5  26963  emcllem7  26965  harmonicbnd4  26974  fsumharmonic  26975  lgamgulm2  26999  lgamcvglem  27003  lgamcvg2  27018  gamcvg2lem  27022  wilthlem2  27032  wilthlem3  27033  ftalem1  27036  ftalem2  27037  ftalem3  27038  ftalem5  27040  basellem2  27045  basellem3  27046  basellem5  27048  basellem8  27051  ppiprm  27114  ppinprm  27115  chtprm  27116  chtnprm  27117  chpp1  27118  vma1  27129  ppiltx  27140  musum  27154  0sgmppw  27161  1sgmprm  27162  ppiublem2  27166  chtublem  27174  fsumvma2  27177  chpchtsum  27182  logexprlim  27188  bposlem5  27251  lgscllem  27267  lgsval2lem  27270  lgsval4a  27282  lgsneg  27284  lgsdir2lem3  27290  lgsdir2lem5  27292  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  gausslemma2dlem3  27331  lgseisenlem1  27338  lgsquadlem2  27344  chebbnd1lem1  27432  chtppilimlem1  27436  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrmusum2  27457  dchrvmasum2lem  27459  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0flb  27473  dchrisum0re  27476  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  mudivsum  27493  mulogsum  27495  mulog2sumlem2  27498  selberg2lem  27513  logdivbnd  27519  pntrsumo1  27528  pntrsumbnd2  27530  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntrlog2bndlem6a  27545  pntlemj  27566  pntlemf  27568  ostth2lem3  27598  madebdayim  27880  oldbdayim  27881  newbdayim  27895  cutminmax  27928  noseqp1  28283  tglngne  28618  ltgseg  28664  eedimeq  28967  axlowdimlem16  29026  ebtwntg  29051  subgruhgredgd  29353  subumgredg2  29354  umgrres1lem  29379  wlkson  29723  wksonproplem  29771  trlsonfval  29772  pthsonfval  29808  spthson  29809  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  eupth2lems  30308  numclwwlk1lem2foa  30424  numclwlk1lem2  30440  numclwwlk2lem1  30446  htthlem  30988  hhsscms  31349  shmodsi  31460  pjoc1i  31502  5oalem1  31725  mayete3i  31799  adj1  32004  iundisj2f  32660  fmptco1f1o  32706  fcnvgreu  32745  suppovss  32754  ssnnssfz  32860  nn0diffz0  32867  iundisj2fi  32870  indpreima  32925  ccatws1f1o  33011  cshw1s2  33020  gsumhashmul  33128  gsummulsubdishift1  33129  gsumwrd2dccat  33139  fzo0pmtrlast  33153  wrdpmtrlast  33154  pmtrto1cl  33160  psgnfzto1stlem  33161  fzto1st1  33163  cycpmfv1  33174  cycpmfv2  33175  cycpmco2rn  33186  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cyc3evpm  33211  cyc3genpm  33213  cycpmconjslem2  33216  cyc3conja  33218  elrgspnlem1  33303  elrgspnlem2  33304  erler  33326  idomrcanOLD  33343  nsgmgc  33472  nsgqusf1olem2  33474  unitpidl1  33484  elrspunsn  33489  ssdifidllem  33516  mxidlirredi  33531  mxidlirred  33532  opprqusplusg  33549  opprqus0g  33550  opprqusmulr  33551  idlsrgmulrss1  33571  idlsrgmulrss2  33572  rprmcl  33578  rprmdvds  33579  rprmnz  33580  rprmnunit  33581  rprmasso  33585  rprmirredb  33592  pidufd  33603  1arithufdlem2  33605  1arithufdlem3  33606  zringfrac  33614  ply1dg3rt0irred  33644  m1pmeq  33645  ig1pmindeg  33662  extvfvvcl  33679  evlextv  33686  psrmonprod  33696  esplysply  33715  esplyind  33719  esplyfvn  33721  vietalem  33723  exsslsb  33741  ply1degltdimlem  33766  lindsun  33769  fldextfld1  33791  fldextfld2  33792  rtelextdg2  33871  cos9thpiminplylem1  33926  1smat1  33948  submateqlem2  33952  lmatfval  33958  mdetlap1  33970  madjusmdetlem1  33971  madjusmdetlem2  33972  madjusmdetlem3  33973  madjusmdetlem4  33974  zarclssn  34017  zartopn  34019  zarmxt1  34024  rhmpreimacnlem  34028  rhmpreimacn  34029  pnfneige0  34095  pl1cn  34099  rrhqima  34158  esumfzf  34213  esumpcvgval  34222  esumpmono  34223  esumcvg  34230  ldgenpisyslem1  34307  ldgenpisys  34310  measbase  34341  dya2iocnei  34426  oddpwdc  34498  eulerpartlems  34504  eulerpartlemb  34512  sseqf  34536  fibp1  34545  orrvcval4  34609  orrvcoel  34610  orrvccel  34611  ballotlem2  34633  ballotlemfrceq  34673  signsplypnf  34694  signswch  34705  signstf0  34712  signstfvn  34713  signstfvneq0  34716  signstfvcl  34717  signstfveq0  34721  signsvfn  34726  fct2relem  34741  fsum2dsub  34751  reprsuc  34759  reprpmtf1o  34770  breprexplema  34774  breprexplemc  34776  hgt749d  34793  hgt750lemb  34800  tgoldbachgnn  34803  bnj1172  35143  bnj1245  35156  bnj1311  35166  bnj1450  35192  bnj1501  35209  r1elcl  35241  subfacp1lem1  35361  subfacp1lem5  35366  subfacp1lem6  35367  subfacval2  35369  erdszelem7  35379  cvxpconn  35424  cvxsconn  35425  cvmliftlem5  35471  cvmliftlem7  35473  cvmliftlem10  35476  cvmliftlem13  35478  mrsubvrs  35704  msubrn  35711  msubco  35713  msubvrs  35742  r1peuqusdeg1  35825  imageval  36110  fwddifnp1  36347  knoppcnlem8  36760  knoppcnlem10  36762  bj-unirel  37358  icoreunrn  37675  istoprelowl  37676  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  mblfinlem2  37979  ftc1cnnc  38013  upixp  38050  sdclem2  38063  caushft  38082  ismtyres  38129  rrnmet  38150  rrndstprj1  38151  rrndstprj2  38152  rrncmslem  38153  rrnequiv  38156  iccbnd  38161  osumcllem7N  40408  pexmidlem4N  40419  lcfrlem4  41991  lcfrlem5  41992  lcfrlem6  41993  lcfrlem16  42004  lcfrlem38  42026  mapdrvallem2  42091  mapdh8ab  42223  mapdh8ad  42225  mapdh8e  42230  3factsumint3  42462  aks4d1p1p1  42502  fldhmf1  42529  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c1  42555  evl1gprodd  42556  idomnnzpownz  42571  aks6d1c5lem1  42575  aks6d1c5lem3  42576  aks6d1c5lem2  42577  deg1gprod  42579  sticksstones10  42594  aks6d1c6lem3  42611  aks5lem2  42626  aks5lem3a  42628  unitscyglem5  42638  fz1sump1  42742  sumcubes  42745  evlselv  43020  mhphf2  43031  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  mapfzcons  43148  diophren  43241  irrapxlem1  43250  monotuz  43369  acongeq  43411  jm2.26lem3  43429  jm3.1lem2  43446  pw2f1ocnv  43465  idomodle  43619  trclfvdecomr  44155  imo72b2lem0  44592  imo72b2lem1  44596  scottelrankd  44674  dvgrat  44739  cvgdvgrat  44740  hashnzfz2  44748  fcnre  45456  refsumcn  45461  rfcnnnub  45467  disjf1o  45621  disjinfi  45622  ssmapsn  45645  ssuzfz  45779  nnsplit  45788  uzssd2  45845  uzublem  45858  fsumsermpt  46009  climsuselem1  46037  limcperiod  46058  sumnnodd  46060  lptioo2cn  46073  lptioo1cn  46074  climresmpt  46087  allbutfifvre  46103  climleltrp  46104  cnrefiisplem  46257  cncfshift  46302  cncfperiod  46307  cncfshiftioo  46320  fperdvper  46347  dvnmptdivc  46366  dvnmul  46371  dvmptfprod  46373  dvnprodlem3  46376  stoweidlem11  46439  stoweidlem15  46443  stoweidlem17  46445  stoweidlem20  46448  stoweidlem34  46462  stoweidlem35  46463  stoweidlem46  46474  stoweidlem47  46475  stoweidlem56  46484  stoweidlem59  46487  stoweidlem62  46490  stirlinglem5  46506  stirlinglem14  46515  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  fourierdlem11  46546  fourierdlem15  46550  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem25  46560  fourierdlem48  46582  fourierdlem52  46586  fourierdlem54  46588  fourierdlem58  46592  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem69  46603  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem80  46614  fourierdlem81  46615  fourierdlem83  46617  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem113  46647  fouriercnp  46654  fouriersw  46659  elaa2lem  46661  etransclem4  46666  etransclem7  46669  etransclem10  46672  etransclem14  46676  etransclem15  46677  etransclem24  46686  etransclem25  46687  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem44  46706  etransclem46  46708  qndenserrnopnlem  46725  qndenserrn  46727  prsal  46746  salgencntex  46771  subsaliuncl  46786  subsalsal  46787  sge0tsms  46808  sge0fodjrnlem  46844  sge0isum  46855  iundjiunlem  46887  iundjiun  46888  meadjiunlem  46893  meaiunlelem  46896  meaiuninclem  46908  meaiininc2  46916  caragensplit  46928  carageneld  46930  carageniuncllem1  46949  caratheodorylem1  46954  caratheodorylem2  46955  hoicvr  46976  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmvlelem2  47024  hoiqssbllem2  47051  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  smflimlem3  47201  smfmullem4  47222  smfsupxr  47244  smflimsuplem2  47249  smflimsuplem5  47252  ormklocald  47304  natlocalincr  47306  elmod2  47809  isuspgrim0lem  48369  upgrimtrlslem2  48381  ssnn0ssfz  48825  zlmodzxzscm  48833  rmsupp0  48844  lincsum  48905  lincscm  48906  lindslinindimp2lem4  48937  lincresunit3  48957  elbigofrcl  49026  intubeu  49459  unilbeu  49460  cicrcl2  49518  cic1st2nd  49522  imaf1homlem  49582  oppfrcl  49603  eloppf  49608  imasubc  49626  imaid  49629  oppcuprcl5  49676  oppcup3  49684  uptrlem2  49686  uptrlem3  49687  natoppf  49704  elxpcbasex1ALT  49724  elxpcbasex2ALT  49726  swapf1a  49744  swapf2f1oa  49752  swapfida  49755  cofuswapf1  49769  cofuswapf2  49770  fucoppcco  49884  postc  50044  reldmlan2  50092  reldmran2  50093  lanrcl  50096  ranrcl  50097  setrec1  50166  aacllem  50276