Theorem eleqtrdi 2875

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  eleqtrrdi  2876  3eltr3g  2881  prid2g  4729  ndmfvrcl  6918  fnwelem  8133  tz7.48-1  8436  brwitnlem  8498  oeeulem  8593  dffi3  9398  cnfcom3lem  9679  ttrclse  9703  scottelrankd  9884  alephgeom  10082  fpwwe2lem5  10639  canthwelem  10654  hargch  10677  r1wunlim  10741  eluzel2  12887  fseq1p1m1  13647  fznn0sub2  13684  nn0split  13692  seqp1d  14076  exple1  14235  digit1  14295  bcval5  14376  bcpasc  14379  hashf1  14516  seqcoll  14523  seqcoll2  14524  ccatrn  14649  swrdccat2  14733  cats1un  14784  pfxccatin12lem3  14795  splfv2a  14819  splval2  14820  caubnd  15438  limsupgre  15560  clim2ser  15734  clim2ser2  15735  iserex  15736  isermulc2  15737  iserle  15739  iserge0  15740  climub  15741  climserle  15742  isercolllem2  15745  isercolllem3  15746  isercoll  15747  isercoll2  15748  serf0  15760  iseraltlem2  15762  iseraltlem3  15763  iseralt  15764  sumeq2ii  15772  summolem3  15792  summolem2a  15793  fsum  15798  sum0  15799  fsumcl2lem  15809  fsumadd  15818  isumclim3  15837  isumadd  15845  fsump1i  15847  fsummulc2  15862  fsumrelem  15886  iserabs  15894  cvgcmp  15895  cvgcmpub  15896  cvgcmpce  15897  binom1dif  15914  isumshft  15920  isumsplit  15921  isumrpcl  15924  isumsup2  15927  climcndslem1  15930  climcndslem2  15931  climcnds  15932  arisum2  15942  trireciplem  15943  geoser  15948  pwdif  15949  geolim  15951  geo2lim  15956  cvgrat  15964  mertenslem1  15965  mertenslem2  15966  mertens  15967  clim2prod  15969  clim2div  15970  ntrivcvgfvn0  15980  ntrivcvgtail  15981  prodeq2ii  15992  prodmolem3  16014  prodmolem2a  16015  fprod  16022  fprodntriv  16023  fprodss  16029  fprodser  16030  fprodcl2lem  16031  fprodmul  16041  fproddiv  16042  fprodabs  16055  fprodeq0  16056  fprodn0  16060  iprodclim3  16081  iprodmul  16084  fallfacfwd  16116  0fallfac  16117  binomfallfaclem2  16120  fallfacval4  16123  bpolysum  16133  bpolydiflem  16134  fsumkthpow  16136  efcvgfsum  16166  efcj  16172  fprodefsum  16175  effsumlt  16193  ruclem7  16318  bitsfzolem  16518  bitsfzo  16519  bitsfi  16521  bitsinv1lem  16525  bitsinv1  16526  bitsinvp1  16533  sadcp1  16539  sadadd  16551  sadass  16555  bitsres  16557  smupp1  16564  smuval2  16566  smupval  16572  smueqlem  16574  smumul  16577  algrp1  16658  phiprmpw  16861  crth  16863  phimullem  16864  eulerthlem2  16867  prmdiv  16870  pcpremul  16929  pcmpt  16978  pcfac  16985  pockthlem  16991  pockthg  16992  prmreclem2  17003  prmreclem3  17004  prmreclem4  17005  prmreclem5  17006  prmreclem6  17007  prmrec  17008  1arith  17013  vdwapun  17060  vdwlem1  17067  vdwlem2  17068  vdwlem3  17069  vdwlem6  17072  vdwlem8  17074  vdwlem10  17076  vdw  17080  imasvscafn  17617  oppccatid  17801  oppccomfpropd  17809  brcic  17881  funcoppc  17958  invfuc  18060  hofcl  18341  yonedalem4c  18359  chnccats1  18707  gsumwsubmcl  18937  gsumsgrpccat  18940  gsumwmhm  18945  mulgnnp1  19196  mulgnnsubcl  19200  mulgnn0z  19215  mulgnndir  19217  ghmquskerlem1  19401  ghmquskerco  19402  psgnunilem4  19615  psgnran  19633  sylow1lem1  19716  lsmmod2  19794  lsmdisj2r  19803  efginvrel2  19845  efgsdmi  19850  efgsrel  19852  efgs1b  19854  efgsp1  19855  efgredleme  19861  efgredlemc  19863  efgcpbllemb  19873  frgpuplem  19890  mulgnn0di  19943  frgpnabllem1  19991  lt6abl  20013  cycsubgcyg  20019  gsumval3eu  20022  gsumval3  20025  gsumzcl2  20028  gsumzaddlem  20039  gsumconst  20052  gsumzmhm  20055  gsumzoppg  20062  telgsumfz0s  20109  dprdwd  20131  dprd2da  20162  pgpfaclem1  20201  srgbinom  20361  isirred  20551  idomdomd  20878  idomcringd  20879  lspprid2  21173  lspsnat  21323  lsppratlem1  21325  lsppratlem3  21327  lidl0cl  21399  lidlacl  21400  lidlnegcl  21401  elrspsn  21425  2idllidld  21447  2idlridld  21448  rng2idl1cntr  21499  ssdifidllem  21538  psgnghm  21784  frlmvscavalb  21974  frlmvplusgscavalb  21975  psrbaglefi  22130  psrass23l  22170  psrass23  22172  mplcoe5lem  22244  mpfind  22320  selvval  22325  mhpvscacl  22371  psr1bascl  22414  ply1basf  22416  gsummoncoe1  22522  lply1binom  22524  lply1binomsc  22525  mpfpf1  22565  pf1mpf  22566  evl1scvarpw  22577  evl1maprhm  22593  matbas2i  22633  matecld  22637  matgsum  22648  mpomatmul  22657  dmatmul  22708  1mavmul  22759  mdetleib2  22799  m1detdiag  22808  marep01ma  22871  smadiadetlem4  22880  slesolinv  22891  pmatcollpw3fi1lem1  22997  chpscmat  23053  chpscmatgsumbin  23055  chp0mat  23057  chpidmat  23058  chfacfisf  23065  chfacfisfcpmat  23066  chfacfpmmulgsum2  23076  cldrcl  23237  ordtbas  23403  iscnp2  23450  dis1stc  23711  ptbasfi  23793  ptpjopn  23824  ptclsg  23827  ptcnp  23834  kqtop  23957  reghmph  24005  ptcmplem2  24265  ptcmplem3  24266  ptcmplem4  24267  tsmslem1  24341  utop2nei  24462  isucn2  24490  cuspcvg  24512  cnextucn  24514  imasdsf1olem  24585  blcvx  25010  xrhmeo  25160  cnrehmeo  25167  evth  25173  reparphti  25211  iscau4  25493  iscmet3lem1  25505  lmle  25515  rrxfsupp  25616  rrxdsfi  25625  pjthlem2  25652  ovollb2lem  25702  ovolunlem1a  25710  ovoliunlem1  25716  ovoliun2  25720  ovolscalem1  25727  ovolicc1  25730  ovolicc2lem4  25734  iundisj2  25763  voliunlem1  25764  volsup  25770  ioombl1lem4  25775  uniioovol  25793  uniioombllem3  25799  uniioombllem4  25800  uniioombllem6  25802  vitalilem5  25826  mbfimaopnlem  25869  mbflimsup  25880  mbfi1fseqlem3  25931  iblitg  25982  dvcnp2  26134  dvnp1  26139  cpncn  26150  dvmulbr  26153  dvcobr  26160  dvlip2  26209  dvfsumlem2  26241  dvfsumlem3  26242  dvfsumrlimge0  26244  dvfsumrlim2  26246  ftc1cn  26257  elplyd  26414  ply1termlem  26415  ply1term  26416  ply0  26420  plyeq0lem  26422  plyaddlem1  26425  plymullem1  26426  plyaddlem  26427  plymullem  26428  coeeulem  26436  plyco  26453  coeeq2  26454  coefv0  26460  coemulhi  26466  coemulc  26467  plycj  26489  plycjOLD  26491  dvply1  26500  vieta1lem2  26527  elqaalem2  26536  dvtaylp  26588  dvntaylp  26589  taylthlem1  26591  taylth  26593  ulmres  26606  ulmshftlem  26607  ulmshft  26608  ulmcau  26613  ulmdvlem1  26618  mtest  26622  mtestbdd  26623  pserulm  26640  psercn2  26641  psercnlem1  26643  psercn  26644  pserdvlem2  26646  abelthlem6  26654  abelth  26659  efif1olem1  26762  efif1olem3  26764  efif1olem4  26765  logcn  26867  advlogexp  26875  efopn  26878  cxpeq  26977  asinsin  27112  atantayl  27157  leibpilem2  27161  birthdaylem2  27172  birthdaylem3  27173  efrlim  27189  emcllem2  27216  emcllem5  27219  emcllem7  27221  harmonicbnd4  27230  fsumharmonic  27231  lgamgulm2  27255  lgamcvglem  27259  lgamcvg2  27274  gamcvg2lem  27278  wilthlem2  27288  wilthlem3  27289  ftalem1  27292  ftalem2  27293  ftalem3  27294  ftalem5  27296  basellem2  27301  basellem3  27302  basellem5  27304  basellem8  27307  ppiprm  27370  ppinprm  27371  chtprm  27372  chtnprm  27373  chpp1  27374  vma1  27385  ppiltx  27396  musum  27410  0sgmppw  27417  1sgmprm  27418  ppiublem2  27422  chtublem  27430  fsumvma2  27433  chpchtsum  27438  logexprlim  27444  bposlem5  27507  lgscllem  27523  lgsval2lem  27526  lgsval4a  27538  lgsneg  27540  lgsdir2lem3  27546  lgsdir2lem5  27548  lgsdir  27551  lgsdilem2  27552  lgsdi  27553  lgsne0  27554  gausslemma2dlem3  27587  lgseisenlem1  27594  lgsquadlem2  27600  chebbnd1lem1  27688  chtppilimlem1  27692  rplogsumlem2  27704  rpvmasumlem  27706  dchrisumlem1  27708  dchrisumlem2  27709  dchrmusum2  27713  dchrvmasum2lem  27715  dchrvmasumiflem1  27720  dchrisum0flblem1  27727  dchrisum0flblem2  27728  dchrisum0flb  27729  dchrisum0re  27732  dchrisum0lem1b  27734  dchrisum0lem1  27735  dchrisum0lem2a  27736  dchrisum0lem2  27737  dchrisum0lem3  27738  mudivsum  27749  mulogsum  27751  mulog2sumlem2  27754  selberg2lem  27769  logdivbnd  27775  pntrsumo1  27784  pntrsumbnd2  27786  pntrlog2bndlem2  27797  pntrlog2bndlem4  27799  pntrlog2bndlem6a  27801  pntlemj  27822  pntlemf  27824  ostth2lem3  27854  madebdayim  28136  oldbdayim  28137  newbdayim  28151  cutminmax  28184  noseqp1  28539  tglngne  28874  ltgseg  28920  eedimeq  29307  axlowdimlem16  29366  ebtwntg  29391  subgruhgredgd  29696  subumgredg2  29697  umgrres1lem  29722  wlkson  30066  wksonproplem  30118  trlsonfval  30119  pthsonfval  30157  spthson  30158  crctcshwlkn0lem4  30233  crctcshwlkn0lem5  30234  eupth2lems  30664  numclwwlk1lem2foa  30780  numclwlk1lem2  30796  numclwwlk2lem1  30802  htthlem  31344  hhsscms  31705  shmodsi  31816  pjoc1i  31858  5oalem1  32081  mayete3i  32155  adj1  32360  iundisj2f  33010  fmptco1f1o  33053  fcnvgreu  33092  suppovss  33101  ssnnssfz  33206  nn0diffz0  33213  iundisj2fi  33216  indpreima  33259  ccatws1f1o  33341  cshw1s2  33348  gsumhashmul  33455  gsummulsubdishift1  33456  gsumwrd2dccat  33466  fzo0pmtrlast  33480  wrdpmtrlast  33481  pmtrto1cl  33487  psgnfzto1stlem  33488  fzto1st1  33490  cycpmfv1  33501  cycpmfv2  33502  cycpmco2rn  33513  cycpmco2lem4  33517  cycpmco2lem5  33518  cycpmco2lem6  33519  cyc3evpm  33538  cyc3genpm  33540  cycpmconjslem2  33543  cyc3conja  33545  elrgspnlem1  33630  elrgspnlem2  33631  erler  33653  nsgmgc  33789  nsgqusf1olem2  33791  unitpidl1  33800  elrspunsn  33805  mxidlirredi  33822  mxidlirred  33823  opprqusplusg  33839  opprqus0g  33840  opprqusmulr  33841  idlsrgmulrss1  33869  idlsrgmulrss2  33870  rprmcl  33876  rprmdvds  33877  rprmnz  33878  rprmnunit  33879  rprmasso  33883  rprmirredb  33890  pidufd  33901  1arithufdlem2  33903  1arithufdlem3  33904  zringfrac  33912  ply1dg3rt0irred  33942  m1pmeq  33943  ig1pmindeg  33960  selvply1rhmlem2  33979  selvply1rhmlem4  33981  selvply1rhm0  33984  extvfvvcl  33993  evlextv  34000  psrmonprod  34010  esplysply  34029  esplyind  34033  esplyfvn  34035  vietalem  34037  exsslsb  34055  ply1degltdimlem  34080  lindsun  34083  fldextfld1  34105  fldextfld2  34106  rtelextdg2  34185  cos9thpiminplylem1  34240  1smat1  34262  submateqlem2  34266  lmatfval  34272  mdetlap1  34284  madjusmdetlem1  34285  madjusmdetlem2  34286  madjusmdetlem3  34287  madjusmdetlem4  34288  zarclssn  34331  zartopn  34333  zarmxt1  34338  rhmpreimacnlem  34342  rhmpreimacn  34343  pnfneige0  34409  pl1cn  34413  rrhqima  34472  esumfzf  34527  esumpcvgval  34536  esumpmono  34537  esumcvg  34544  ldgenpisyslem1  34622  ldgenpisys  34625  measbase  34656  dya2iocnei  34741  oddpwdc  34813  eulerpartlems  34819  eulerpartlemb  34827  sseqf  34851  fibp1  34860  orrvcval4  34924  orrvcoel  34925  orrvccel  34926  ballotlem2  34948  ballotlemfrceq  34988  signsplypnf  35006  signswch  35017  signstf0  35024  signstfvn  35025  signstfvneq0  35028  signstfvcl  35029  signstfveq0  35033  signsvfn  35038  fct2relem  35053  fsum2dsub  35063  reprsuc  35071  reprpmtf1o  35082  breprexplema  35086  breprexplemc  35088  hgt749d  35105  hgt750lemb  35112  tgoldbachgnn  35115  bnj1172  35458  bnj1245  35471  bnj1311  35481  bnj1450  35507  bnj1501  35524  r1elcl  35553  subfacp1lem1  35712  subfacp1lem5  35717  subfacp1lem6  35718  subfacval2  35720  erdszelem7  35730  cvxpconn  35775  cvxsconn  35776  cvmliftlem5  35822  cvmliftlem7  35824  cvmliftlem10  35827  cvmliftlem13  35829  mrsubvrs  36055  msubrn  36062  msubco  36064  msubvrs  36093  r1peuqusdeg1  36176  imageval  36461  fwddifnp1  36698  knoppcnlem8  37150  knoppcnlem10  37152  bj-unirel  37748  icoreunrn  38066  istoprelowl  38067  poimirlem3  38335  poimirlem4  38336  poimirlem6  38338  poimirlem7  38339  poimirlem8  38340  poimirlem12  38344  poimirlem15  38347  poimirlem16  38348  poimirlem17  38349  poimirlem18  38350  poimirlem19  38351  poimirlem20  38352  poimirlem21  38353  poimirlem22  38354  poimirlem23  38355  poimirlem24  38356  poimirlem25  38357  poimirlem26  38358  poimirlem27  38359  poimirlem28  38360  poimirlem29  38361  poimirlem31  38363  mblfinlem2  38370  ftc1cnnc  38404  upixp  38442  sdclem2  38455  caushft  38474  ismtyres  38521  rrnmet  38542  rrndstprj1  38543  rrndstprj2  38544  rrncmslem  38545  rrnequiv  38548  iccbnd  38553  osumcllem7N  40798  pexmidlem4N  40809  lcfrlem4  42381  lcfrlem5  42382  lcfrlem6  42383  lcfrlem16  42394  lcfrlem38  42416  mapdrvallem2  42481  mapdh8ab  42613  mapdh8ad  42615  mapdh8e  42620  3factsumint3  42852  aks4d1p1p1  42892  fldhmf1  42919  aks6d1c1p2  42938  aks6d1c1p3  42939  aks6d1c1p7  42942  aks6d1c1p6  42943  aks6d1c1p8  42944  aks6d1c1  42945  evl1gprodd  42946  idomnnzpownz  42961  aks6d1c5lem1  42965  aks6d1c5lem3  42966  aks6d1c5lem2  42967  deg1gprod  42969  sticksstones10  42984  aks6d1c6lem3  43001  aks5lem2  43016  aks5lem3a  43018  unitscyglem5  43028  fz1sump1  43148  sumcubes  43151  evlselv  43398  mhphf2  43407  prjspnfv01  43433  prjspner01  43434  prjspner1  43435  mapfzcons  43524  diophren  43617  irrapxlem1  43626  monotuz  43745  acongeq  43787  jm2.26lem3  43805  jm3.1lem2  43822  pw2f1ocnv  43841  idomodle  43995  trclfvdecomr  44531  imo72b2lem0  44968  imo72b2lem1  44972  dvgrat  45099  cvgdvgrat  45100  hashnzfz2  45108  fcnre  45822  refsumcn  45827  rfcnnnub  45833  disjf1o  45986  disjinfi  45987  ssmapsn  46009  ssuzfz  46142  nnsplit  46151  uzssd2  46208  uzublem  46221  fsumsermpt  46372  climsuselem1  46400  limcperiod  46421  sumnnodd  46423  lptioo2cn  46436  lptioo1cn  46437  climresmpt  46450  allbutfifvre  46466  climleltrp  46467  cnrefiisplem  46620  cncfshift  46665  cncfperiod  46670  cncfshiftioo  46683  fperdvper  46710  dvnmptdivc  46729  dvnmul  46734  dvmptfprod  46736  dvnprodlem3  46739  stoweidlem11  46802  stoweidlem15  46806  stoweidlem17  46808  stoweidlem20  46811  stoweidlem34  46825  stoweidlem35  46826  stoweidlem46  46837  stoweidlem47  46838  stoweidlem56  46847  stoweidlem59  46850  stoweidlem62  46853  stirlinglem5  46869  stirlinglem14  46878  dirkertrigeqlem2  46890  dirkertrigeqlem3  46891  fourierdlem11  46909  fourierdlem15  46913  fourierdlem16  46914  fourierdlem21  46919  fourierdlem22  46920  fourierdlem25  46923  fourierdlem48  46945  fourierdlem49  46946  fourierdlem52  46949  fourierdlem54  46951  fourierdlem58  46955  fourierdlem62  46959  fourierdlem64  46961  fourierdlem65  46962  fourierdlem69  46966  fourierdlem70  46967  fourierdlem71  46968  fourierdlem73  46970  fourierdlem80  46977  fourierdlem81  46978  fourierdlem83  46980  fourierdlem92  46989  fourierdlem93  46990  fourierdlem97  46994  fourierdlem103  47000  fourierdlem104  47001  fourierdlem112  47009  fourierdlem113  47010  fouriercnp  47017  fouriersw  47022  elaa2lem  47024  etransclem4  47029  etransclem7  47032  etransclem10  47035  etransclem14  47039  etransclem15  47040  etransclem24  47049  etransclem25  47050  etransclem31  47056  etransclem32  47057  etransclem35  47060  etransclem44  47069  etransclem46  47071  qndenserrnopnlem  47088  qndenserrn  47090  prsal  47109  salgencntex  47134  subsaliuncl  47149  subsalsal  47150  sge0tsms  47171  sge0fodjrnlem  47207  sge0isum  47218  iundjiunlem  47250  iundjiun  47251  meadjiunlem  47256  meaiunlelem  47259  meaiuninclem  47271  meaiininc2  47279  caragensplit  47291  carageneld  47293  carageniuncllem1  47312  caratheodorylem1  47317  caratheodorylem2  47318  hoicvr  47339  hsphoidmvle2  47376  hsphoidmvle  47377  hoidmv1lelem2  47383  hoidmv1lelem3  47384  hoidmvlelem2  47387  hoiqssbllem2  47414  pimdecfgtioc  47506  pimincfltioc  47507  pimdecfgtioo  47508  pimincfltioo  47509  smflimlem3  47564  smfmullem4  47585  smfsupxr  47607  smflimsuplem2  47612  smflimsuplem5  47615  ormklocald  47667  natlocalincr  47669  elmod2  48175  isuspgrim0lem  48735  upgrimtrlslem2  48747  ssnn0ssfz  49205  zlmodzxzscm  49213  rmsupp0  49224  lincsum  49285  lincscm  49286  lindslinindimp2lem4  49317  lincresunit3  49337  elbigofrcl  49406  intubeu  49838  unilbeu  49839  cicrcl2  49897  cic1st2nd  49901  imaf1homlem  49961  oppfrcl  49982  eloppf  49987  imasubc  50005  imaid  50008  oppcuprcl5  50055  oppcup3  50063  uptrlem2  50065  uptrlem3  50066  natoppf  50083  elxpcbasex1ALT  50103  elxpcbasex2ALT  50105  swapf1a  50123  swapf2f1oa  50131  swapfida  50134  cofuswapf1  50148  cofuswapf2  50149  fucoppcco  50263  postc  50423  reldmlan2  50471  reldmran2  50472  lanrcl  50475  ranrcl  50476  setrec1  50545  aacllem  50697  crosspaltd  50724  crossp3d  50725