Theorem eleqtrdi 2850

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  eleqtrrdi  2851  3eltr3g  2856  prid2g  4698  ndmfvrcl  6814  fnwelem  7981  tz7.48-1  8283  brwitnlem  8346  oeeulem  8441  dffi3  9199  cnfcom3lem  9470  ttrclse  9494  alephgeom  9847  fpwwe2lem5  10400  canthwelem  10415  hargch  10438  r1wunlim  10502  eluzel2  12596  fseq1p1m1  13339  fznn0sub2  13372  nn0split  13380  seqp1d  13747  exple1  13903  digit1  13961  bcval5  14041  bcpasc  14044  hashf1  14180  seqcoll  14187  seqcoll2  14188  ccatrn  14303  swrdccat2  14391  cats1un  14443  pfxccatin12lem3  14454  splfv2a  14478  splval2  14479  caubnd  15079  limsupgre  15199  clim2ser  15375  clim2ser2  15376  iserex  15377  isermulc2  15378  iserle  15380  iserge0  15381  climub  15382  climserle  15383  isercolllem2  15386  isercolllem3  15387  isercoll  15388  isercoll2  15389  serf0  15401  iseraltlem2  15403  iseraltlem3  15404  iseralt  15405  sumeq2ii  15414  summolem3  15435  summolem2a  15436  fsum  15441  sum0  15442  fsumcl2lem  15452  fsumadd  15461  isumclim3  15480  isumadd  15488  fsump1i  15490  fsummulc2  15505  fsumrelem  15528  iserabs  15536  cvgcmp  15537  cvgcmpub  15538  cvgcmpce  15539  binom1dif  15554  isumshft  15560  isumsplit  15561  isumrpcl  15564  isumsup2  15567  climcndslem1  15570  climcndslem2  15571  climcnds  15572  arisum2  15582  trireciplem  15583  geoser  15588  pwdif  15589  geolim  15591  geo2lim  15596  cvgrat  15604  mertenslem1  15605  mertenslem2  15606  mertens  15607  clim2prod  15609  clim2div  15610  ntrivcvgfvn0  15620  ntrivcvgtail  15621  prodeq2ii  15632  prodmolem3  15652  prodmolem2a  15653  fprod  15660  fprodntriv  15661  fprodss  15667  fprodser  15668  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodabs  15693  fprodeq0  15694  fprodn0  15698  iprodclim3  15719  iprodmul  15722  fallfacfwd  15755  0fallfac  15756  binomfallfaclem2  15759  fallfacval4  15762  bpolysum  15772  bpolydiflem  15773  fsumkthpow  15775  efcvgfsum  15804  efcj  15810  fprodefsum  15813  effsumlt  15829  ruclem7  15954  bitsfzolem  16150  bitsfzo  16151  bitsfi  16153  bitsinv1lem  16157  bitsinv1  16158  bitsinvp1  16165  sadcp1  16171  sadadd  16183  sadass  16187  bitsres  16189  smupp1  16196  smuval2  16198  smupval  16204  smueqlem  16206  smumul  16209  algrp1  16288  phiprmpw  16486  crth  16488  phimullem  16489  eulerthlem2  16492  prmdiv  16495  pcpremul  16553  pcmpt  16602  pcfac  16609  pockthlem  16615  pockthg  16616  prmreclem2  16627  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  prmrec  16632  1arith  16637  vdwapun  16684  vdwlem1  16691  vdwlem2  16692  vdwlem3  16693  vdwlem6  16696  vdwlem8  16698  vdwlem10  16700  vdw  16704  imasvscafn  17257  oppccatid  17439  oppccomfpropd  17447  brcic  17519  funcoppc  17599  invfuc  17701  hofcl  17986  yonedalem4c  18004  gsumwsubmcl  18484  gsumsgrpccat  18487  gsumccatOLD  18488  gsumwmhm  18493  mulgnnp1  18721  mulgnnsubcl  18725  mulgnn0z  18739  mulgnndir  18741  psgnunilem4  19114  psgnran  19132  sylow1lem1  19212  lsmmod2  19291  lsmdisj2r  19300  efginvrel2  19342  efgsdmi  19347  efgsrel  19349  efgs1b  19351  efgsp1  19352  efgredleme  19358  efgredlemc  19360  efgcpbllemb  19370  frgpuplem  19387  mulgnn0di  19436  frgpnabllem1  19483  lt6abl  19505  cycsubgcyg  19511  gsumval3eu  19514  gsumval3  19517  gsumzcl2  19520  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  telgsumfz0s  19601  dprdwd  19623  dprd2da  19654  pgpfaclem1  19693  srgbinom  19790  isirred  19950  lspprid2  20269  lspsnat  20416  lsppratlem1  20418  lsppratlem3  20420  lidl0cl  20492  lidlacl  20493  lidlnegcl  20494  lidlmcl  20497  psgnghm  20794  frlmvscavalb  20986  frlmvplusgscavalb  20987  psrbaglefi  21144  psrbaglefiOLD  21145  psrass23l  21186  psrass23  21188  mplcoe5lem  21249  mpfind  21326  selvval  21337  mhpvscacl  21353  psr1bascl  21380  ply1basf  21382  gsummoncoe1  21484  lply1binom  21486  lply1binomsc  21487  mpfpf1  21526  pf1mpf  21527  evl1scvarpw  21538  matbas2i  21580  matecld  21584  matgsum  21595  mpomatmul  21604  dmatmul  21655  1mavmul  21706  mdetleib2  21746  m1detdiag  21755  marep01ma  21818  smadiadetlem4  21827  slesolinv  21838  pmatcollpw3fi1lem1  21944  chpscmat  22000  chpscmatgsumbin  22002  chp0mat  22004  chpidmat  22005  chfacfisf  22012  chfacfisfcpmat  22013  chfacfpmmulgsum2  22023  cldrcl  22186  ordtbas  22352  iscnp2  22399  dis1stc  22659  ptbasfi  22741  ptpjopn  22772  ptclsg  22775  ptcnp  22782  kqtop  22905  reghmph  22953  ptcmplem2  23213  ptcmplem3  23214  ptcmplem4  23215  tsmslem1  23289  utop2nei  23411  isucn2  23440  cuspcvg  23462  cnextucn  23464  imasdsf1olem  23535  blcvx  23970  xrhmeo  24118  cnrehmeo  24125  evth  24131  reparphti  24169  iscau4  24452  iscmet3lem1  24464  lmle  24474  rrxfsupp  24575  rrxdsfi  24584  pjthlem2  24611  ovollb2lem  24661  ovolunlem1a  24669  ovoliunlem1  24675  ovoliun2  24679  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem4  24693  iundisj2  24722  voliunlem1  24723  volsup  24729  ioombl1lem4  24734  uniioovol  24752  uniioombllem3  24758  uniioombllem4  24759  uniioombllem6  24761  vitalilem5  24785  mbfimaopnlem  24828  mbflimsup  24839  mbfi1fseqlem3  24891  iblitg  24942  dvnp1  25098  cpncn  25109  dvlip2  25168  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumrlimge0  25203  dvfsumrlim2  25205  ftc1cn  25216  elplyd  25372  ply1termlem  25373  ply1term  25374  ply0  25378  plyeq0lem  25380  plyaddlem1  25383  plymullem1  25384  plyaddlem  25385  plymullem  25386  coeeulem  25394  plyco  25411  coeeq2  25412  coefv0  25418  coemulhi  25424  coemulc  25425  plycj  25447  dvply1  25453  vieta1lem2  25480  elqaalem2  25489  dvtaylp  25538  dvntaylp  25539  taylthlem1  25541  taylth  25543  ulmres  25556  ulmshftlem  25557  ulmshft  25558  ulmcau  25563  ulmdvlem1  25568  mtest  25572  mtestbdd  25573  pserulm  25590  psercn2  25591  psercnlem1  25593  psercn  25594  pserdvlem2  25596  abelthlem6  25604  abelth  25609  efif1olem1  25707  efif1olem3  25709  efif1olem4  25710  logcn  25811  advlogexp  25819  efopn  25822  cxpeq  25919  asinsin  26051  atantayl  26096  leibpilem2  26100  birthdaylem2  26111  birthdaylem3  26112  efrlim  26128  emcllem2  26155  emcllem5  26158  emcllem7  26160  harmonicbnd4  26169  fsumharmonic  26170  lgamgulm2  26194  lgamcvglem  26198  lgamcvg2  26213  gamcvg2lem  26217  wilthlem2  26227  wilthlem3  26228  ftalem1  26231  ftalem2  26232  ftalem3  26233  ftalem5  26235  basellem2  26240  basellem3  26241  basellem5  26243  basellem8  26246  ppiprm  26309  ppinprm  26310  chtprm  26311  chtnprm  26312  chpp1  26313  vma1  26324  ppiltx  26335  musum  26349  0sgmppw  26355  1sgmprm  26356  ppiublem2  26360  chtublem  26368  fsumvma2  26371  chpchtsum  26376  logexprlim  26382  bposlem5  26445  lgscllem  26461  lgsval2lem  26464  lgsval4a  26476  lgsneg  26478  lgsdir2lem3  26484  lgsdir2lem5  26486  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  gausslemma2dlem3  26525  lgseisenlem1  26532  lgsquadlem2  26538  chebbnd1lem1  26626  chtppilimlem1  26630  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasum2lem  26653  dchrvmasumiflem1  26658  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0flb  26667  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  mudivsum  26687  mulogsum  26689  mulog2sumlem2  26692  selberg2lem  26707  logdivbnd  26713  pntrsumo1  26722  pntrsumbnd2  26724  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  pntrlog2bndlem6a  26739  pntlemj  26760  pntlemf  26762  ostth2lem3  26792  tglngne  26920  ltgseg  26966  eedimeq  27275  axlowdimlem16  27334  ebtwntg  27359  subgruhgredgd  27660  subumgredg2  27661  umgrres1lem  27686  wlkson  28033  wksonproplem  28081  wksonproplemOLD  28082  trlsonfval  28083  pthsonfval  28117  spthson  28118  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  eupth2lems  28611  numclwwlk1lem2foa  28727  numclwlk1lem2  28743  numclwwlk2lem1  28749  htthlem  29288  hhsscms  29649  shmodsi  29760  pjoc1i  29802  5oalem1  30025  mayete3i  30099  adj1  30304  iundisj2f  30938  fmptco1f1o  30977  fcnvgreu  31019  suppovss  31026  ssnnssfz  31117  iundisj2fi  31127  cshw1s2  31241  gsumhashmul  31325  pmtrto1cl  31375  psgnfzto1stlem  31376  fzto1st1  31378  cycpmfv1  31389  cycpmfv2  31390  cycpmco2rn  31401  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cyc3evpm  31426  cyc3genpm  31428  cycpmconjslem2  31431  cyc3conja  31433  rspsnel  31576  nsgmgc  31606  nsgqusf1olem2  31608  idlsrgmulrss1  31665  idlsrgmulrss2  31666  lindsun  31715  fldextfld1  31733  fldextfld2  31734  1smat1  31763  submateqlem2  31767  lmatfval  31773  mdetlap1  31785  madjusmdetlem1  31786  madjusmdetlem2  31787  madjusmdetlem3  31788  madjusmdetlem4  31789  zarclssn  31832  zartopn  31834  zarmxt1  31839  rhmpreimacnlem  31843  rhmpreimacn  31844  pnfneige0  31910  pl1cn  31914  rrhqima  31973  indpreima  32002  esumfzf  32046  esumpcvgval  32055  esumpmono  32056  esumcvg  32063  ldgenpisyslem1  32140  ldgenpisys  32143  measbase  32174  dya2iocnei  32258  oddpwdc  32330  eulerpartlems  32336  eulerpartlemb  32344  sseqf  32368  fibp1  32377  orrvcval4  32440  orrvcoel  32441  orrvccel  32442  ballotlem2  32464  ballotlemfrceq  32504  signsplypnf  32538  signswch  32549  signstf0  32556  signstfvn  32557  signstfvneq0  32560  signstfvcl  32561  signstfveq0  32565  signsvfn  32570  fct2relem  32586  fsum2dsub  32596  reprsuc  32604  reprpmtf1o  32615  breprexplema  32619  breprexplemc  32621  hgt749d  32638  hgt750lemb  32645  tgoldbachgnn  32648  bnj1172  32990  bnj1245  33003  bnj1311  33013  bnj1450  33039  bnj1501  33056  subfacp1lem1  33150  subfacp1lem5  33155  subfacp1lem6  33156  subfacval2  33158  erdszelem7  33168  cvxsconn  33214  cvmliftlem5  33260  cvmliftlem7  33262  cvmliftlem10  33265  cvmliftlem13  33267  mrsubvrs  33493  msubrn  33500  msubco  33502  msubvrs  33531  madebdayim  34079  oldbdayim  34080  imageval  34241  fwddifnp1  34476  knoppcnlem8  34689  knoppcnlem10  34691  bj-unirel  35233  icoreunrn  35539  istoprelowl  35540  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem12  35798  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  ftc1cnnc  35858  upixp  35896  sdclem2  35909  caushft  35928  ismtyres  35975  rrnmet  35996  rrndstprj1  35997  rrndstprj2  35998  rrncmslem  35999  rrnequiv  36002  iccbnd  36007  osumcllem7N  37983  pexmidlem4N  37994  lcfrlem4  39566  lcfrlem5  39567  lcfrlem6  39568  lcfrlem16  39579  lcfrlem38  39601  mapdrvallem2  39666  mapdh8ab  39798  mapdh8ad  39800  mapdh8e  39805  3factsumint3  40038  aks4d1p1p1  40078  sticksstones10  40118  metakunt20  40151  mhphf2  40293  prjspnfv01  40468  prjspner01  40469  prjspner1  40470  mapfzcons  40545  diophren  40642  irrapxlem1  40651  monotuz  40770  acongeq  40812  jm2.26lem3  40830  jm3.1lem2  40847  pw2f1ocnv  40866  idomodle  41028  trclfvdecomr  41343  imo72b2lem1  41787  scottelrankd  41872  dvgrat  41937  cvgdvgrat  41938  hashnzfz2  41946  fcnre  42575  refsumcn  42580  rfcnnnub  42586  disjf1o  42736  disjinfi  42738  ssmapsn  42763  ssuzfz  42895  nnsplit  42904  uzssd2  42964  uzublem  42977  fsumsermpt  43127  climsuselem1  43155  limcperiod  43176  sumnnodd  43178  lptioo2cn  43193  lptioo1cn  43194  climresmpt  43207  allbutfifvre  43223  climleltrp  43224  cnrefiisplem  43377  cncfshift  43422  cncfperiod  43427  cncfshiftioo  43440  fperdvper  43467  dvnmptdivc  43486  dvnmul  43491  dvmptfprod  43493  dvnprodlem3  43496  stoweidlem11  43559  stoweidlem15  43563  stoweidlem17  43565  stoweidlem20  43568  stoweidlem34  43582  stoweidlem35  43583  stoweidlem46  43594  stoweidlem47  43595  stoweidlem56  43604  stoweidlem59  43607  stoweidlem62  43610  stirlinglem5  43626  stirlinglem14  43635  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  fourierdlem11  43666  fourierdlem15  43670  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem25  43680  fourierdlem48  43702  fourierdlem52  43706  fourierdlem54  43708  fourierdlem58  43712  fourierdlem62  43716  fourierdlem64  43718  fourierdlem65  43719  fourierdlem69  43723  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem80  43734  fourierdlem81  43735  fourierdlem83  43737  fourierdlem92  43746  fourierdlem93  43747  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem113  43767  fouriercnp  43774  fouriersw  43779  elaa2lem  43781  etransclem4  43786  etransclem7  43789  etransclem10  43792  etransclem14  43796  etransclem15  43797  etransclem24  43806  etransclem25  43807  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem44  43826  etransclem46  43828  qndenserrnopnlem  43845  qndenserrn  43847  prsal  43866  salgencntex  43889  subsaliuncl  43904  subsalsal  43905  sge0tsms  43925  sge0fodjrnlem  43961  sge0isum  43972  iundjiunlem  44004  iundjiun  44005  meadjiunlem  44010  meaiunlelem  44013  meaiuninclem  44025  meaiininc2  44033  caragensplit  44045  carageneld  44047  carageniuncllem1  44066  caratheodorylem1  44071  caratheodorylem2  44072  hoicvr  44093  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem2  44141  hoiqssbllem2  44168  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  smflimlem3  44318  smfmullem4  44339  smfsupxr  44360  smflimsuplem2  44365  smflimsuplem5  44368  elmod2  44833  ssnn0ssfz  45696  zlmodzxzscm  45704  rmsupp0  45715  lincsum  45781  lincscm  45782  lindslinindimp2lem4  45813  lincresunit3  45833  elbigofrcl  45907  intubeu  46281  unilbeu  46282  postc  46374  setrec1  46408  aacllem  46516  natlocalincr  46522