Theorem eleqtrdi 2849

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eleqtrrdi  2850  3eltr3g  2855  prid2g  4694  ndmfvrcl  6787  fnwelem  7943  tz7.48-1  8244  brwitnlem  8299  oeeulem  8394  dffi3  9120  cnfcom3lem  9391  alephgeom  9769  fpwwe2lem5  10322  canthwelem  10337  hargch  10360  r1wunlim  10424  eluzel2  12516  fseq1p1m1  13259  fznn0sub2  13292  nn0split  13300  seqp1d  13666  exple1  13822  digit1  13880  bcval5  13960  bcpasc  13963  hashf1  14099  seqcoll  14106  seqcoll2  14107  ccatrn  14222  swrdccat2  14310  cats1un  14362  pfxccatin12lem3  14373  splfv2a  14397  splval2  14398  caubnd  14998  limsupgre  15118  clim2ser  15294  clim2ser2  15295  iserex  15296  isermulc2  15297  iserle  15299  iserge0  15300  climub  15301  climserle  15302  isercolllem2  15305  isercolllem3  15306  isercoll  15307  isercoll2  15308  serf0  15320  iseraltlem2  15322  iseraltlem3  15323  iseralt  15324  sumeq2ii  15333  summolem3  15354  summolem2a  15355  fsum  15360  sum0  15361  fsumcl2lem  15371  fsumadd  15380  isumclim3  15399  isumadd  15407  fsump1i  15409  fsummulc2  15424  fsumrelem  15447  iserabs  15455  cvgcmp  15456  cvgcmpub  15457  cvgcmpce  15458  binom1dif  15473  isumshft  15479  isumsplit  15480  isumrpcl  15483  isumsup2  15486  climcndslem1  15489  climcndslem2  15490  climcnds  15491  arisum2  15501  trireciplem  15502  geoser  15507  pwdif  15508  geolim  15510  geo2lim  15515  cvgrat  15523  mertenslem1  15524  mertenslem2  15525  mertens  15526  clim2prod  15528  clim2div  15529  ntrivcvgfvn0  15539  ntrivcvgtail  15540  prodeq2ii  15551  prodmolem3  15571  prodmolem2a  15572  fprod  15579  fprodntriv  15580  fprodss  15586  fprodser  15587  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodabs  15612  fprodeq0  15613  fprodn0  15617  iprodclim3  15638  iprodmul  15641  fallfacfwd  15674  0fallfac  15675  binomfallfaclem2  15678  fallfacval4  15681  bpolysum  15691  bpolydiflem  15692  fsumkthpow  15694  efcvgfsum  15723  efcj  15729  fprodefsum  15732  effsumlt  15748  ruclem7  15873  bitsfzolem  16069  bitsfzo  16070  bitsfi  16072  bitsinv1lem  16076  bitsinv1  16077  bitsinvp1  16084  sadcp1  16090  sadadd  16102  sadass  16106  bitsres  16108  smupp1  16115  smuval2  16117  smupval  16123  smueqlem  16125  smumul  16128  algrp1  16207  phiprmpw  16405  crth  16407  phimullem  16408  eulerthlem2  16411  prmdiv  16414  pcpremul  16472  pcmpt  16521  pcfac  16528  pockthlem  16534  pockthg  16535  prmreclem2  16546  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  prmrec  16551  1arith  16556  vdwapun  16603  vdwlem1  16610  vdwlem2  16611  vdwlem3  16612  vdwlem6  16615  vdwlem8  16617  vdwlem10  16619  vdw  16623  imasvscafn  17165  oppccatid  17347  oppccomfpropd  17355  brcic  17427  funcoppc  17506  invfuc  17608  hofcl  17893  yonedalem4c  17911  gsumwsubmcl  18390  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  mulgnnp1  18627  mulgnnsubcl  18631  mulgnn0z  18645  mulgnndir  18647  psgnunilem4  19020  psgnran  19038  sylow1lem1  19118  lsmmod2  19197  lsmdisj2r  19206  efginvrel2  19248  efgsdmi  19253  efgsrel  19255  efgs1b  19257  efgsp1  19258  efgredleme  19264  efgredlemc  19266  efgcpbllemb  19276  frgpuplem  19293  mulgnn0di  19342  frgpnabllem1  19389  lt6abl  19411  cycsubgcyg  19417  gsumval3eu  19420  gsumval3  19423  gsumzcl2  19426  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  telgsumfz0s  19507  dprdwd  19529  dprd2da  19560  pgpfaclem1  19599  srgbinom  19696  isirred  19856  lspprid2  20175  lspsnat  20322  lsppratlem1  20324  lsppratlem3  20326  lidl0cl  20396  lidlacl  20397  lidlnegcl  20398  lidlmcl  20401  psgnghm  20697  frlmvscavalb  20887  frlmvplusgscavalb  20888  psrbaglefi  21045  psrbaglefiOLD  21046  psrass23l  21087  psrass23  21089  mplcoe5lem  21150  mpfind  21227  selvval  21238  mhpvscacl  21254  psr1bascl  21281  ply1basf  21283  gsummoncoe1  21385  lply1binom  21387  lply1binomsc  21388  mpfpf1  21427  pf1mpf  21428  evl1scvarpw  21439  matbas2i  21479  matecld  21483  matgsum  21494  mpomatmul  21503  dmatmul  21554  1mavmul  21605  mdetleib2  21645  m1detdiag  21654  marep01ma  21717  smadiadetlem4  21726  slesolinv  21737  pmatcollpw3fi1lem1  21843  chpscmat  21899  chpscmatgsumbin  21901  chp0mat  21903  chpidmat  21904  chfacfisf  21911  chfacfisfcpmat  21912  chfacfpmmulgsum2  21922  cldrcl  22085  ordtbas  22251  iscnp2  22298  dis1stc  22558  ptbasfi  22640  ptpjopn  22671  ptclsg  22674  ptcnp  22681  kqtop  22804  reghmph  22852  ptcmplem2  23112  ptcmplem3  23113  ptcmplem4  23114  tsmslem1  23188  utop2nei  23310  isucn2  23339  cuspcvg  23361  cnextucn  23363  imasdsf1olem  23434  blcvx  23867  xrhmeo  24015  cnrehmeo  24022  evth  24028  reparphti  24066  iscau4  24348  iscmet3lem1  24360  lmle  24370  rrxfsupp  24471  rrxdsfi  24480  pjthlem2  24507  ovollb2lem  24557  ovolunlem1a  24565  ovoliunlem1  24571  ovoliun2  24575  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem4  24589  iundisj2  24618  voliunlem1  24619  volsup  24625  ioombl1lem4  24630  uniioovol  24648  uniioombllem3  24654  uniioombllem4  24655  uniioombllem6  24657  vitalilem5  24681  mbfimaopnlem  24724  mbflimsup  24735  mbfi1fseqlem3  24787  iblitg  24838  dvnp1  24994  cpncn  25005  dvlip2  25064  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumrlimge0  25099  dvfsumrlim2  25101  ftc1cn  25112  elplyd  25268  ply1termlem  25269  ply1term  25270  ply0  25274  plyeq0lem  25276  plyaddlem1  25279  plymullem1  25280  plyaddlem  25281  plymullem  25282  coeeulem  25290  plyco  25307  coeeq2  25308  coefv0  25314  coemulhi  25320  coemulc  25321  plycj  25343  dvply1  25349  vieta1lem2  25376  elqaalem2  25385  dvtaylp  25434  dvntaylp  25435  taylthlem1  25437  taylth  25439  ulmres  25452  ulmshftlem  25453  ulmshft  25454  ulmcau  25459  ulmdvlem1  25464  mtest  25468  mtestbdd  25469  pserulm  25486  psercn2  25487  psercnlem1  25489  psercn  25490  pserdvlem2  25492  abelthlem6  25500  abelth  25505  efif1olem1  25603  efif1olem3  25605  efif1olem4  25606  logcn  25707  advlogexp  25715  efopn  25718  cxpeq  25815  asinsin  25947  atantayl  25992  leibpilem2  25996  birthdaylem2  26007  birthdaylem3  26008  efrlim  26024  emcllem2  26051  emcllem5  26054  emcllem7  26056  harmonicbnd4  26065  fsumharmonic  26066  lgamgulm2  26090  lgamcvglem  26094  lgamcvg2  26109  gamcvg2lem  26113  wilthlem2  26123  wilthlem3  26124  ftalem1  26127  ftalem2  26128  ftalem3  26129  ftalem5  26131  basellem2  26136  basellem3  26137  basellem5  26139  basellem8  26142  ppiprm  26205  ppinprm  26206  chtprm  26207  chtnprm  26208  chpp1  26209  vma1  26220  ppiltx  26231  musum  26245  0sgmppw  26251  1sgmprm  26252  ppiublem2  26256  chtublem  26264  fsumvma2  26267  chpchtsum  26272  logexprlim  26278  bposlem5  26341  lgscllem  26357  lgsval2lem  26360  lgsval4a  26372  lgsneg  26374  lgsdir2lem3  26380  lgsdir2lem5  26382  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  gausslemma2dlem3  26421  lgseisenlem1  26428  lgsquadlem2  26434  chebbnd1lem1  26522  chtppilimlem1  26526  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasum2lem  26549  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0flb  26563  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  mudivsum  26583  mulogsum  26585  mulog2sumlem2  26588  selberg2lem  26603  logdivbnd  26609  pntrsumo1  26618  pntrsumbnd2  26620  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem6a  26635  pntlemj  26656  pntlemf  26658  ostth2lem3  26688  tglngne  26815  ltgseg  26861  eedimeq  27169  axlowdimlem16  27228  ebtwntg  27253  subgruhgredgd  27554  subumgredg2  27555  umgrres1lem  27580  wlkson  27926  wksonproplem  27974  trlsonfval  27975  pthsonfval  28009  spthson  28010  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  eupth2lems  28503  numclwwlk1lem2foa  28619  numclwlk1lem2  28635  numclwwlk2lem1  28641  htthlem  29180  hhsscms  29541  shmodsi  29652  pjoc1i  29694  5oalem1  29917  mayete3i  29991  adj1  30196  iundisj2f  30830  fmptco1f1o  30869  fcnvgreu  30912  suppovss  30919  ssnnssfz  31010  iundisj2fi  31020  cshw1s2  31134  gsumhashmul  31218  pmtrto1cl  31268  psgnfzto1stlem  31269  fzto1st1  31271  cycpmfv1  31282  cycpmfv2  31283  cycpmco2rn  31294  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cyc3evpm  31319  cyc3genpm  31321  cycpmconjslem2  31324  cyc3conja  31326  rspsnel  31469  nsgmgc  31499  nsgqusf1olem2  31501  idlsrgmulrss1  31558  idlsrgmulrss2  31559  lindsun  31608  fldextfld1  31626  fldextfld2  31627  1smat1  31656  submateqlem2  31660  lmatfval  31666  mdetlap1  31678  madjusmdetlem1  31679  madjusmdetlem2  31680  madjusmdetlem3  31681  madjusmdetlem4  31682  zarclssn  31725  zartopn  31727  zarmxt1  31732  rhmpreimacnlem  31736  rhmpreimacn  31737  pnfneige0  31803  pl1cn  31807  rrhqima  31864  indpreima  31893  esumfzf  31937  esumpcvgval  31946  esumpmono  31947  esumcvg  31954  ldgenpisyslem1  32031  ldgenpisys  32034  measbase  32065  dya2iocnei  32149  oddpwdc  32221  eulerpartlems  32227  eulerpartlemb  32235  sseqf  32259  fibp1  32268  orrvcval4  32331  orrvcoel  32332  orrvccel  32333  ballotlem2  32355  ballotlemfrceq  32395  signsplypnf  32429  signswch  32440  signstf0  32447  signstfvn  32448  signstfvneq0  32451  signstfvcl  32452  signstfveq0  32456  signsvfn  32461  fct2relem  32477  fsum2dsub  32487  reprsuc  32495  reprpmtf1o  32506  breprexplema  32510  breprexplemc  32512  hgt749d  32529  hgt750lemb  32536  tgoldbachgnn  32539  bnj1172  32881  bnj1245  32894  bnj1311  32904  bnj1450  32930  bnj1501  32947  subfacp1lem1  33041  subfacp1lem5  33046  subfacp1lem6  33047  subfacval2  33049  erdszelem7  33059  cvxsconn  33105  cvmliftlem5  33151  cvmliftlem7  33153  cvmliftlem10  33156  cvmliftlem13  33158  mrsubvrs  33384  msubrn  33391  msubco  33393  msubvrs  33422  ttrclse  33713  madebdayim  33997  oldbdayim  33998  imageval  34159  fwddifnp1  34394  knoppcnlem8  34607  knoppcnlem10  34609  bj-unirel  35151  icoreunrn  35457  istoprelowl  35458  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  ftc1cnnc  35776  upixp  35814  sdclem2  35827  caushft  35846  ismtyres  35893  rrnmet  35914  rrndstprj1  35915  rrndstprj2  35916  rrncmslem  35917  rrnequiv  35920  iccbnd  35925  osumcllem7N  37903  pexmidlem4N  37914  lcfrlem4  39486  lcfrlem5  39487  lcfrlem6  39488  lcfrlem16  39499  lcfrlem38  39521  mapdrvallem2  39586  mapdh8ab  39718  mapdh8ad  39720  mapdh8e  39725  3factsumint3  39959  aks4d1p1p1  39999  sticksstones10  40039  metakunt20  40072  mhphf2  40209  prjspnfv01  40382  prjspner01  40383  prjspner1  40384  mapfzcons  40454  diophren  40551  irrapxlem1  40560  monotuz  40679  acongeq  40721  jm2.26lem3  40739  jm3.1lem2  40756  pw2f1ocnv  40775  idomodle  40937  trclfvdecomr  41225  imo72b2lem1  41669  scottelrankd  41754  dvgrat  41819  cvgdvgrat  41820  hashnzfz2  41828  fcnre  42457  refsumcn  42462  rfcnnnub  42468  disjf1o  42618  disjinfi  42620  ssmapsn  42645  ssuzfz  42778  nnsplit  42787  uzssd2  42847  uzublem  42860  fsumsermpt  43010  climsuselem1  43038  limcperiod  43059  sumnnodd  43061  lptioo2cn  43076  lptioo1cn  43077  climresmpt  43090  allbutfifvre  43106  climleltrp  43107  cnrefiisplem  43260  cncfshift  43305  cncfperiod  43310  cncfshiftioo  43323  fperdvper  43350  dvnmptdivc  43369  dvnmul  43374  dvmptfprod  43376  dvnprodlem3  43379  stoweidlem11  43442  stoweidlem15  43446  stoweidlem17  43448  stoweidlem20  43451  stoweidlem34  43465  stoweidlem35  43466  stoweidlem46  43477  stoweidlem47  43478  stoweidlem56  43487  stoweidlem59  43490  stoweidlem62  43493  stirlinglem5  43509  stirlinglem14  43518  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  fourierdlem11  43549  fourierdlem15  43553  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem25  43563  fourierdlem48  43585  fourierdlem52  43589  fourierdlem54  43591  fourierdlem58  43595  fourierdlem62  43599  fourierdlem64  43601  fourierdlem65  43602  fourierdlem69  43606  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem80  43617  fourierdlem81  43618  fourierdlem83  43620  fourierdlem92  43629  fourierdlem93  43630  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  fouriercnp  43657  fouriersw  43662  elaa2lem  43664  etransclem4  43669  etransclem7  43672  etransclem10  43675  etransclem14  43679  etransclem15  43680  etransclem24  43689  etransclem25  43690  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem44  43709  etransclem46  43711  qndenserrnopnlem  43728  qndenserrn  43730  prsal  43749  salgencntex  43772  subsaliuncl  43787  subsalsal  43788  sge0tsms  43808  sge0fodjrnlem  43844  sge0isum  43855  iundjiunlem  43887  iundjiun  43888  meadjiunlem  43893  meaiunlelem  43896  meaiuninclem  43908  meaiininc2  43916  caragensplit  43928  carageneld  43930  carageniuncllem1  43949  caratheodorylem1  43954  caratheodorylem2  43955  hoicvr  43976  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem2  44024  hoiqssbllem2  44051  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  smflimlem3  44195  smfmullem4  44215  smfsupxr  44236  smflimsuplem2  44241  smflimsuplem5  44244  elmod2  44710  ssnn0ssfz  45573  zlmodzxzscm  45581  rmsupp0  45592  lincsum  45658  lincscm  45659  lindslinindimp2lem4  45690  lincresunit3  45710  elbigofrcl  45784  intubeu  46158  unilbeu  46159  postc  46249  setrec1  46283  aacllem  46391