Theorem eleqtrdi 2843

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  eleqtrrdi  2844  3eltr3g  2849  prid2g  4764  ndmfvrcl  6924  fnwelem  8113  tz7.48-1  8439  brwitnlem  8503  oeeulem  8597  dffi3  9422  cnfcom3lem  9694  ttrclse  9718  alephgeom  10073  fpwwe2lem5  10626  canthwelem  10641  hargch  10664  r1wunlim  10728  eluzel2  12823  fseq1p1m1  13571  fznn0sub2  13604  nn0split  13612  seqp1d  13979  exple1  14137  digit1  14196  bcval5  14274  bcpasc  14277  hashf1  14414  seqcoll  14421  seqcoll2  14422  ccatrn  14535  swrdccat2  14615  cats1un  14667  pfxccatin12lem3  14678  splfv2a  14702  splval2  14703  caubnd  15301  limsupgre  15421  clim2ser  15597  clim2ser2  15598  iserex  15599  isermulc2  15600  iserle  15602  iserge0  15603  climub  15604  climserle  15605  isercolllem2  15608  isercolllem3  15609  isercoll  15610  isercoll2  15611  serf0  15623  iseraltlem2  15625  iseraltlem3  15626  iseralt  15627  sumeq2ii  15635  summolem3  15656  summolem2a  15657  fsum  15662  sum0  15663  fsumcl2lem  15673  fsumadd  15682  isumclim3  15701  isumadd  15709  fsump1i  15711  fsummulc2  15726  fsumrelem  15749  iserabs  15757  cvgcmp  15758  cvgcmpub  15759  cvgcmpce  15760  binom1dif  15775  isumshft  15781  isumsplit  15782  isumrpcl  15785  isumsup2  15788  climcndslem1  15791  climcndslem2  15792  climcnds  15793  arisum2  15803  trireciplem  15804  geoser  15809  pwdif  15810  geolim  15812  geo2lim  15817  cvgrat  15825  mertenslem1  15826  mertenslem2  15827  mertens  15828  clim2prod  15830  clim2div  15831  ntrivcvgfvn0  15841  ntrivcvgtail  15842  prodeq2ii  15853  prodmolem3  15873  prodmolem2a  15874  fprod  15881  fprodntriv  15882  fprodss  15888  fprodser  15889  fprodcl2lem  15890  fprodmul  15900  fproddiv  15901  fprodabs  15914  fprodeq0  15915  fprodn0  15919  iprodclim3  15940  iprodmul  15943  fallfacfwd  15976  0fallfac  15977  binomfallfaclem2  15980  fallfacval4  15983  bpolysum  15993  bpolydiflem  15994  fsumkthpow  15996  efcvgfsum  16025  efcj  16031  fprodefsum  16034  effsumlt  16050  ruclem7  16175  bitsfzolem  16371  bitsfzo  16372  bitsfi  16374  bitsinv1lem  16378  bitsinv1  16379  bitsinvp1  16386  sadcp1  16392  sadadd  16404  sadass  16408  bitsres  16410  smupp1  16417  smuval2  16419  smupval  16425  smueqlem  16427  smumul  16430  algrp1  16507  phiprmpw  16705  crth  16707  phimullem  16708  eulerthlem2  16711  prmdiv  16714  pcpremul  16772  pcmpt  16821  pcfac  16828  pockthlem  16834  pockthg  16835  prmreclem2  16846  prmreclem3  16847  prmreclem4  16848  prmreclem5  16849  prmreclem6  16850  prmrec  16851  1arith  16856  vdwapun  16903  vdwlem1  16910  vdwlem2  16911  vdwlem3  16912  vdwlem6  16915  vdwlem8  16917  vdwlem10  16919  vdw  16923  imasvscafn  17479  oppccatid  17661  oppccomfpropd  17669  brcic  17741  funcoppc  17821  invfuc  17923  hofcl  18208  yonedalem4c  18226  gsumwsubmcl  18714  gsumsgrpccat  18717  gsumwmhm  18722  mulgnnp1  18956  mulgnnsubcl  18960  mulgnn0z  18975  mulgnndir  18977  psgnunilem4  19359  psgnran  19377  sylow1lem1  19460  lsmmod2  19538  lsmdisj2r  19547  efginvrel2  19589  efgsdmi  19594  efgsrel  19596  efgs1b  19598  efgsp1  19599  efgredleme  19605  efgredlemc  19607  efgcpbllemb  19617  frgpuplem  19634  mulgnn0di  19687  frgpnabllem1  19735  lt6abl  19757  cycsubgcyg  19763  gsumval3eu  19766  gsumval3  19769  gsumzcl2  19772  gsumzaddlem  19783  gsumconst  19796  gsumzmhm  19799  gsumzoppg  19806  telgsumfz0s  19853  dprdwd  19875  dprd2da  19906  pgpfaclem1  19945  srgbinom  20047  isirred  20225  lspprid2  20601  lspsnat  20750  lsppratlem1  20752  lsppratlem3  20754  lidl0cl  20827  lidlacl  20828  lidlnegcl  20829  lidlmcl  20832  2idllidld  20858  2idlridld  20859  psgnghm  21124  frlmvscavalb  21316  frlmvplusgscavalb  21317  psrbaglefi  21476  psrbaglefiOLD  21477  psrass23l  21519  psrass23  21521  mplcoe5lem  21585  mpfind  21661  selvval  21672  mhpvscacl  21688  psr1bascl  21715  ply1basf  21717  gsummoncoe1  21819  lply1binom  21821  lply1binomsc  21822  mpfpf1  21861  pf1mpf  21862  evl1scvarpw  21873  matbas2i  21915  matecld  21919  matgsum  21930  mpomatmul  21939  dmatmul  21990  1mavmul  22041  mdetleib2  22081  m1detdiag  22090  marep01ma  22153  smadiadetlem4  22162  slesolinv  22173  pmatcollpw3fi1lem1  22279  chpscmat  22335  chpscmatgsumbin  22337  chp0mat  22339  chpidmat  22340  chfacfisf  22347  chfacfisfcpmat  22348  chfacfpmmulgsum2  22358  cldrcl  22521  ordtbas  22687  iscnp2  22734  dis1stc  22994  ptbasfi  23076  ptpjopn  23107  ptclsg  23110  ptcnp  23117  kqtop  23240  reghmph  23288  ptcmplem2  23548  ptcmplem3  23549  ptcmplem4  23550  tsmslem1  23624  utop2nei  23746  isucn2  23775  cuspcvg  23797  cnextucn  23799  imasdsf1olem  23870  blcvx  24305  xrhmeo  24453  cnrehmeo  24460  evth  24466  reparphti  24504  iscau4  24787  iscmet3lem1  24799  lmle  24809  rrxfsupp  24910  rrxdsfi  24919  pjthlem2  24946  ovollb2lem  24996  ovolunlem1a  25004  ovoliunlem1  25010  ovoliun2  25014  ovolscalem1  25021  ovolicc1  25024  ovolicc2lem4  25028  iundisj2  25057  voliunlem1  25058  volsup  25064  ioombl1lem4  25069  uniioovol  25087  uniioombllem3  25093  uniioombllem4  25094  uniioombllem6  25096  vitalilem5  25120  mbfimaopnlem  25163  mbflimsup  25174  mbfi1fseqlem3  25226  iblitg  25277  dvnp1  25433  cpncn  25444  dvlip2  25503  dvfsumlem2  25535  dvfsumlem3  25536  dvfsumrlimge0  25538  dvfsumrlim2  25540  ftc1cn  25551  elplyd  25707  ply1termlem  25708  ply1term  25709  ply0  25713  plyeq0lem  25715  plyaddlem1  25718  plymullem1  25719  plyaddlem  25720  plymullem  25721  coeeulem  25729  plyco  25746  coeeq2  25747  coefv0  25753  coemulhi  25759  coemulc  25760  plycj  25782  dvply1  25788  vieta1lem2  25815  elqaalem2  25824  dvtaylp  25873  dvntaylp  25874  taylthlem1  25876  taylth  25878  ulmres  25891  ulmshftlem  25892  ulmshft  25893  ulmcau  25898  ulmdvlem1  25903  mtest  25907  mtestbdd  25908  pserulm  25925  psercn2  25926  psercnlem1  25928  psercn  25929  pserdvlem2  25931  abelthlem6  25939  abelth  25944  efif1olem1  26042  efif1olem3  26044  efif1olem4  26045  logcn  26146  advlogexp  26154  efopn  26157  cxpeq  26254  asinsin  26386  atantayl  26431  leibpilem2  26435  birthdaylem2  26446  birthdaylem3  26447  efrlim  26463  emcllem2  26490  emcllem5  26493  emcllem7  26495  harmonicbnd4  26504  fsumharmonic  26505  lgamgulm2  26529  lgamcvglem  26533  lgamcvg2  26548  gamcvg2lem  26552  wilthlem2  26562  wilthlem3  26563  ftalem1  26566  ftalem2  26567  ftalem3  26568  ftalem5  26570  basellem2  26575  basellem3  26576  basellem5  26578  basellem8  26581  ppiprm  26644  ppinprm  26645  chtprm  26646  chtnprm  26647  chpp1  26648  vma1  26659  ppiltx  26670  musum  26684  0sgmppw  26690  1sgmprm  26691  ppiublem2  26695  chtublem  26703  fsumvma2  26706  chpchtsum  26711  logexprlim  26717  bposlem5  26780  lgscllem  26796  lgsval2lem  26799  lgsval4a  26811  lgsneg  26813  lgsdir2lem3  26819  lgsdir2lem5  26821  lgsdir  26824  lgsdilem2  26825  lgsdi  26826  lgsne0  26827  gausslemma2dlem3  26860  lgseisenlem1  26867  lgsquadlem2  26873  chebbnd1lem1  26961  chtppilimlem1  26965  rplogsumlem2  26977  rpvmasumlem  26979  dchrisumlem1  26981  dchrisumlem2  26982  dchrmusum2  26986  dchrvmasum2lem  26988  dchrvmasumiflem1  26993  dchrisum0flblem1  27000  dchrisum0flblem2  27001  dchrisum0flb  27002  dchrisum0re  27005  dchrisum0lem1b  27007  dchrisum0lem1  27008  dchrisum0lem2a  27009  dchrisum0lem2  27010  dchrisum0lem3  27011  mudivsum  27022  mulogsum  27024  mulog2sumlem2  27027  selberg2lem  27042  logdivbnd  27048  pntrsumo1  27057  pntrsumbnd2  27059  pntrlog2bndlem2  27070  pntrlog2bndlem4  27072  pntrlog2bndlem6a  27074  pntlemj  27095  pntlemf  27097  ostth2lem3  27127  madebdayim  27371  oldbdayim  27372  tglngne  27790  ltgseg  27836  eedimeq  28145  axlowdimlem16  28204  ebtwntg  28229  subgruhgredgd  28530  subumgredg2  28531  umgrres1lem  28556  wlkson  28902  wksonproplem  28950  wksonproplemOLD  28951  trlsonfval  28952  pthsonfval  28986  spthson  28987  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  eupth2lems  29480  numclwwlk1lem2foa  29596  numclwlk1lem2  29612  numclwwlk2lem1  29618  htthlem  30157  hhsscms  30518  shmodsi  30629  pjoc1i  30671  5oalem1  30894  mayete3i  30968  adj1  31173  iundisj2f  31808  fmptco1f1o  31844  fcnvgreu  31885  suppovss  31893  ssnnssfz  31985  iundisj2fi  31995  cshw1s2  32111  gsumhashmul  32195  pmtrto1cl  32245  psgnfzto1stlem  32246  fzto1st1  32248  cycpmfv1  32259  cycpmfv2  32260  cycpmco2rn  32271  cycpmco2lem4  32275  cycpmco2lem5  32276  cycpmco2lem6  32277  cyc3evpm  32296  cyc3genpm  32298  cycpmconjslem2  32301  cyc3conja  32303  idomdomd  32361  idomringd  32362  idomrcan  32364  rspsnel  32472  nsgmgc  32511  nsgqusf1olem2  32513  ghmquskerlem1  32516  ghmquskerco  32517  unitpidl1  32530  elrspunsn  32535  mxidlirredi  32575  mxidlirred  32576  opprqusplusg  32591  opprqus0g  32592  opprqusmulr  32593  idlsrgmulrss1  32613  idlsrgmulrss2  32614  ig1pmindeg  32659  ply1degltdimlem  32695  lindsun  32698  fldextfld1  32716  fldextfld2  32717  1smat1  32772  submateqlem2  32776  lmatfval  32782  mdetlap1  32794  madjusmdetlem1  32795  madjusmdetlem2  32796  madjusmdetlem3  32797  madjusmdetlem4  32798  zarclssn  32841  zartopn  32843  zarmxt1  32848  rhmpreimacnlem  32852  rhmpreimacn  32853  pnfneige0  32919  pl1cn  32923  rrhqima  32982  indpreima  33011  esumfzf  33055  esumpcvgval  33064  esumpmono  33065  esumcvg  33072  ldgenpisyslem1  33149  ldgenpisys  33152  measbase  33183  dya2iocnei  33269  oddpwdc  33341  eulerpartlems  33347  eulerpartlemb  33355  sseqf  33379  fibp1  33388  orrvcval4  33451  orrvcoel  33452  orrvccel  33453  ballotlem2  33475  ballotlemfrceq  33515  signsplypnf  33549  signswch  33560  signstf0  33567  signstfvn  33568  signstfvneq0  33571  signstfvcl  33572  signstfveq0  33576  signsvfn  33581  fct2relem  33597  fsum2dsub  33607  reprsuc  33615  reprpmtf1o  33626  breprexplema  33630  breprexplemc  33632  hgt749d  33649  hgt750lemb  33656  tgoldbachgnn  33659  bnj1172  34000  bnj1245  34013  bnj1311  34023  bnj1450  34049  bnj1501  34066  subfacp1lem1  34158  subfacp1lem5  34163  subfacp1lem6  34164  subfacval2  34166  erdszelem7  34176  cvxsconn  34222  cvmliftlem5  34268  cvmliftlem7  34270  cvmliftlem10  34273  cvmliftlem13  34275  mrsubvrs  34501  msubrn  34508  msubco  34510  msubvrs  34539  imageval  34890  fwddifnp1  35125  gg-cnrehmeo  35159  gg-reparphti  35160  gg-dvcnp2  35162  gg-dvmulbr  35163  gg-dvcobr  35164  gg-psercn2  35166  gg-dvfsumlem2  35171  knoppcnlem8  35364  knoppcnlem10  35366  bj-unirel  35920  icoreunrn  36228  istoprelowl  36229  poimirlem3  36479  poimirlem4  36480  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem12  36488  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem19  36495  poimirlem20  36496  poimirlem21  36497  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  poimirlem29  36505  poimirlem31  36507  mblfinlem2  36514  ftc1cnnc  36548  upixp  36585  sdclem2  36598  caushft  36617  ismtyres  36664  rrnmet  36685  rrndstprj1  36686  rrndstprj2  36687  rrncmslem  36688  rrnequiv  36691  iccbnd  36696  osumcllem7N  38821  pexmidlem4N  38832  lcfrlem4  40404  lcfrlem5  40405  lcfrlem6  40406  lcfrlem16  40417  lcfrlem38  40439  mapdrvallem2  40504  mapdh8ab  40636  mapdh8ad  40638  mapdh8e  40643  3factsumint3  40876  aks4d1p1p1  40916  fldhmf1  40943  sticksstones10  40959  metakunt20  40992  evlselv  41156  mhphf2  41167  fz1sump1  41203  sumcubes  41206  prjspnfv01  41362  prjspner01  41363  prjspner1  41364  mapfzcons  41439  diophren  41536  irrapxlem1  41545  monotuz  41665  acongeq  41707  jm2.26lem3  41725  jm3.1lem2  41742  pw2f1ocnv  41761  idomodle  41923  trclfvdecomr  42464  imo72b2lem1  42906  scottelrankd  42991  dvgrat  43056  cvgdvgrat  43057  hashnzfz2  43065  fcnre  43694  refsumcn  43699  rfcnnnub  43705  disjf1o  43874  disjinfi  43876  ssmapsn  43900  ssuzfz  44045  nnsplit  44054  uzssd2  44113  uzublem  44126  fsumsermpt  44281  climsuselem1  44309  limcperiod  44330  sumnnodd  44332  lptioo2cn  44347  lptioo1cn  44348  climresmpt  44361  allbutfifvre  44377  climleltrp  44378  cnrefiisplem  44531  cncfshift  44576  cncfperiod  44581  cncfshiftioo  44594  fperdvper  44621  dvnmptdivc  44640  dvnmul  44645  dvmptfprod  44647  dvnprodlem3  44650  stoweidlem11  44713  stoweidlem15  44717  stoweidlem17  44719  stoweidlem20  44722  stoweidlem34  44736  stoweidlem35  44737  stoweidlem46  44748  stoweidlem47  44749  stoweidlem56  44758  stoweidlem59  44761  stoweidlem62  44764  stirlinglem5  44780  stirlinglem14  44789  dirkertrigeqlem2  44801  dirkertrigeqlem3  44802  fourierdlem11  44820  fourierdlem15  44824  fourierdlem16  44825  fourierdlem21  44830  fourierdlem22  44831  fourierdlem25  44834  fourierdlem48  44856  fourierdlem52  44860  fourierdlem54  44862  fourierdlem58  44866  fourierdlem62  44870  fourierdlem64  44872  fourierdlem65  44873  fourierdlem69  44877  fourierdlem70  44878  fourierdlem71  44879  fourierdlem73  44881  fourierdlem80  44888  fourierdlem81  44889  fourierdlem83  44891  fourierdlem92  44900  fourierdlem93  44901  fourierdlem97  44905  fourierdlem103  44911  fourierdlem104  44912  fourierdlem112  44920  fourierdlem113  44921  fouriercnp  44928  fouriersw  44933  elaa2lem  44935  etransclem4  44940  etransclem7  44943  etransclem10  44946  etransclem14  44950  etransclem15  44951  etransclem24  44960  etransclem25  44961  etransclem31  44967  etransclem32  44968  etransclem35  44971  etransclem44  44980  etransclem46  44982  qndenserrnopnlem  44999  qndenserrn  45001  prsal  45020  salgencntex  45045  subsaliuncl  45060  subsalsal  45061  sge0tsms  45082  sge0fodjrnlem  45118  sge0isum  45129  iundjiunlem  45161  iundjiun  45162  meadjiunlem  45167  meaiunlelem  45170  meaiuninclem  45182  meaiininc2  45190  caragensplit  45202  carageneld  45204  carageniuncllem1  45223  caratheodorylem1  45228  caratheodorylem2  45229  hoicvr  45250  hsphoidmvle2  45287  hsphoidmvle  45288  hoidmv1lelem2  45294  hoidmv1lelem3  45295  hoidmvlelem2  45298  hoiqssbllem2  45325  pimdecfgtioc  45417  pimincfltioc  45418  pimdecfgtioo  45419  pimincfltioo  45420  smflimlem3  45475  smfmullem4  45496  smfsupxr  45518  smflimsuplem2  45523  smflimsuplem5  45526  natlocalincr  45576  elmod2  46024  rng2idl1cntr  46770  ssnn0ssfz  46978  zlmodzxzscm  46986  rmsupp0  46997  lincsum  47063  lincscm  47064  lindslinindimp2lem4  47095  lincresunit3  47115  elbigofrcl  47189  intubeu  47562  unilbeu  47563  postc  47655  setrec1  47689  aacllem  47801