Theorem eleqtrdi 2844

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  eleqtrrdi  2845  3eltr3g  2850  prid2g  4716  ndmfvrcl  6865  fnwelem  8071  tz7.48-1  8372  brwitnlem  8432  oeeulem  8527  dffi3  9332  cnfcom3lem  9610  ttrclse  9634  alephgeom  9990  fpwwe2lem5  10544  canthwelem  10559  hargch  10582  r1wunlim  10646  eluzel2  12754  fseq1p1m1  13512  fznn0sub2  13549  nn0split  13557  seqp1d  13939  exple1  14098  digit1  14158  bcval5  14239  bcpasc  14242  hashf1  14378  seqcoll  14385  seqcoll2  14386  ccatrn  14511  swrdccat2  14591  cats1un  14642  pfxccatin12lem3  14653  splfv2a  14677  splval2  14678  caubnd  15280  limsupgre  15402  clim2ser  15576  clim2ser2  15577  iserex  15578  isermulc2  15579  iserle  15581  iserge0  15582  climub  15583  climserle  15584  isercolllem2  15587  isercolllem3  15588  isercoll  15589  isercoll2  15590  serf0  15602  iseraltlem2  15604  iseraltlem3  15605  iseralt  15606  sumeq2ii  15614  summolem3  15635  summolem2a  15636  fsum  15641  sum0  15642  fsumcl2lem  15652  fsumadd  15661  isumclim3  15680  isumadd  15688  fsump1i  15690  fsummulc2  15705  fsumrelem  15728  iserabs  15736  cvgcmp  15737  cvgcmpub  15738  cvgcmpce  15739  binom1dif  15754  isumshft  15760  isumsplit  15761  isumrpcl  15764  isumsup2  15767  climcndslem1  15770  climcndslem2  15771  climcnds  15772  arisum2  15782  trireciplem  15783  geoser  15788  pwdif  15789  geolim  15791  geo2lim  15796  cvgrat  15804  mertenslem1  15805  mertenslem2  15806  mertens  15807  clim2prod  15809  clim2div  15810  ntrivcvgfvn0  15820  ntrivcvgtail  15821  prodeq2ii  15832  prodmolem3  15854  prodmolem2a  15855  fprod  15862  fprodntriv  15863  fprodss  15869  fprodser  15870  fprodcl2lem  15871  fprodmul  15881  fproddiv  15882  fprodabs  15895  fprodeq0  15896  fprodn0  15900  iprodclim3  15921  iprodmul  15924  fallfacfwd  15957  0fallfac  15958  binomfallfaclem2  15961  fallfacval4  15964  bpolysum  15974  bpolydiflem  15975  fsumkthpow  15977  efcvgfsum  16007  efcj  16013  fprodefsum  16016  effsumlt  16034  ruclem7  16159  bitsfzolem  16359  bitsfzo  16360  bitsfi  16362  bitsinv1lem  16366  bitsinv1  16367  bitsinvp1  16374  sadcp1  16380  sadadd  16392  sadass  16396  bitsres  16398  smupp1  16405  smuval2  16407  smupval  16413  smueqlem  16415  smumul  16418  algrp1  16499  phiprmpw  16701  crth  16703  phimullem  16704  eulerthlem2  16707  prmdiv  16710  pcpremul  16769  pcmpt  16818  pcfac  16825  pockthlem  16831  pockthg  16832  prmreclem2  16843  prmreclem3  16844  prmreclem4  16845  prmreclem5  16846  prmreclem6  16847  prmrec  16848  1arith  16853  vdwapun  16900  vdwlem1  16907  vdwlem2  16908  vdwlem3  16909  vdwlem6  16912  vdwlem8  16914  vdwlem10  16916  vdw  16920  imasvscafn  17456  oppccatid  17640  oppccomfpropd  17648  brcic  17720  funcoppc  17797  invfuc  17899  hofcl  18180  yonedalem4c  18198  chnccats1  18546  gsumwsubmcl  18760  gsumsgrpccat  18763  gsumwmhm  18768  mulgnnp1  19010  mulgnnsubcl  19014  mulgnn0z  19029  mulgnndir  19031  ghmquskerlem1  19210  ghmquskerco  19211  psgnunilem4  19424  psgnran  19442  sylow1lem1  19525  lsmmod2  19603  lsmdisj2r  19612  efginvrel2  19654  efgsdmi  19659  efgsrel  19661  efgs1b  19663  efgsp1  19664  efgredleme  19670  efgredlemc  19672  efgcpbllemb  19682  frgpuplem  19699  mulgnn0di  19752  frgpnabllem1  19800  lt6abl  19822  cycsubgcyg  19828  gsumval3eu  19831  gsumval3  19834  gsumzcl2  19837  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  gsumzoppg  19871  telgsumfz0s  19918  dprdwd  19940  dprd2da  19971  pgpfaclem1  20010  srgbinom  20164  isirred  20353  idomdomd  20657  idomcringd  20658  lspprid2  20947  lspsnat  21098  lsppratlem1  21100  lsppratlem3  21102  lidl0cl  21173  lidlacl  21174  lidlnegcl  21175  elrspsn  21193  2idllidld  21207  2idlridld  21208  rng2idl1cntr  21258  psgnghm  21533  frlmvscavalb  21723  frlmvplusgscavalb  21724  psrbaglefi  21880  psrass23l  21920  psrass23  21922  mplcoe5lem  21992  mpfind  22068  selvval  22076  mhpvscacl  22095  psr1bascl  22139  ply1basf  22141  gsummoncoe1  22250  lply1binom  22252  lply1binomsc  22253  mpfpf1  22293  pf1mpf  22294  evl1scvarpw  22305  evl1maprhm  22321  matbas2i  22364  matecld  22368  matgsum  22379  mpomatmul  22388  dmatmul  22439  1mavmul  22490  mdetleib2  22530  m1detdiag  22539  marep01ma  22602  smadiadetlem4  22611  slesolinv  22622  pmatcollpw3fi1lem1  22728  chpscmat  22784  chpscmatgsumbin  22786  chp0mat  22788  chpidmat  22789  chfacfisf  22796  chfacfisfcpmat  22797  chfacfpmmulgsum2  22807  cldrcl  22968  ordtbas  23134  iscnp2  23181  dis1stc  23441  ptbasfi  23523  ptpjopn  23554  ptclsg  23557  ptcnp  23564  kqtop  23687  reghmph  23735  ptcmplem2  23995  ptcmplem3  23996  ptcmplem4  23997  tsmslem1  24071  utop2nei  24192  isucn2  24220  cuspcvg  24242  cnextucn  24244  imasdsf1olem  24315  blcvx  24740  xrhmeo  24898  cnrehmeo  24905  cnrehmeoOLD  24906  evth  24912  reparphti  24950  reparphtiOLD  24951  iscau4  25233  iscmet3lem1  25245  lmle  25255  rrxfsupp  25356  rrxdsfi  25365  pjthlem2  25392  ovollb2lem  25443  ovolunlem1a  25451  ovoliunlem1  25457  ovoliun2  25461  ovolscalem1  25468  ovolicc1  25471  ovolicc2lem4  25475  iundisj2  25504  voliunlem1  25505  volsup  25511  ioombl1lem4  25516  uniioovol  25534  uniioombllem3  25540  uniioombllem4  25541  uniioombllem6  25543  vitalilem5  25567  mbfimaopnlem  25610  mbflimsup  25621  mbfi1fseqlem3  25672  iblitg  25723  dvcnp2  25875  dvnp1  25881  cpncn  25892  dvmulbr  25895  dvcobr  25903  dvlip2  25954  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumrlimge0  25991  dvfsumrlim2  25993  ftc1cn  26004  elplyd  26161  ply1termlem  26162  ply1term  26163  ply0  26167  plyeq0lem  26169  plyaddlem1  26172  plymullem1  26173  plyaddlem  26174  plymullem  26175  coeeulem  26183  plyco  26200  coeeq2  26201  coefv0  26207  coemulhi  26213  coemulc  26214  plycj  26237  plycjOLD  26239  dvply1  26245  vieta1lem2  26273  elqaalem2  26282  dvtaylp  26332  dvntaylp  26333  taylthlem1  26335  taylth  26338  ulmres  26351  ulmshftlem  26352  ulmshft  26353  ulmcau  26358  ulmdvlem1  26363  mtest  26367  mtestbdd  26368  pserulm  26385  psercn2  26386  psercn2OLD  26387  psercnlem1  26389  psercn  26390  pserdvlem2  26392  abelthlem6  26400  abelth  26405  efif1olem1  26505  efif1olem3  26507  efif1olem4  26508  logcn  26610  advlogexp  26618  efopn  26621  cxpeq  26721  asinsin  26856  atantayl  26901  leibpilem2  26905  birthdaylem2  26916  birthdaylem3  26917  efrlim  26933  efrlimOLD  26934  emcllem2  26961  emcllem5  26964  emcllem7  26966  harmonicbnd4  26975  fsumharmonic  26976  lgamgulm2  27000  lgamcvglem  27004  lgamcvg2  27019  gamcvg2lem  27023  wilthlem2  27033  wilthlem3  27034  ftalem1  27037  ftalem2  27038  ftalem3  27039  ftalem5  27041  basellem2  27046  basellem3  27047  basellem5  27049  basellem8  27052  ppiprm  27115  ppinprm  27116  chtprm  27117  chtnprm  27118  chpp1  27119  vma1  27130  ppiltx  27141  musum  27155  0sgmppw  27163  1sgmprm  27164  ppiublem2  27168  chtublem  27176  fsumvma2  27179  chpchtsum  27184  logexprlim  27190  bposlem5  27253  lgscllem  27269  lgsval2lem  27272  lgsval4a  27284  lgsneg  27286  lgsdir2lem3  27292  lgsdir2lem5  27294  lgsdir  27297  lgsdilem2  27298  lgsdi  27299  lgsne0  27300  gausslemma2dlem3  27333  lgseisenlem1  27340  lgsquadlem2  27346  chebbnd1lem1  27434  chtppilimlem1  27438  rplogsumlem2  27450  rpvmasumlem  27452  dchrisumlem1  27454  dchrisumlem2  27455  dchrmusum2  27459  dchrvmasum2lem  27461  dchrvmasumiflem1  27466  dchrisum0flblem1  27473  dchrisum0flblem2  27474  dchrisum0flb  27475  dchrisum0re  27478  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0lem2  27483  dchrisum0lem3  27484  mudivsum  27495  mulogsum  27497  mulog2sumlem2  27500  selberg2lem  27515  logdivbnd  27521  pntrsumo1  27530  pntrsumbnd2  27532  pntrlog2bndlem2  27543  pntrlog2bndlem4  27545  pntrlog2bndlem6a  27547  pntlemj  27568  pntlemf  27570  ostth2lem3  27600  madebdayim  27860  oldbdayim  27861  newbdayim  27875  noseqp1  28252  tglngne  28571  ltgseg  28617  eedimeq  28920  axlowdimlem16  28979  ebtwntg  29004  subgruhgredgd  29306  subumgredg2  29307  umgrres1lem  29332  wlkson  29677  wksonproplem  29725  trlsonfval  29726  pthsonfval  29762  spthson  29763  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  eupth2lems  30262  numclwwlk1lem2foa  30378  numclwlk1lem2  30394  numclwwlk2lem1  30400  htthlem  30941  hhsscms  31302  shmodsi  31413  pjoc1i  31455  5oalem1  31678  mayete3i  31752  adj1  31957  iundisj2f  32614  fmptco1f1o  32660  fcnvgreu  32700  suppovss  32709  ssnnssfz  32816  nn0diffz0  32823  iundisj2fi  32826  indpreima  32896  ccatws1f1o  32982  cshw1s2  32991  gsumhashmul  33099  gsummulsubdishift1  33100  gsumwrd2dccat  33109  fzo0pmtrlast  33123  wrdpmtrlast  33124  pmtrto1cl  33130  psgnfzto1stlem  33131  fzto1st1  33133  cycpmfv1  33144  cycpmfv2  33145  cycpmco2rn  33156  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cyc3evpm  33181  cyc3genpm  33183  cycpmconjslem2  33186  cyc3conja  33188  elrgspnlem1  33273  elrgspnlem2  33274  erler  33296  idomrcanOLD  33313  nsgmgc  33442  nsgqusf1olem2  33444  unitpidl1  33454  elrspunsn  33459  ssdifidllem  33486  mxidlirredi  33501  mxidlirred  33502  opprqusplusg  33519  opprqus0g  33520  opprqusmulr  33521  idlsrgmulrss1  33541  idlsrgmulrss2  33542  rprmcl  33548  rprmdvds  33549  rprmnz  33550  rprmnunit  33551  rprmasso  33555  rprmirredb  33562  pidufd  33573  1arithufdlem2  33575  1arithufdlem3  33576  zringfrac  33584  ply1dg3rt0irred  33614  m1pmeq  33615  ig1pmindeg  33632  extvfvvcl  33649  evlextv  33656  esplysply  33678  esplyind  33680  esplyfvn  33682  vietalem  33684  exsslsb  33702  ply1degltdimlem  33728  lindsun  33731  fldextfld1  33753  fldextfld2  33754  rtelextdg2  33833  cos9thpiminplylem1  33888  1smat1  33910  submateqlem2  33914  lmatfval  33920  mdetlap1  33932  madjusmdetlem1  33933  madjusmdetlem2  33934  madjusmdetlem3  33935  madjusmdetlem4  33936  zarclssn  33979  zartopn  33981  zarmxt1  33986  rhmpreimacnlem  33990  rhmpreimacn  33991  pnfneige0  34057  pl1cn  34061  rrhqima  34120  esumfzf  34175  esumpcvgval  34184  esumpmono  34185  esumcvg  34192  ldgenpisyslem1  34269  ldgenpisys  34272  measbase  34303  dya2iocnei  34388  oddpwdc  34460  eulerpartlems  34466  eulerpartlemb  34474  sseqf  34498  fibp1  34507  orrvcval4  34571  orrvcoel  34572  orrvccel  34573  ballotlem2  34595  ballotlemfrceq  34635  signsplypnf  34656  signswch  34667  signstf0  34674  signstfvn  34675  signstfvneq0  34678  signstfvcl  34679  signstfveq0  34683  signsvfn  34688  fct2relem  34703  fsum2dsub  34713  reprsuc  34721  reprpmtf1o  34732  breprexplema  34736  breprexplemc  34738  hgt749d  34755  hgt750lemb  34762  tgoldbachgnn  34765  bnj1172  35106  bnj1245  35119  bnj1311  35129  bnj1450  35155  bnj1501  35172  r1elcl  35203  subfacp1lem1  35322  subfacp1lem5  35327  subfacp1lem6  35328  subfacval2  35330  erdszelem7  35340  cvxpconn  35385  cvxsconn  35386  cvmliftlem5  35432  cvmliftlem7  35434  cvmliftlem10  35437  cvmliftlem13  35439  mrsubvrs  35665  msubrn  35672  msubco  35674  msubvrs  35703  r1peuqusdeg1  35786  imageval  36071  fwddifnp1  36308  knoppcnlem8  36643  knoppcnlem10  36645  bj-unirel  37195  icoreunrn  37503  istoprelowl  37504  poimirlem3  37763  poimirlem4  37764  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem12  37772  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem21  37781  poimirlem22  37782  poimirlem23  37783  poimirlem24  37784  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  poimirlem28  37788  poimirlem29  37789  poimirlem31  37791  mblfinlem2  37798  ftc1cnnc  37832  upixp  37869  sdclem2  37882  caushft  37901  ismtyres  37948  rrnmet  37969  rrndstprj1  37970  rrndstprj2  37971  rrncmslem  37972  rrnequiv  37975  iccbnd  37980  osumcllem7N  40161  pexmidlem4N  40172  lcfrlem4  41744  lcfrlem5  41745  lcfrlem6  41746  lcfrlem16  41757  lcfrlem38  41779  mapdrvallem2  41844  mapdh8ab  41976  mapdh8ad  41978  mapdh8e  41983  3factsumint3  42216  aks4d1p1p1  42256  fldhmf1  42283  aks6d1c1p2  42302  aks6d1c1p3  42303  aks6d1c1p7  42306  aks6d1c1p6  42307  aks6d1c1p8  42308  aks6d1c1  42309  evl1gprodd  42310  idomnnzpownz  42325  aks6d1c5lem1  42329  aks6d1c5lem3  42330  aks6d1c5lem2  42331  deg1gprod  42333  sticksstones10  42348  aks6d1c6lem3  42365  aks5lem2  42380  aks5lem3a  42382  unitscyglem5  42392  fz1sump1  42507  sumcubes  42510  evlselv  42772  mhphf2  42783  prjspnfv01  42809  prjspner01  42810  prjspner1  42811  mapfzcons  42900  diophren  42997  irrapxlem1  43006  monotuz  43125  acongeq  43167  jm2.26lem3  43185  jm3.1lem2  43202  pw2f1ocnv  43221  idomodle  43375  trclfvdecomr  43911  imo72b2lem0  44348  imo72b2lem1  44352  scottelrankd  44430  dvgrat  44495  cvgdvgrat  44496  hashnzfz2  44504  fcnre  45212  refsumcn  45217  rfcnnnub  45223  disjf1o  45377  disjinfi  45378  ssmapsn  45402  ssuzfz  45536  nnsplit  45545  uzssd2  45603  uzublem  45616  fsumsermpt  45767  climsuselem1  45795  limcperiod  45816  sumnnodd  45818  lptioo2cn  45831  lptioo1cn  45832  climresmpt  45845  allbutfifvre  45861  climleltrp  45862  cnrefiisplem  46015  cncfshift  46060  cncfperiod  46065  cncfshiftioo  46078  fperdvper  46105  dvnmptdivc  46124  dvnmul  46129  dvmptfprod  46131  dvnprodlem3  46134  stoweidlem11  46197  stoweidlem15  46201  stoweidlem17  46203  stoweidlem20  46206  stoweidlem34  46220  stoweidlem35  46221  stoweidlem46  46232  stoweidlem47  46233  stoweidlem56  46242  stoweidlem59  46245  stoweidlem62  46248  stirlinglem5  46264  stirlinglem14  46273  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  fourierdlem11  46304  fourierdlem15  46308  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem25  46318  fourierdlem48  46340  fourierdlem52  46344  fourierdlem54  46346  fourierdlem58  46350  fourierdlem62  46354  fourierdlem64  46356  fourierdlem65  46357  fourierdlem69  46361  fourierdlem70  46362  fourierdlem71  46363  fourierdlem73  46365  fourierdlem80  46372  fourierdlem81  46373  fourierdlem83  46375  fourierdlem92  46384  fourierdlem93  46385  fourierdlem97  46389  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  fourierdlem113  46405  fouriercnp  46412  fouriersw  46417  elaa2lem  46419  etransclem4  46424  etransclem7  46427  etransclem10  46430  etransclem14  46434  etransclem15  46435  etransclem24  46444  etransclem25  46445  etransclem31  46451  etransclem32  46452  etransclem35  46455  etransclem44  46464  etransclem46  46466  qndenserrnopnlem  46483  qndenserrn  46485  prsal  46504  salgencntex  46529  subsaliuncl  46544  subsalsal  46545  sge0tsms  46566  sge0fodjrnlem  46602  sge0isum  46613  iundjiunlem  46645  iundjiun  46646  meadjiunlem  46651  meaiunlelem  46654  meaiuninclem  46666  meaiininc2  46674  caragensplit  46686  carageneld  46688  carageniuncllem1  46707  caratheodorylem1  46712  caratheodorylem2  46713  hoicvr  46734  hsphoidmvle2  46771  hsphoidmvle  46772  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmvlelem2  46782  hoiqssbllem2  46809  pimdecfgtioc  46901  pimincfltioc  46902  pimdecfgtioo  46903  pimincfltioo  46904  smflimlem3  46959  smfmullem4  46980  smfsupxr  47002  smflimsuplem2  47007  smflimsuplem5  47010  ormklocald  47060  natlocalincr  47062  elmod2  47543  isuspgrim0lem  48081  upgrimtrlslem2  48093  ssnn0ssfz  48537  zlmodzxzscm  48545  rmsupp0  48556  lincsum  48617  lincscm  48618  lindslinindimp2lem4  48649  lincresunit3  48669  elbigofrcl  48738  intubeu  49171  unilbeu  49172  cicrcl2  49230  cic1st2nd  49234  imaf1homlem  49294  oppfrcl  49315  eloppf  49320  imasubc  49338  imaid  49341  oppcuprcl5  49388  oppcup3  49396  uptrlem2  49398  uptrlem3  49399  natoppf  49416  elxpcbasex1ALT  49436  elxpcbasex2ALT  49438  swapf1a  49456  swapf2f1oa  49464  swapfida  49467  cofuswapf1  49481  cofuswapf2  49482  fucoppcco  49596  postc  49756  reldmlan2  49804  reldmran2  49805  lanrcl  49808  ranrcl  49809  setrec1  49878  aacllem  49988