Theorem eleqtrdi 2872

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837

This theorem is used by:  eleqtrrdi  2873  3eltr3g  2878  prid2g  4726  ndmfvrcl  6914  fnwelem  8125  tz7.48-1  8428  brwitnlem  8490  oeeulem  8585  dffi3  9389  cnfcom3lem  9670  ttrclse  9694  scottelrankd  9875  alephgeom  10073  fpwwe2lem5  10626  canthwelem  10641  hargch  10664  r1wunlim  10728  eluzel2  12873  fseq1p1m1  13633  fznn0sub2  13670  nn0split  13678  seqp1d  14061  exple1  14220  digit1  14280  bcval5  14361  bcpasc  14364  hashf1  14501  seqcoll  14508  seqcoll2  14509  ccatrn  14634  swrdccat2  14714  cats1un  14765  pfxccatin12lem3  14776  splfv2a  14800  splval2  14801  caubnd  15417  limsupgre  15539  clim2ser  15713  clim2ser2  15714  iserex  15715  isermulc2  15716  iserle  15718  iserge0  15719  climub  15720  climserle  15721  isercolllem2  15724  isercolllem3  15725  isercoll  15726  isercoll2  15727  serf0  15739  iseraltlem2  15741  iseraltlem3  15742  iseralt  15743  sumeq2ii  15751  summolem3  15772  summolem2a  15773  fsum  15778  sum0  15779  fsumcl2lem  15789  fsumadd  15798  isumclim3  15817  isumadd  15825  fsump1i  15827  fsummulc2  15842  fsumrelem  15866  iserabs  15874  cvgcmp  15875  cvgcmpub  15876  cvgcmpce  15877  binom1dif  15894  isumshft  15900  isumsplit  15901  isumrpcl  15904  isumsup2  15907  climcndslem1  15910  climcndslem2  15911  climcnds  15912  arisum2  15922  trireciplem  15923  geoser  15928  pwdif  15929  geolim  15931  geo2lim  15936  cvgrat  15944  mertenslem1  15945  mertenslem2  15946  mertens  15947  clim2prod  15949  clim2div  15950  ntrivcvgfvn0  15960  ntrivcvgtail  15961  prodeq2ii  15972  prodmolem3  15994  prodmolem2a  15995  fprod  16002  fprodntriv  16003  fprodss  16009  fprodser  16010  fprodcl2lem  16011  fprodmul  16021  fproddiv  16022  fprodabs  16035  fprodeq0  16036  fprodn0  16040  iprodclim3  16061  iprodmul  16064  fallfacfwd  16096  0fallfac  16097  binomfallfaclem2  16100  fallfacval4  16103  bpolysum  16113  bpolydiflem  16114  fsumkthpow  16116  efcvgfsum  16146  efcj  16152  fprodefsum  16155  effsumlt  16173  ruclem7  16298  bitsfzolem  16498  bitsfzo  16499  bitsfi  16501  bitsinv1lem  16505  bitsinv1  16506  bitsinvp1  16513  sadcp1  16519  sadadd  16531  sadass  16535  bitsres  16537  smupp1  16544  smuval2  16546  smupval  16552  smueqlem  16554  smumul  16557  algrp1  16638  phiprmpw  16841  crth  16843  phimullem  16844  eulerthlem2  16847  prmdiv  16850  pcpremul  16909  pcmpt  16958  pcfac  16965  pockthlem  16971  pockthg  16972  prmreclem2  16983  prmreclem3  16984  prmreclem4  16985  prmreclem5  16986  prmreclem6  16987  prmrec  16988  1arith  16993  vdwapun  17040  vdwlem1  17047  vdwlem2  17048  vdwlem3  17049  vdwlem6  17052  vdwlem8  17054  vdwlem10  17056  vdw  17060  imasvscafn  17597  oppccatid  17781  oppccomfpropd  17789  brcic  17861  funcoppc  17938  invfuc  18040  hofcl  18321  yonedalem4c  18339  chnccats1  18687  gsumwsubmcl  18902  gsumsgrpccat  18905  gsumwmhm  18910  mulgnnp1  19154  mulgnnsubcl  19158  mulgnn0z  19173  mulgnndir  19175  ghmquskerlem1  19359  ghmquskerco  19360  psgnunilem4  19573  psgnran  19591  sylow1lem1  19674  lsmmod2  19752  lsmdisj2r  19761  efginvrel2  19803  efgsdmi  19808  efgsrel  19810  efgs1b  19812  efgsp1  19813  efgredleme  19819  efgredlemc  19821  efgcpbllemb  19831  frgpuplem  19848  mulgnn0di  19901  frgpnabllem1  19949  lt6abl  19971  cycsubgcyg  19977  gsumval3eu  19980  gsumval3  19983  gsumzcl2  19986  gsumzaddlem  19997  gsumconst  20010  gsumzmhm  20013  gsumzoppg  20020  telgsumfz0s  20067  dprdwd  20089  dprd2da  20120  pgpfaclem1  20159  srgbinom  20319  isirred  20508  idomdomd  20835  idomcringd  20836  lspprid2  21130  lspsnat  21280  lsppratlem1  21282  lsppratlem3  21284  lidl0cl  21356  lidlacl  21357  lidlnegcl  21358  elrspsn  21382  2idllidld  21404  2idlridld  21405  rng2idl1cntr  21456  ssdifidllem  21495  psgnghm  21741  frlmvscavalb  21931  frlmvplusgscavalb  21932  psrbaglefi  22087  psrass23l  22127  psrass23  22129  mplcoe5lem  22201  mpfind  22277  selvval  22282  mhpvscacl  22328  psr1bascl  22371  ply1basf  22373  gsummoncoe1  22479  lply1binom  22481  lply1binomsc  22482  mpfpf1  22522  pf1mpf  22523  evl1scvarpw  22534  evl1maprhm  22550  matbas2i  22590  matecld  22594  matgsum  22605  mpomatmul  22614  dmatmul  22665  1mavmul  22716  mdetleib2  22756  m1detdiag  22765  marep01ma  22828  smadiadetlem4  22837  slesolinv  22848  pmatcollpw3fi1lem1  22954  chpscmat  23010  chpscmatgsumbin  23012  chp0mat  23014  chpidmat  23015  chfacfisf  23022  chfacfisfcpmat  23023  chfacfpmmulgsum2  23033  cldrcl  23194  ordtbas  23360  iscnp2  23407  dis1stc  23667  ptbasfi  23749  ptpjopn  23780  ptclsg  23783  ptcnp  23790  kqtop  23913  reghmph  23961  ptcmplem2  24221  ptcmplem3  24222  ptcmplem4  24223  tsmslem1  24297  utop2nei  24418  isucn2  24446  cuspcvg  24468  cnextucn  24470  imasdsf1olem  24541  blcvx  24966  xrhmeo  25116  cnrehmeo  25123  evth  25129  reparphti  25167  iscau4  25449  iscmet3lem1  25461  lmle  25471  rrxfsupp  25572  rrxdsfi  25581  pjthlem2  25608  ovollb2lem  25658  ovolunlem1a  25666  ovoliunlem1  25672  ovoliun2  25676  ovolscalem1  25683  ovolicc1  25686  ovolicc2lem4  25690  iundisj2  25719  voliunlem1  25720  volsup  25726  ioombl1lem4  25731  uniioovol  25749  uniioombllem3  25755  uniioombllem4  25756  uniioombllem6  25758  vitalilem5  25782  mbfimaopnlem  25825  mbflimsup  25836  mbfi1fseqlem3  25887  iblitg  25938  dvcnp2  26090  dvnp1  26095  cpncn  26106  dvmulbr  26109  dvcobr  26116  dvlip2  26165  dvfsumlem2  26197  dvfsumlem3  26198  dvfsumrlimge0  26200  dvfsumrlim2  26202  ftc1cn  26213  elplyd  26370  ply1termlem  26371  ply1term  26372  ply0  26376  plyeq0lem  26378  plyaddlem1  26381  plymullem1  26382  plyaddlem  26383  plymullem  26384  coeeulem  26392  plyco  26409  coeeq2  26410  coefv0  26416  coemulhi  26422  coemulc  26423  plycj  26445  plycjOLD  26447  dvply1  26456  vieta1lem2  26483  elqaalem2  26492  dvtaylp  26544  dvntaylp  26545  taylthlem1  26547  taylth  26549  ulmres  26562  ulmshftlem  26563  ulmshft  26564  ulmcau  26569  ulmdvlem1  26574  mtest  26578  mtestbdd  26579  pserulm  26596  psercn2  26597  psercnlem1  26599  psercn  26600  pserdvlem2  26602  abelthlem6  26610  abelth  26615  efif1olem1  26718  efif1olem3  26720  efif1olem4  26721  logcn  26823  advlogexp  26831  efopn  26834  cxpeq  26933  asinsin  27068  atantayl  27113  leibpilem2  27117  birthdaylem2  27128  birthdaylem3  27129  efrlim  27145  emcllem2  27172  emcllem5  27175  emcllem7  27177  harmonicbnd4  27186  fsumharmonic  27187  lgamgulm2  27211  lgamcvglem  27215  lgamcvg2  27230  gamcvg2lem  27234  wilthlem2  27244  wilthlem3  27245  ftalem1  27248  ftalem2  27249  ftalem3  27250  ftalem5  27252  basellem2  27257  basellem3  27258  basellem5  27260  basellem8  27263  ppiprm  27326  ppinprm  27327  chtprm  27328  chtnprm  27329  chpp1  27330  vma1  27341  ppiltx  27352  musum  27366  0sgmppw  27373  1sgmprm  27374  ppiublem2  27378  chtublem  27386  fsumvma2  27389  chpchtsum  27394  logexprlim  27400  bposlem5  27463  lgscllem  27479  lgsval2lem  27482  lgsval4a  27494  lgsneg  27496  lgsdir2lem3  27502  lgsdir2lem5  27504  lgsdir  27507  lgsdilem2  27508  lgsdi  27509  lgsne0  27510  gausslemma2dlem3  27543  lgseisenlem1  27550  lgsquadlem2  27556  chebbnd1lem1  27644  chtppilimlem1  27648  rplogsumlem2  27660  rpvmasumlem  27662  dchrisumlem1  27664  dchrisumlem2  27665  dchrmusum2  27669  dchrvmasum2lem  27671  dchrvmasumiflem1  27676  dchrisum0flblem1  27683  dchrisum0flblem2  27684  dchrisum0flb  27685  dchrisum0re  27688  dchrisum0lem1b  27690  dchrisum0lem1  27691  dchrisum0lem2a  27692  dchrisum0lem2  27693  dchrisum0lem3  27694  mudivsum  27705  mulogsum  27707  mulog2sumlem2  27710  selberg2lem  27725  logdivbnd  27731  pntrsumo1  27740  pntrsumbnd2  27742  pntrlog2bndlem2  27753  pntrlog2bndlem4  27755  pntrlog2bndlem6a  27757  pntlemj  27778  pntlemf  27780  ostth2lem3  27810  madebdayim  28092  oldbdayim  28093  newbdayim  28107  cutminmax  28140  noseqp1  28495  tglngne  28830  ltgseg  28876  eedimeq  29259  axlowdimlem16  29318  ebtwntg  29343  subgruhgredgd  29645  subumgredg2  29646  umgrres1lem  29671  wlkson  30015  wksonproplem  30063  trlsonfval  30064  pthsonfval  30100  spthson  30101  crctcshwlkn0lem4  30173  crctcshwlkn0lem5  30174  eupth2lems  30600  numclwwlk1lem2foa  30716  numclwlk1lem2  30732  numclwwlk2lem1  30738  htthlem  31280  hhsscms  31641  shmodsi  31752  pjoc1i  31794  5oalem1  32017  mayete3i  32091  adj1  32296  iundisj2f  32946  fmptco1f1o  32989  fcnvgreu  33028  suppovss  33037  ssnnssfz  33143  nn0diffz0  33150  iundisj2fi  33153  indpreima  33196  ccatws1f1o  33280  cshw1s2  33289  gsumhashmul  33396  gsummulsubdishift1  33397  gsumwrd2dccat  33407  fzo0pmtrlast  33421  wrdpmtrlast  33422  pmtrto1cl  33428  psgnfzto1stlem  33429  fzto1st1  33431  cycpmfv1  33442  cycpmfv2  33443  cycpmco2rn  33454  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cyc3evpm  33479  cyc3genpm  33481  cycpmconjslem2  33484  cyc3conja  33486  elrgspnlem1  33571  elrgspnlem2  33572  erler  33594  nsgmgc  33730  nsgqusf1olem2  33732  unitpidl1  33741  elrspunsn  33746  mxidlirredi  33763  mxidlirred  33764  opprqusplusg  33780  opprqus0g  33781  opprqusmulr  33782  idlsrgmulrss1  33810  idlsrgmulrss2  33811  rprmcl  33817  rprmdvds  33818  rprmnz  33819  rprmnunit  33820  rprmasso  33824  rprmirredb  33831  pidufd  33842  1arithufdlem2  33844  1arithufdlem3  33845  zringfrac  33853  ply1dg3rt0irred  33883  m1pmeq  33884  ig1pmindeg  33901  selvply1rhmlem2  33920  selvply1rhmlem4  33922  selvply1rhm0  33925  extvfvvcl  33934  evlextv  33941  psrmonprod  33951  esplysply  33970  esplyind  33974  esplyfvn  33976  vietalem  33978  exsslsb  33996  ply1degltdimlem  34021  lindsun  34024  fldextfld1  34046  fldextfld2  34047  rtelextdg2  34126  cos9thpiminplylem1  34181  1smat1  34203  submateqlem2  34207  lmatfval  34213  mdetlap1  34225  madjusmdetlem1  34226  madjusmdetlem2  34227  madjusmdetlem3  34228  madjusmdetlem4  34229  zarclssn  34272  zartopn  34274  zarmxt1  34279  rhmpreimacnlem  34283  rhmpreimacn  34284  pnfneige0  34350  pl1cn  34354  rrhqima  34413  esumfzf  34468  esumpcvgval  34477  esumpmono  34478  esumcvg  34485  ldgenpisyslem1  34562  ldgenpisys  34565  measbase  34596  dya2iocnei  34681  oddpwdc  34753  eulerpartlems  34759  eulerpartlemb  34767  sseqf  34791  fibp1  34800  orrvcval4  34864  orrvcoel  34865  orrvccel  34866  ballotlem2  34888  ballotlemfrceq  34928  signsplypnf  34946  signswch  34957  signstf0  34964  signstfvn  34965  signstfvneq0  34968  signstfvcl  34969  signstfveq0  34973  signsvfn  34978  fct2relem  34993  fsum2dsub  35003  reprsuc  35011  reprpmtf1o  35022  breprexplema  35026  breprexplemc  35028  hgt749d  35045  hgt750lemb  35052  tgoldbachgnn  35055  bnj1172  35398  bnj1245  35411  bnj1311  35421  bnj1450  35447  bnj1501  35464  r1elcl  35500  subfacp1lem1  35679  subfacp1lem5  35684  subfacp1lem6  35685  subfacval2  35687  erdszelem7  35697  cvxpconn  35742  cvxsconn  35743  cvmliftlem5  35789  cvmliftlem7  35791  cvmliftlem10  35794  cvmliftlem13  35796  mrsubvrs  36022  msubrn  36029  msubco  36031  msubvrs  36060  r1peuqusdeg1  36143  imageval  36428  fwddifnp1  36665  knoppcnlem8  37117  knoppcnlem10  37119  bj-unirel  37715  icoreunrn  38033  istoprelowl  38034  poimirlem3  38302  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem12  38311  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  poimirlem29  38328  poimirlem31  38330  mblfinlem2  38337  ftc1cnnc  38371  upixp  38408  sdclem2  38421  caushft  38440  ismtyres  38487  rrnmet  38508  rrndstprj1  38509  rrndstprj2  38510  rrncmslem  38511  rrnequiv  38514  iccbnd  38519  osumcllem7N  40764  pexmidlem4N  40775  lcfrlem4  42347  lcfrlem5  42348  lcfrlem6  42349  lcfrlem16  42360  lcfrlem38  42382  mapdrvallem2  42447  mapdh8ab  42579  mapdh8ad  42581  mapdh8e  42586  3factsumint3  42818  aks4d1p1p1  42858  fldhmf1  42885  aks6d1c1p2  42904  aks6d1c1p3  42905  aks6d1c1p7  42908  aks6d1c1p6  42909  aks6d1c1p8  42910  aks6d1c1  42911  evl1gprodd  42912  idomnnzpownz  42927  aks6d1c5lem1  42931  aks6d1c5lem3  42932  aks6d1c5lem2  42933  deg1gprod  42935  sticksstones10  42950  aks6d1c6lem3  42967  aks5lem2  42982  aks5lem3a  42984  unitscyglem5  42994  fz1sump1  43099  sumcubes  43102  evlselv  43349  mhphf2  43358  prjspnfv01  43384  prjspner01  43385  prjspner1  43386  mapfzcons  43475  diophren  43568  irrapxlem1  43577  monotuz  43696  acongeq  43738  jm2.26lem3  43756  jm3.1lem2  43773  pw2f1ocnv  43792  idomodle  43946  trclfvdecomr  44482  imo72b2lem0  44919  imo72b2lem1  44923  dvgrat  45050  cvgdvgrat  45051  hashnzfz2  45059  fcnre  45773  refsumcn  45778  rfcnnnub  45784  disjf1o  45937  disjinfi  45938  ssmapsn  45960  ssuzfz  46093  nnsplit  46102  uzssd2  46159  uzublem  46172  fsumsermpt  46323  climsuselem1  46351  limcperiod  46372  sumnnodd  46374  lptioo2cn  46387  lptioo1cn  46388  climresmpt  46401  allbutfifvre  46417  climleltrp  46418  cnrefiisplem  46571  cncfshift  46616  cncfperiod  46621  cncfshiftioo  46634  fperdvper  46661  dvnmptdivc  46680  dvnmul  46685  dvmptfprod  46687  dvnprodlem3  46690  stoweidlem11  46753  stoweidlem15  46757  stoweidlem17  46759  stoweidlem20  46762  stoweidlem34  46776  stoweidlem35  46777  stoweidlem46  46788  stoweidlem47  46789  stoweidlem56  46798  stoweidlem59  46801  stoweidlem62  46804  stirlinglem5  46820  stirlinglem14  46829  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  fourierdlem11  46860  fourierdlem15  46864  fourierdlem16  46865  fourierdlem21  46870  fourierdlem22  46871  fourierdlem25  46874  fourierdlem48  46896  fourierdlem49  46897  fourierdlem52  46900  fourierdlem54  46902  fourierdlem58  46906  fourierdlem62  46910  fourierdlem64  46912  fourierdlem65  46913  fourierdlem69  46917  fourierdlem70  46918  fourierdlem71  46919  fourierdlem73  46921  fourierdlem80  46928  fourierdlem81  46929  fourierdlem83  46931  fourierdlem92  46940  fourierdlem93  46941  fourierdlem97  46945  fourierdlem103  46951  fourierdlem104  46952  fourierdlem112  46960  fourierdlem113  46961  fouriercnp  46968  fouriersw  46973  elaa2lem  46975  etransclem4  46980  etransclem7  46983  etransclem10  46986  etransclem14  46990  etransclem15  46991  etransclem24  47000  etransclem25  47001  etransclem31  47007  etransclem32  47008  etransclem35  47011  etransclem44  47020  etransclem46  47022  qndenserrnopnlem  47039  qndenserrn  47041  prsal  47060  salgencntex  47085  subsaliuncl  47100  subsalsal  47101  sge0tsms  47122  sge0fodjrnlem  47158  sge0isum  47169  iundjiunlem  47201  iundjiun  47202  meadjiunlem  47207  meaiunlelem  47210  meaiuninclem  47222  meaiininc2  47230  caragensplit  47242  carageneld  47244  carageniuncllem1  47263  caratheodorylem1  47268  caratheodorylem2  47269  hoicvr  47290  hsphoidmvle2  47327  hsphoidmvle  47328  hoidmv1lelem2  47334  hoidmv1lelem3  47335  hoidmvlelem2  47338  hoiqssbllem2  47365  pimdecfgtioc  47457  pimincfltioc  47458  pimdecfgtioo  47459  pimincfltioo  47460  smflimlem3  47515  smfmullem4  47536  smfsupxr  47558  smflimsuplem2  47563  smflimsuplem5  47566  ormklocald  47618  natlocalincr  47620  elmod2  48126  isuspgrim0lem  48686  upgrimtrlslem2  48698  ssnn0ssfz  49157  zlmodzxzscm  49165  rmsupp0  49176  lincsum  49237  lincscm  49238  lindslinindimp2lem4  49269  lincresunit3  49289  elbigofrcl  49358  intubeu  49790  unilbeu  49791  cicrcl2  49849  cic1st2nd  49853  imaf1homlem  49913  oppfrcl  49934  eloppf  49939  imasubc  49957  imaid  49960  oppcuprcl5  50007  oppcup3  50015  uptrlem2  50017  uptrlem3  50018  natoppf  50035  elxpcbasex1ALT  50055  elxpcbasex2ALT  50057  swapf1a  50075  swapf2f1oa  50083  swapfida  50086  cofuswapf1  50100  cofuswapf2  50101  fucoppcco  50215  postc  50375  reldmlan2  50423  reldmran2  50424  lanrcl  50427  ranrcl  50428  setrec1  50497  aacllem  50649  crosspalti  50675  crossp3i  50676