Theorem eleqtrdi 2874

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

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839

This theorem is referenced by:  eleqtrrdi  2875  3eltr3g  2880  prid2g  4722  ndmfvrcl  6902  fnwelem  8113  tz7.48-1  8416  brwitnlem  8478  oeeulem  8573  dffi3  9379  cnfcom3lem  9660  ttrclse  9684  alephgeom  10040  fpwwe2lem5  10595  canthwelem  10610  hargch  10633  r1wunlim  10697  eluzel2  12846  fseq1p1m1  13605  fznn0sub2  13642  nn0split  13650  seqp1d  14033  exple1  14192  digit1  14252  bcval5  14333  bcpasc  14336  hashf1  14472  seqcoll  14479  seqcoll2  14480  ccatrn  14605  swrdccat2  14685  cats1un  14736  pfxccatin12lem3  14747  splfv2a  14771  splval2  14772  caubnd  15388  limsupgre  15510  clim2ser  15684  clim2ser2  15685  iserex  15686  isermulc2  15687  iserle  15689  iserge0  15690  climub  15691  climserle  15692  isercolllem2  15695  isercolllem3  15696  isercoll  15697  isercoll2  15698  serf0  15710  iseraltlem2  15712  iseraltlem3  15713  iseralt  15714  sumeq2ii  15722  summolem3  15743  summolem2a  15744  fsum  15749  sum0  15750  fsumcl2lem  15760  fsumadd  15769  isumclim3  15788  isumadd  15796  fsump1i  15798  fsummulc2  15813  fsumrelem  15837  iserabs  15845  cvgcmp  15846  cvgcmpub  15847  cvgcmpce  15848  binom1dif  15865  isumshft  15871  isumsplit  15872  isumrpcl  15875  isumsup2  15878  climcndslem1  15881  climcndslem2  15882  climcnds  15883  arisum2  15893  trireciplem  15894  geoser  15899  pwdif  15900  geolim  15902  geo2lim  15907  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  mertens  15918  clim2prod  15920  clim2div  15921  ntrivcvgfvn0  15931  ntrivcvgtail  15932  prodeq2ii  15943  prodmolem3  15965  prodmolem2a  15966  fprod  15973  fprodntriv  15974  fprodss  15980  fprodser  15981  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodabs  16006  fprodeq0  16007  fprodn0  16011  iprodclim3  16032  iprodmul  16035  fallfacfwd  16068  0fallfac  16069  binomfallfaclem2  16072  fallfacval4  16075  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  efcvgfsum  16118  efcj  16124  fprodefsum  16127  effsumlt  16145  ruclem7  16270  bitsfzolem  16470  bitsfzo  16471  bitsfi  16473  bitsinv1lem  16477  bitsinv1  16478  bitsinvp1  16485  sadcp1  16491  sadadd  16503  sadass  16507  bitsres  16509  smupp1  16516  smuval2  16518  smupval  16524  smueqlem  16526  smumul  16529  algrp1  16610  phiprmpw  16813  crth  16815  phimullem  16816  eulerthlem2  16819  prmdiv  16822  pcpremul  16881  pcmpt  16930  pcfac  16937  pockthlem  16943  pockthg  16944  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  prmrec  16960  1arith  16965  vdwapun  17012  vdwlem1  17019  vdwlem2  17020  vdwlem3  17021  vdwlem6  17024  vdwlem8  17026  vdwlem10  17028  vdw  17032  imasvscafn  17569  oppccatid  17753  oppccomfpropd  17761  brcic  17833  funcoppc  17910  invfuc  18012  hofcl  18293  yonedalem4c  18311  chnccats1  18659  gsumwsubmcl  18873  gsumsgrpccat  18876  gsumwmhm  18881  mulgnnp1  19126  mulgnnsubcl  19130  mulgnn0z  19145  mulgnndir  19147  ghmquskerlem1  19325  ghmquskerco  19326  psgnunilem4  19539  psgnran  19557  sylow1lem1  19640  lsmmod2  19718  lsmdisj2r  19727  efginvrel2  19769  efgsdmi  19774  efgsrel  19776  efgs1b  19778  efgsp1  19779  efgredleme  19785  efgredlemc  19787  efgcpbllemb  19797  frgpuplem  19814  mulgnn0di  19867  frgpnabllem1  19915  lt6abl  19937  cycsubgcyg  19943  gsumval3eu  19946  gsumval3  19949  gsumzcl2  19952  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  telgsumfz0s  20033  dprdwd  20055  dprd2da  20086  pgpfaclem1  20125  srgbinom  20283  isirred  20470  idomdomd  20778  idomcringd  20779  lspprid2  21067  lspsnat  21217  lsppratlem1  21219  lsppratlem3  21221  lidl0cl  21292  lidlacl  21293  lidlnegcl  21294  elrspsn  21312  2idllidld  21326  2idlridld  21327  rng2idl1cntr  21377  psgnghm  21634  frlmvscavalb  21824  frlmvplusgscavalb  21825  psrbaglefi  21980  psrass23l  22020  psrass23  22022  mplcoe5lem  22094  mpfind  22170  selvval  22175  mhpvscacl  22221  psr1bascl  22264  ply1basf  22266  gsummoncoe1  22373  lply1binom  22375  lply1binomsc  22376  mpfpf1  22416  pf1mpf  22417  evl1scvarpw  22428  evl1maprhm  22444  matbas2i  22484  matecld  22488  matgsum  22499  mpomatmul  22508  dmatmul  22559  1mavmul  22610  mdetleib2  22650  m1detdiag  22659  marep01ma  22722  smadiadetlem4  22731  slesolinv  22742  pmatcollpw3fi1lem1  22848  chpscmat  22904  chpscmatgsumbin  22906  chp0mat  22908  chpidmat  22909  chfacfisf  22916  chfacfisfcpmat  22917  chfacfpmmulgsum2  22927  cldrcl  23088  ordtbas  23254  iscnp2  23301  dis1stc  23561  ptbasfi  23643  ptpjopn  23674  ptclsg  23677  ptcnp  23684  kqtop  23807  reghmph  23855  ptcmplem2  24115  ptcmplem3  24116  ptcmplem4  24117  tsmslem1  24191  utop2nei  24312  isucn2  24340  cuspcvg  24362  cnextucn  24364  imasdsf1olem  24435  blcvx  24860  xrhmeo  25010  cnrehmeo  25017  evth  25023  reparphti  25061  iscau4  25343  iscmet3lem1  25355  lmle  25365  rrxfsupp  25466  rrxdsfi  25475  pjthlem2  25502  ovollb2lem  25552  ovolunlem1a  25560  ovoliunlem1  25566  ovoliun2  25570  ovolscalem1  25577  ovolicc1  25580  ovolicc2lem4  25584  iundisj2  25613  voliunlem1  25614  volsup  25620  ioombl1lem4  25625  uniioovol  25643  uniioombllem3  25649  uniioombllem4  25650  uniioombllem6  25652  vitalilem5  25676  mbfimaopnlem  25719  mbflimsup  25730  mbfi1fseqlem3  25781  iblitg  25832  dvcnp2  25984  dvnp1  25989  cpncn  26000  dvmulbr  26003  dvcobr  26010  dvlip2  26059  dvfsumlem2  26091  dvfsumlem3  26092  dvfsumrlimge0  26094  dvfsumrlim2  26096  ftc1cn  26107  elplyd  26264  ply1termlem  26265  ply1term  26266  ply0  26270  plyeq0lem  26272  plyaddlem1  26275  plymullem1  26276  plyaddlem  26277  plymullem  26278  coeeulem  26286  plyco  26303  coeeq2  26304  coefv0  26310  coemulhi  26316  coemulc  26317  plycj  26339  plycjOLD  26341  dvply1  26350  vieta1lem2  26377  elqaalem2  26386  dvtaylp  26435  dvntaylp  26436  taylthlem1  26438  taylth  26440  ulmres  26453  ulmshftlem  26454  ulmshft  26455  ulmcau  26460  ulmdvlem1  26465  mtest  26469  mtestbdd  26470  pserulm  26487  psercn2  26488  psercnlem1  26490  psercn  26491  pserdvlem2  26493  abelthlem6  26501  abelth  26506  efif1olem1  26609  efif1olem3  26611  efif1olem4  26612  logcn  26714  advlogexp  26722  efopn  26725  cxpeq  26824  asinsin  26959  atantayl  27004  leibpilem2  27008  birthdaylem2  27019  birthdaylem3  27020  efrlim  27036  emcllem2  27063  emcllem5  27066  emcllem7  27068  harmonicbnd4  27077  fsumharmonic  27078  lgamgulm2  27102  lgamcvglem  27106  lgamcvg2  27121  gamcvg2lem  27125  wilthlem2  27135  wilthlem3  27136  ftalem1  27139  ftalem2  27140  ftalem3  27141  ftalem5  27143  basellem2  27148  basellem3  27149  basellem5  27151  basellem8  27154  ppiprm  27217  ppinprm  27218  chtprm  27219  chtnprm  27220  chpp1  27221  vma1  27232  ppiltx  27243  musum  27257  0sgmppw  27264  1sgmprm  27265  ppiublem2  27269  chtublem  27277  fsumvma2  27280  chpchtsum  27285  logexprlim  27291  bposlem5  27354  lgscllem  27370  lgsval2lem  27373  lgsval4a  27385  lgsneg  27387  lgsdir2lem3  27393  lgsdir2lem5  27395  lgsdir  27398  lgsdilem2  27399  lgsdi  27400  lgsne0  27401  gausslemma2dlem3  27434  lgseisenlem1  27441  lgsquadlem2  27447  chebbnd1lem1  27535  chtppilimlem1  27539  rplogsumlem2  27551  rpvmasumlem  27553  dchrisumlem1  27555  dchrisumlem2  27556  dchrmusum2  27560  dchrvmasum2lem  27562  dchrvmasumiflem1  27567  dchrisum0flblem1  27574  dchrisum0flblem2  27575  dchrisum0flb  27576  dchrisum0re  27579  dchrisum0lem1b  27581  dchrisum0lem1  27582  dchrisum0lem2a  27583  dchrisum0lem2  27584  dchrisum0lem3  27585  mudivsum  27596  mulogsum  27598  mulog2sumlem2  27601  selberg2lem  27616  logdivbnd  27622  pntrsumo1  27631  pntrsumbnd2  27633  pntrlog2bndlem2  27644  pntrlog2bndlem4  27646  pntrlog2bndlem6a  27648  pntlemj  27669  pntlemf  27671  ostth2lem3  27701  madebdayim  27983  oldbdayim  27984  newbdayim  27998  cutminmax  28031  noseqp1  28386  tglngne  28721  ltgseg  28767  eedimeq  29101  axlowdimlem16  29160  ebtwntg  29185  subgruhgredgd  29487  subumgredg2  29488  umgrres1lem  29513  wlkson  29857  wksonproplem  29905  trlsonfval  29906  pthsonfval  29942  spthson  29943  crctcshwlkn0lem4  30015  crctcshwlkn0lem5  30016  eupth2lems  30442  numclwwlk1lem2foa  30558  numclwlk1lem2  30574  numclwwlk2lem1  30580  htthlem  31122  hhsscms  31483  shmodsi  31594  pjoc1i  31636  5oalem1  31859  mayete3i  31933  adj1  32138  iundisj2f  32792  fmptco1f1o  32837  fcnvgreu  32876  suppovss  32885  ssnnssfz  32991  nn0diffz0  32998  iundisj2fi  33001  indpreima  33045  ccatws1f1o  33131  cshw1s2  33140  gsumhashmul  33249  gsummulsubdishift1  33250  gsumwrd2dccat  33260  fzo0pmtrlast  33274  wrdpmtrlast  33275  pmtrto1cl  33281  psgnfzto1stlem  33282  fzto1st1  33284  cycpmfv1  33295  cycpmfv2  33296  cycpmco2rn  33307  cycpmco2lem4  33311  cycpmco2lem5  33312  cycpmco2lem6  33313  cyc3evpm  33332  cyc3genpm  33334  cycpmconjslem2  33337  cyc3conja  33339  elrgspnlem1  33425  elrgspnlem2  33426  erler  33448  idomrcanOLD  33468  nsgmgc  33600  nsgqusf1olem2  33602  unitpidl1  33612  elrspunsn  33617  ssdifidllem  33645  mxidlirredi  33661  mxidlirred  33662  opprqusplusg  33679  opprqus0g  33680  opprqusmulr  33681  idlsrgmulrss1  33709  idlsrgmulrss2  33710  rprmcl  33716  rprmdvds  33717  rprmnz  33718  rprmnunit  33719  rprmasso  33723  rprmirredb  33730  pidufd  33741  1arithufdlem2  33743  1arithufdlem3  33744  zringfrac  33752  ply1dg3rt0irred  33782  m1pmeq  33783  ig1pmindeg  33800  selvply1rhmlem2  33820  selvply1rhmlem4  33822  selvply1rhm0  33825  extvfvvcl  33834  evlextv  33841  psrmonprod  33851  esplysply  33870  esplyind  33874  esplyfvn  33876  vietalem  33878  exsslsb  33896  ply1degltdimlem  33921  lindsun  33924  fldextfld1  33946  fldextfld2  33947  rtelextdg2  34026  cos9thpiminplylem1  34081  1smat1  34103  submateqlem2  34107  lmatfval  34113  mdetlap1  34125  madjusmdetlem1  34126  madjusmdetlem2  34127  madjusmdetlem3  34128  madjusmdetlem4  34129  zarclssn  34172  zartopn  34174  zarmxt1  34179  rhmpreimacnlem  34183  rhmpreimacn  34184  pnfneige0  34250  pl1cn  34254  rrhqima  34313  esumfzf  34368  esumpcvgval  34377  esumpmono  34378  esumcvg  34385  ldgenpisyslem1  34462  ldgenpisys  34465  measbase  34496  dya2iocnei  34581  oddpwdc  34653  eulerpartlems  34659  eulerpartlemb  34667  sseqf  34691  fibp1  34700  orrvcval4  34764  orrvcoel  34765  orrvccel  34766  ballotlem2  34788  ballotlemfrceq  34828  signsplypnf  34846  signswch  34857  signstf0  34864  signstfvn  34865  signstfvneq0  34868  signstfvcl  34869  signstfveq0  34873  signsvfn  34878  fct2relem  34893  fsum2dsub  34903  reprsuc  34911  reprpmtf1o  34922  breprexplema  34926  breprexplemc  34928  hgt749d  34945  hgt750lemb  34952  tgoldbachgnn  34955  bnj1172  35298  bnj1245  35311  bnj1311  35321  bnj1450  35347  bnj1501  35364  r1elcl  35398  subfacp1lem1  35534  subfacp1lem5  35539  subfacp1lem6  35540  subfacval2  35542  erdszelem7  35552  cvxpconn  35597  cvxsconn  35598  cvmliftlem5  35644  cvmliftlem7  35646  cvmliftlem10  35649  cvmliftlem13  35651  mrsubvrs  35877  msubrn  35884  msubco  35886  msubvrs  35915  r1peuqusdeg1  35998  imageval  36283  fwddifnp1  36520  knoppcnlem8  36943  knoppcnlem10  36945  bj-unirel  37541  icoreunrn  37858  istoprelowl  37859  poimirlem3  38127  poimirlem4  38128  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem12  38136  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem20  38144  poimirlem21  38145  poimirlem22  38146  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  poimirlem29  38153  poimirlem31  38155  mblfinlem2  38162  ftc1cnnc  38196  upixp  38233  sdclem2  38246  caushft  38265  ismtyres  38312  rrnmet  38333  rrndstprj1  38334  rrndstprj2  38335  rrncmslem  38336  rrnequiv  38339  iccbnd  38344  osumcllem7N  40591  pexmidlem4N  40602  lcfrlem4  42174  lcfrlem5  42175  lcfrlem6  42176  lcfrlem16  42187  lcfrlem38  42209  mapdrvallem2  42274  mapdh8ab  42406  mapdh8ad  42408  mapdh8e  42413  3factsumint3  42645  aks4d1p1p1  42685  fldhmf1  42712  aks6d1c1p2  42731  aks6d1c1p3  42732  aks6d1c1p7  42735  aks6d1c1p6  42736  aks6d1c1p8  42737  aks6d1c1  42738  evl1gprodd  42739  idomnnzpownz  42754  aks6d1c5lem1  42758  aks6d1c5lem3  42759  aks6d1c5lem2  42760  deg1gprod  42762  sticksstones10  42777  aks6d1c6lem3  42794  aks5lem2  42809  aks5lem3a  42811  unitscyglem5  42821  fz1sump1  42924  sumcubes  42927  evlselv  43176  mhphf2  43185  prjspnfv01  43211  prjspner01  43212  prjspner1  43213  mapfzcons  43302  diophren  43395  irrapxlem1  43404  monotuz  43523  acongeq  43565  jm2.26lem3  43583  jm3.1lem2  43600  pw2f1ocnv  43619  idomodle  43773  trclfvdecomr  44309  imo72b2lem0  44746  imo72b2lem1  44750  scottelrankd  44828  dvgrat  44893  cvgdvgrat  44894  hashnzfz2  44902  fcnre  45610  refsumcn  45615  rfcnnnub  45621  disjf1o  45774  disjinfi  45775  ssmapsn  45797  ssuzfz  45930  nnsplit  45939  uzssd2  45996  uzublem  46009  fsumsermpt  46160  climsuselem1  46188  limcperiod  46209  sumnnodd  46211  lptioo2cn  46224  lptioo1cn  46225  climresmpt  46238  allbutfifvre  46254  climleltrp  46255  cnrefiisplem  46408  cncfshift  46453  cncfperiod  46458  cncfshiftioo  46471  fperdvper  46498  dvnmptdivc  46517  dvnmul  46522  dvmptfprod  46524  dvnprodlem3  46527  stoweidlem11  46590  stoweidlem15  46594  stoweidlem17  46596  stoweidlem20  46599  stoweidlem34  46613  stoweidlem35  46614  stoweidlem46  46625  stoweidlem47  46626  stoweidlem56  46635  stoweidlem59  46638  stoweidlem62  46641  stirlinglem5  46657  stirlinglem14  46666  dirkertrigeqlem2  46678  dirkertrigeqlem3  46679  fourierdlem11  46697  fourierdlem15  46701  fourierdlem16  46702  fourierdlem21  46707  fourierdlem22  46708  fourierdlem25  46711  fourierdlem48  46733  fourierdlem49  46734  fourierdlem52  46737  fourierdlem54  46739  fourierdlem58  46743  fourierdlem62  46747  fourierdlem64  46749  fourierdlem65  46750  fourierdlem69  46754  fourierdlem70  46755  fourierdlem71  46756  fourierdlem73  46758  fourierdlem80  46765  fourierdlem81  46766  fourierdlem83  46768  fourierdlem92  46777  fourierdlem93  46778  fourierdlem97  46782  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  fourierdlem113  46798  fouriercnp  46805  fouriersw  46810  elaa2lem  46812  etransclem4  46817  etransclem7  46820  etransclem10  46823  etransclem14  46827  etransclem15  46828  etransclem24  46837  etransclem25  46838  etransclem31  46844  etransclem32  46845  etransclem35  46848  etransclem44  46857  etransclem46  46859  qndenserrnopnlem  46876  qndenserrn  46878  prsal  46897  salgencntex  46922  subsaliuncl  46937  subsalsal  46938  sge0tsms  46959  sge0fodjrnlem  46995  sge0isum  47006  iundjiunlem  47038  iundjiun  47039  meadjiunlem  47044  meaiunlelem  47047  meaiuninclem  47059  meaiininc2  47067  caragensplit  47079  carageneld  47081  carageniuncllem1  47100  caratheodorylem1  47105  caratheodorylem2  47106  hoicvr  47127  hsphoidmvle2  47164  hsphoidmvle  47165  hoidmv1lelem2  47171  hoidmv1lelem3  47172  hoidmvlelem2  47175  hoiqssbllem2  47202  pimdecfgtioc  47294  pimincfltioc  47295  pimdecfgtioo  47296  pimincfltioo  47297  smflimlem3  47352  smfmullem4  47373  smfsupxr  47395  smflimsuplem2  47400  smflimsuplem5  47403  ormklocald  47455  natlocalincr  47457  elmod2  47960  isuspgrim0lem  48520  upgrimtrlslem2  48532  ssnn0ssfz  48976  zlmodzxzscm  48984  rmsupp0  48995  lincsum  49056  lincscm  49057  lindslinindimp2lem4  49088  lincresunit3  49108  elbigofrcl  49177  intubeu  49610  unilbeu  49611  cicrcl2  49669  cic1st2nd  49673  imaf1homlem  49733  oppfrcl  49754  eloppf  49759  imasubc  49777  imaid  49780  oppcuprcl5  49827  oppcup3  49835  uptrlem2  49837  uptrlem3  49838  natoppf  49855  elxpcbasex1ALT  49875  elxpcbasex2ALT  49877  swapf1a  49895  swapf2f1oa  49903  swapfida  49906  cofuswapf1  49920  cofuswapf2  49921  fucoppcco  50035  postc  50195  reldmlan2  50243  reldmran2  50244  lanrcl  50247  ranrcl  50248  setrec1  50317  aacllem  50427