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 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eleqtrrdi  2845  3eltr3g  2850  prid2g  4737  ndmfvrcl  6911  fnwelem  8128  tz7.48-1  8455  brwitnlem  8517  oeeulem  8611  dffi3  9441  cnfcom3lem  9715  ttrclse  9739  alephgeom  10094  fpwwe2lem5  10647  canthwelem  10662  hargch  10685  r1wunlim  10749  eluzel2  12855  fseq1p1m1  13613  fznn0sub2  13650  nn0split  13658  seqp1d  14034  exple1  14193  digit1  14253  bcval5  14334  bcpasc  14337  hashf1  14473  seqcoll  14480  seqcoll2  14481  ccatrn  14605  swrdccat2  14685  cats1un  14737  pfxccatin12lem3  14748  splfv2a  14772  splval2  14773  caubnd  15375  limsupgre  15495  clim2ser  15669  clim2ser2  15670  iserex  15671  isermulc2  15672  iserle  15674  iserge0  15675  climub  15676  climserle  15677  isercolllem2  15680  isercolllem3  15681  isercoll  15682  isercoll2  15683  serf0  15695  iseraltlem2  15697  iseraltlem3  15698  iseralt  15699  sumeq2ii  15707  summolem3  15728  summolem2a  15729  fsum  15734  sum0  15735  fsumcl2lem  15745  fsumadd  15754  isumclim3  15773  isumadd  15781  fsump1i  15783  fsummulc2  15798  fsumrelem  15821  iserabs  15829  cvgcmp  15830  cvgcmpub  15831  cvgcmpce  15832  binom1dif  15847  isumshft  15853  isumsplit  15854  isumrpcl  15857  isumsup2  15860  climcndslem1  15863  climcndslem2  15864  climcnds  15865  arisum2  15875  trireciplem  15876  geoser  15881  pwdif  15882  geolim  15884  geo2lim  15889  cvgrat  15897  mertenslem1  15898  mertenslem2  15899  mertens  15900  clim2prod  15902  clim2div  15903  ntrivcvgfvn0  15913  ntrivcvgtail  15914  prodeq2ii  15925  prodmolem3  15947  prodmolem2a  15948  fprod  15955  fprodntriv  15956  fprodss  15962  fprodser  15963  fprodcl2lem  15964  fprodmul  15974  fproddiv  15975  fprodabs  15988  fprodeq0  15989  fprodn0  15993  iprodclim3  16014  iprodmul  16017  fallfacfwd  16050  0fallfac  16051  binomfallfaclem2  16054  fallfacval4  16057  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  efcvgfsum  16100  efcj  16106  fprodefsum  16109  effsumlt  16127  ruclem7  16252  bitsfzolem  16451  bitsfzo  16452  bitsfi  16454  bitsinv1lem  16458  bitsinv1  16459  bitsinvp1  16466  sadcp1  16472  sadadd  16484  sadass  16488  bitsres  16490  smupp1  16497  smuval2  16499  smupval  16505  smueqlem  16507  smumul  16510  algrp1  16591  phiprmpw  16793  crth  16795  phimullem  16796  eulerthlem2  16799  prmdiv  16802  pcpremul  16861  pcmpt  16910  pcfac  16917  pockthlem  16923  pockthg  16924  prmreclem2  16935  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  prmrec  16940  1arith  16945  vdwapun  16992  vdwlem1  16999  vdwlem2  17000  vdwlem3  17001  vdwlem6  17004  vdwlem8  17006  vdwlem10  17008  vdw  17012  imasvscafn  17549  oppccatid  17729  oppccomfpropd  17737  brcic  17809  funcoppc  17886  invfuc  17988  hofcl  18269  yonedalem4c  18287  gsumwsubmcl  18813  gsumsgrpccat  18816  gsumwmhm  18821  mulgnnp1  19063  mulgnnsubcl  19067  mulgnn0z  19082  mulgnndir  19084  ghmquskerlem1  19264  ghmquskerco  19265  psgnunilem4  19476  psgnran  19494  sylow1lem1  19577  lsmmod2  19655  lsmdisj2r  19664  efginvrel2  19706  efgsdmi  19711  efgsrel  19713  efgs1b  19715  efgsp1  19716  efgredleme  19722  efgredlemc  19724  efgcpbllemb  19734  frgpuplem  19751  mulgnn0di  19804  frgpnabllem1  19852  lt6abl  19874  cycsubgcyg  19880  gsumval3eu  19883  gsumval3  19886  gsumzcl2  19889  gsumzaddlem  19900  gsumconst  19913  gsumzmhm  19916  gsumzoppg  19923  telgsumfz0s  19970  dprdwd  19992  dprd2da  20023  pgpfaclem1  20062  srgbinom  20189  isirred  20377  idomdomd  20684  idomcringd  20685  lspprid2  20953  lspsnat  21104  lsppratlem1  21106  lsppratlem3  21108  lidl0cl  21179  lidlacl  21180  lidlnegcl  21181  elrspsn  21199  2idllidld  21213  2idlridld  21214  rng2idl1cntr  21264  psgnghm  21538  frlmvscavalb  21728  frlmvplusgscavalb  21729  psrbaglefi  21884  psrass23l  21925  psrass23  21927  mplcoe5lem  21995  mpfind  22063  selvval  22071  mhpvscacl  22090  psr1bascl  22134  ply1basf  22136  gsummoncoe1  22244  lply1binom  22246  lply1binomsc  22247  mpfpf1  22287  pf1mpf  22288  evl1scvarpw  22299  evl1maprhm  22315  matbas2i  22358  matecld  22362  matgsum  22373  mpomatmul  22382  dmatmul  22433  1mavmul  22484  mdetleib2  22524  m1detdiag  22533  marep01ma  22596  smadiadetlem4  22605  slesolinv  22616  pmatcollpw3fi1lem1  22722  chpscmat  22778  chpscmatgsumbin  22780  chp0mat  22782  chpidmat  22783  chfacfisf  22790  chfacfisfcpmat  22791  chfacfpmmulgsum2  22801  cldrcl  22962  ordtbas  23128  iscnp2  23175  dis1stc  23435  ptbasfi  23517  ptpjopn  23548  ptclsg  23551  ptcnp  23558  kqtop  23681  reghmph  23729  ptcmplem2  23989  ptcmplem3  23990  ptcmplem4  23991  tsmslem1  24065  utop2nei  24187  isucn2  24215  cuspcvg  24237  cnextucn  24239  imasdsf1olem  24310  blcvx  24735  xrhmeo  24893  cnrehmeo  24900  cnrehmeoOLD  24901  evth  24907  reparphti  24945  reparphtiOLD  24946  iscau4  25229  iscmet3lem1  25241  lmle  25251  rrxfsupp  25352  rrxdsfi  25361  pjthlem2  25388  ovollb2lem  25439  ovolunlem1a  25447  ovoliunlem1  25453  ovoliun2  25457  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem4  25471  iundisj2  25500  voliunlem1  25501  volsup  25507  ioombl1lem4  25512  uniioovol  25530  uniioombllem3  25536  uniioombllem4  25537  uniioombllem6  25539  vitalilem5  25563  mbfimaopnlem  25606  mbflimsup  25617  mbfi1fseqlem3  25668  iblitg  25719  dvcnp2  25871  dvnp1  25877  cpncn  25888  dvmulbr  25891  dvcobr  25899  dvlip2  25950  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumrlimge0  25987  dvfsumrlim2  25989  ftc1cn  26000  elplyd  26157  ply1termlem  26158  ply1term  26159  ply0  26163  plyeq0lem  26165  plyaddlem1  26168  plymullem1  26169  plyaddlem  26170  plymullem  26171  coeeulem  26179  plyco  26196  coeeq2  26197  coefv0  26203  coemulhi  26209  coemulc  26210  plycj  26233  plycjOLD  26235  dvply1  26241  vieta1lem2  26269  elqaalem2  26278  dvtaylp  26328  dvntaylp  26329  taylthlem1  26331  taylth  26334  ulmres  26347  ulmshftlem  26348  ulmshft  26349  ulmcau  26354  ulmdvlem1  26359  mtest  26363  mtestbdd  26364  pserulm  26381  psercn2  26382  psercn2OLD  26383  psercnlem1  26385  psercn  26386  pserdvlem2  26388  abelthlem6  26396  abelth  26401  efif1olem1  26501  efif1olem3  26503  efif1olem4  26504  logcn  26606  advlogexp  26614  efopn  26617  cxpeq  26717  asinsin  26852  atantayl  26897  leibpilem2  26901  birthdaylem2  26912  birthdaylem3  26913  efrlim  26929  efrlimOLD  26930  emcllem2  26957  emcllem5  26960  emcllem7  26962  harmonicbnd4  26971  fsumharmonic  26972  lgamgulm2  26996  lgamcvglem  27000  lgamcvg2  27015  gamcvg2lem  27019  wilthlem2  27029  wilthlem3  27030  ftalem1  27033  ftalem2  27034  ftalem3  27035  ftalem5  27037  basellem2  27042  basellem3  27043  basellem5  27045  basellem8  27048  ppiprm  27111  ppinprm  27112  chtprm  27113  chtnprm  27114  chpp1  27115  vma1  27126  ppiltx  27137  musum  27151  0sgmppw  27159  1sgmprm  27160  ppiublem2  27164  chtublem  27172  fsumvma2  27175  chpchtsum  27180  logexprlim  27186  bposlem5  27249  lgscllem  27265  lgsval2lem  27268  lgsval4a  27280  lgsneg  27282  lgsdir2lem3  27288  lgsdir2lem5  27290  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  gausslemma2dlem3  27329  lgseisenlem1  27336  lgsquadlem2  27342  chebbnd1lem1  27430  chtppilimlem1  27434  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasum2lem  27457  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0flb  27471  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  mudivsum  27491  mulogsum  27493  mulog2sumlem2  27496  selberg2lem  27511  logdivbnd  27517  pntrsumo1  27526  pntrsumbnd2  27528  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem6a  27543  pntlemj  27564  pntlemf  27566  ostth2lem3  27596  madebdayim  27843  oldbdayim  27844  noseqp1  28214  tglngne  28475  ltgseg  28521  eedimeq  28823  axlowdimlem16  28882  ebtwntg  28907  subgruhgredgd  29209  subumgredg2  29210  umgrres1lem  29235  wlkson  29582  wksonproplem  29630  wksonproplemOLD  29631  trlsonfval  29632  pthsonfval  29668  spthson  29669  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  eupth2lems  30165  numclwwlk1lem2foa  30281  numclwlk1lem2  30297  numclwwlk2lem1  30303  htthlem  30844  hhsscms  31205  shmodsi  31316  pjoc1i  31358  5oalem1  31581  mayete3i  31655  adj1  31860  iundisj2f  32517  fmptco1f1o  32557  fcnvgreu  32597  suppovss  32604  ssnnssfz  32710  iundisj2fi  32720  indpreima  32788  ccatws1f1o  32873  cshw1s2  32882  chnccats1  32941  gsumhashmul  33001  gsumwrd2dccat  33007  fzo0pmtrlast  33049  wrdpmtrlast  33050  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st1  33059  cycpmfv1  33070  cycpmfv2  33071  cycpmco2rn  33082  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cyc3evpm  33107  cyc3genpm  33109  cycpmconjslem2  33112  cyc3conja  33114  elrgspnlem1  33183  elrgspnlem2  33184  erler  33206  idomrcanOLD  33222  nsgmgc  33373  nsgqusf1olem2  33375  unitpidl1  33385  elrspunsn  33390  ssdifidllem  33417  mxidlirredi  33432  mxidlirred  33433  opprqusplusg  33450  opprqus0g  33451  opprqusmulr  33452  idlsrgmulrss1  33472  idlsrgmulrss2  33473  rprmcl  33479  rprmdvds  33480  rprmnz  33481  rprmnunit  33482  rprmasso  33486  rprmirredb  33493  pidufd  33504  1arithufdlem2  33506  1arithufdlem3  33507  zringfrac  33515  ply1dg3rt0irred  33541  m1pmeq  33542  ig1pmindeg  33557  exsslsb  33582  ply1degltdimlem  33608  lindsun  33611  fldextfld1  33635  fldextfld2  33636  rtelextdg2  33707  cos9thpiminplylem1  33762  1smat1  33781  submateqlem2  33785  lmatfval  33791  mdetlap1  33803  madjusmdetlem1  33804  madjusmdetlem2  33805  madjusmdetlem3  33806  madjusmdetlem4  33807  zarclssn  33850  zartopn  33852  zarmxt1  33857  rhmpreimacnlem  33861  rhmpreimacn  33862  pnfneige0  33928  pl1cn  33932  rrhqima  33991  esumfzf  34046  esumpcvgval  34055  esumpmono  34056  esumcvg  34063  ldgenpisyslem1  34140  ldgenpisys  34143  measbase  34174  dya2iocnei  34260  oddpwdc  34332  eulerpartlems  34338  eulerpartlemb  34346  sseqf  34370  fibp1  34379  orrvcval4  34443  orrvcoel  34444  orrvccel  34445  ballotlem2  34467  ballotlemfrceq  34507  signsplypnf  34528  signswch  34539  signstf0  34546  signstfvn  34547  signstfvneq0  34550  signstfvcl  34551  signstfveq0  34555  signsvfn  34560  fct2relem  34575  fsum2dsub  34585  reprsuc  34593  reprpmtf1o  34604  breprexplema  34608  breprexplemc  34610  hgt749d  34627  hgt750lemb  34634  tgoldbachgnn  34637  bnj1172  34978  bnj1245  34991  bnj1311  35001  bnj1450  35027  bnj1501  35044  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  subfacval2  35155  erdszelem7  35165  cvxpconn  35210  cvxsconn  35211  cvmliftlem5  35257  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  mrsubvrs  35490  msubrn  35497  msubco  35499  msubvrs  35528  r1peuqusdeg1  35611  imageval  35894  fwddifnp1  36129  knoppcnlem8  36464  knoppcnlem10  36466  bj-unirel  37015  icoreunrn  37323  istoprelowl  37324  poimirlem3  37593  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  mblfinlem2  37628  ftc1cnnc  37662  upixp  37699  sdclem2  37712  caushft  37731  ismtyres  37778  rrnmet  37799  rrndstprj1  37800  rrndstprj2  37801  rrncmslem  37802  rrnequiv  37805  iccbnd  37810  osumcllem7N  39927  pexmidlem4N  39938  lcfrlem4  41510  lcfrlem5  41511  lcfrlem6  41512  lcfrlem16  41523  lcfrlem38  41545  mapdrvallem2  41610  mapdh8ab  41742  mapdh8ad  41744  mapdh8e  41749  3factsumint3  41982  aks4d1p1p1  42022  fldhmf1  42049  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1p8  42074  aks6d1c1  42075  evl1gprodd  42076  idomnnzpownz  42091  aks6d1c5lem1  42095  aks6d1c5lem3  42096  aks6d1c5lem2  42097  deg1gprod  42099  sticksstones10  42114  aks6d1c6lem3  42131  aks5lem2  42146  aks5lem3a  42148  unitscyglem5  42158  metakunt20  42183  fz1sump1  42306  sumcubes  42309  evlselv  42557  mhphf2  42568  prjspnfv01  42594  prjspner01  42595  prjspner1  42596  mapfzcons  42686  diophren  42783  irrapxlem1  42792  monotuz  42912  acongeq  42954  jm2.26lem3  42972  jm3.1lem2  42989  pw2f1ocnv  43008  idomodle  43162  trclfvdecomr  43699  imo72b2lem0  44136  imo72b2lem1  44140  scottelrankd  44219  dvgrat  44284  cvgdvgrat  44285  hashnzfz2  44293  fcnre  44997  refsumcn  45002  rfcnnnub  45008  disjf1o  45163  disjinfi  45164  ssmapsn  45188  ssuzfz  45324  nnsplit  45333  uzssd2  45392  uzublem  45405  fsumsermpt  45556  climsuselem1  45584  limcperiod  45605  sumnnodd  45607  lptioo2cn  45622  lptioo1cn  45623  climresmpt  45636  allbutfifvre  45652  climleltrp  45653  cnrefiisplem  45806  cncfshift  45851  cncfperiod  45856  cncfshiftioo  45869  fperdvper  45896  dvnmptdivc  45915  dvnmul  45920  dvmptfprod  45922  dvnprodlem3  45925  stoweidlem11  45988  stoweidlem15  45992  stoweidlem17  45994  stoweidlem20  45997  stoweidlem34  46011  stoweidlem35  46012  stoweidlem46  46023  stoweidlem47  46024  stoweidlem56  46033  stoweidlem59  46036  stoweidlem62  46039  stirlinglem5  46055  stirlinglem14  46064  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  fourierdlem11  46095  fourierdlem15  46099  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem25  46109  fourierdlem48  46131  fourierdlem52  46135  fourierdlem54  46137  fourierdlem58  46141  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem69  46152  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem80  46163  fourierdlem81  46164  fourierdlem83  46166  fourierdlem92  46175  fourierdlem93  46176  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem113  46196  fouriercnp  46203  fouriersw  46208  elaa2lem  46210  etransclem4  46215  etransclem7  46218  etransclem10  46221  etransclem14  46225  etransclem15  46226  etransclem24  46235  etransclem25  46236  etransclem31  46242  etransclem32  46243  etransclem35  46246  etransclem44  46255  etransclem46  46257  qndenserrnopnlem  46274  qndenserrn  46276  prsal  46295  salgencntex  46320  subsaliuncl  46335  subsalsal  46336  sge0tsms  46357  sge0fodjrnlem  46393  sge0isum  46404  iundjiunlem  46436  iundjiun  46437  meadjiunlem  46442  meaiunlelem  46445  meaiuninclem  46457  meaiininc2  46465  caragensplit  46477  carageneld  46479  carageniuncllem1  46498  caratheodorylem1  46503  caratheodorylem2  46504  hoicvr  46525  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmvlelem2  46573  hoiqssbllem2  46600  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  smflimlem3  46750  smfmullem4  46771  smfsupxr  46793  smflimsuplem2  46798  smflimsuplem5  46801  ormklocald  46851  natlocalincr  46853  elmod2  47332  isuspgrim0lem  47854  upgrimtrlslem2  47866  ssnn0ssfz  48272  zlmodzxzscm  48280  rmsupp0  48291  lincsum  48353  lincscm  48354  lindslinindimp2lem4  48385  lincresunit3  48405  elbigofrcl  48478  intubeu  48906  unilbeu  48907  cicrcl2  48958  cic1st2nd  48962  imaf1homlem  49014  oppfrcl  49024  imasubc  49039  imaid  49042  oppcuprcl5  49082  oppcup3  49090  elxpcbasex1ALT  49114  elxpcbasex2ALT  49116  swapf1a  49134  swapf2f1oa  49142  swapfida  49145  cofuswapf1  49153  cofuswapf2  49154  postc  49394  reldmlan2  49440  reldmran2  49441  lanrcl  49444  ranrcl  49445  setrec1  49503  aacllem  49613