Theorem eleqtrdi 2838

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eleqtrrdi  2839  3eltr3g  2844  prid2g  4725  ndmfvrcl  6894  fnwelem  8110  tz7.48-1  8411  brwitnlem  8471  oeeulem  8565  dffi3  9382  cnfcom3lem  9656  ttrclse  9680  alephgeom  10035  fpwwe2lem5  10588  canthwelem  10603  hargch  10626  r1wunlim  10690  eluzel2  12798  fseq1p1m1  13559  fznn0sub2  13596  nn0split  13604  seqp1d  13983  exple1  14142  digit1  14202  bcval5  14283  bcpasc  14286  hashf1  14422  seqcoll  14429  seqcoll2  14430  ccatrn  14554  swrdccat2  14634  cats1un  14686  pfxccatin12lem3  14697  splfv2a  14721  splval2  14722  caubnd  15325  limsupgre  15447  clim2ser  15621  clim2ser2  15622  iserex  15623  isermulc2  15624  iserle  15626  iserge0  15627  climub  15628  climserle  15629  isercolllem2  15632  isercolllem3  15633  isercoll  15634  isercoll2  15635  serf0  15647  iseraltlem2  15649  iseraltlem3  15650  iseralt  15651  sumeq2ii  15659  summolem3  15680  summolem2a  15681  fsum  15686  sum0  15687  fsumcl2lem  15697  fsumadd  15706  isumclim3  15725  isumadd  15733  fsump1i  15735  fsummulc2  15750  fsumrelem  15773  iserabs  15781  cvgcmp  15782  cvgcmpub  15783  cvgcmpce  15784  binom1dif  15799  isumshft  15805  isumsplit  15806  isumrpcl  15809  isumsup2  15812  climcndslem1  15815  climcndslem2  15816  climcnds  15817  arisum2  15827  trireciplem  15828  geoser  15833  pwdif  15834  geolim  15836  geo2lim  15841  cvgrat  15849  mertenslem1  15850  mertenslem2  15851  mertens  15852  clim2prod  15854  clim2div  15855  ntrivcvgfvn0  15865  ntrivcvgtail  15866  prodeq2ii  15877  prodmolem3  15899  prodmolem2a  15900  fprod  15907  fprodntriv  15908  fprodss  15914  fprodser  15915  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodabs  15940  fprodeq0  15941  fprodn0  15945  iprodclim3  15966  iprodmul  15969  fallfacfwd  16002  0fallfac  16003  binomfallfaclem2  16006  fallfacval4  16009  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  efcvgfsum  16052  efcj  16058  fprodefsum  16061  effsumlt  16079  ruclem7  16204  bitsfzolem  16404  bitsfzo  16405  bitsfi  16407  bitsinv1lem  16411  bitsinv1  16412  bitsinvp1  16419  sadcp1  16425  sadadd  16437  sadass  16441  bitsres  16443  smupp1  16450  smuval2  16452  smupval  16458  smueqlem  16460  smumul  16463  algrp1  16544  phiprmpw  16746  crth  16748  phimullem  16749  eulerthlem2  16752  prmdiv  16755  pcpremul  16814  pcmpt  16863  pcfac  16870  pockthlem  16876  pockthg  16877  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  prmrec  16893  1arith  16898  vdwapun  16945  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  vdw  16965  imasvscafn  17500  oppccatid  17680  oppccomfpropd  17688  brcic  17760  funcoppc  17837  invfuc  17939  hofcl  18220  yonedalem4c  18238  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  mulgnnp1  19014  mulgnnsubcl  19018  mulgnn0z  19033  mulgnndir  19035  ghmquskerlem1  19215  ghmquskerco  19216  psgnunilem4  19427  psgnran  19445  sylow1lem1  19528  lsmmod2  19606  lsmdisj2r  19615  efginvrel2  19657  efgsdmi  19662  efgsrel  19664  efgs1b  19666  efgsp1  19667  efgredleme  19673  efgredlemc  19675  efgcpbllemb  19685  frgpuplem  19702  mulgnn0di  19755  frgpnabllem1  19803  lt6abl  19825  cycsubgcyg  19831  gsumval3eu  19834  gsumval3  19837  gsumzcl2  19840  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  telgsumfz0s  19921  dprdwd  19943  dprd2da  19974  pgpfaclem1  20013  srgbinom  20140  isirred  20328  idomdomd  20635  idomcringd  20636  lspprid2  20904  lspsnat  21055  lsppratlem1  21057  lsppratlem3  21059  lidl0cl  21130  lidlacl  21131  lidlnegcl  21132  elrspsn  21150  2idllidld  21164  2idlridld  21165  rng2idl1cntr  21215  psgnghm  21489  frlmvscavalb  21679  frlmvplusgscavalb  21680  psrbaglefi  21835  psrass23l  21876  psrass23  21878  mplcoe5lem  21946  mpfind  22014  selvval  22022  mhpvscacl  22041  psr1bascl  22085  ply1basf  22087  gsummoncoe1  22195  lply1binom  22197  lply1binomsc  22198  mpfpf1  22238  pf1mpf  22239  evl1scvarpw  22250  evl1maprhm  22266  matbas2i  22309  matecld  22313  matgsum  22324  mpomatmul  22333  dmatmul  22384  1mavmul  22435  mdetleib2  22475  m1detdiag  22484  marep01ma  22547  smadiadetlem4  22556  slesolinv  22567  pmatcollpw3fi1lem1  22673  chpscmat  22729  chpscmatgsumbin  22731  chp0mat  22733  chpidmat  22734  chfacfisf  22741  chfacfisfcpmat  22742  chfacfpmmulgsum2  22752  cldrcl  22913  ordtbas  23079  iscnp2  23126  dis1stc  23386  ptbasfi  23468  ptpjopn  23499  ptclsg  23502  ptcnp  23509  kqtop  23632  reghmph  23680  ptcmplem2  23940  ptcmplem3  23941  ptcmplem4  23942  tsmslem1  24016  utop2nei  24138  isucn2  24166  cuspcvg  24188  cnextucn  24190  imasdsf1olem  24261  blcvx  24686  xrhmeo  24844  cnrehmeo  24851  cnrehmeoOLD  24852  evth  24858  reparphti  24896  reparphtiOLD  24897  iscau4  25179  iscmet3lem1  25191  lmle  25201  rrxfsupp  25302  rrxdsfi  25311  pjthlem2  25338  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliun2  25407  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem4  25421  iundisj2  25450  voliunlem1  25451  volsup  25457  ioombl1lem4  25462  uniioovol  25480  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  vitalilem5  25513  mbfimaopnlem  25556  mbflimsup  25567  mbfi1fseqlem3  25618  iblitg  25669  dvcnp2  25821  dvnp1  25827  cpncn  25838  dvmulbr  25841  dvcobr  25849  dvlip2  25900  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumrlimge0  25937  dvfsumrlim2  25939  ftc1cn  25950  elplyd  26107  ply1termlem  26108  ply1term  26109  ply0  26113  plyeq0lem  26115  plyaddlem1  26118  plymullem1  26119  plyaddlem  26120  plymullem  26121  coeeulem  26129  plyco  26146  coeeq2  26147  coefv0  26153  coemulhi  26159  coemulc  26160  plycj  26183  plycjOLD  26185  dvply1  26191  vieta1lem2  26219  elqaalem2  26228  dvtaylp  26278  dvntaylp  26279  taylthlem1  26281  taylth  26284  ulmres  26297  ulmshftlem  26298  ulmshft  26299  ulmcau  26304  ulmdvlem1  26309  mtest  26313  mtestbdd  26314  pserulm  26331  psercn2  26332  psercn2OLD  26333  psercnlem1  26335  psercn  26336  pserdvlem2  26338  abelthlem6  26346  abelth  26351  efif1olem1  26451  efif1olem3  26453  efif1olem4  26454  logcn  26556  advlogexp  26564  efopn  26567  cxpeq  26667  asinsin  26802  atantayl  26847  leibpilem2  26851  birthdaylem2  26862  birthdaylem3  26863  efrlim  26879  efrlimOLD  26880  emcllem2  26907  emcllem5  26910  emcllem7  26912  harmonicbnd4  26921  fsumharmonic  26922  lgamgulm2  26946  lgamcvglem  26950  lgamcvg2  26965  gamcvg2lem  26969  wilthlem2  26979  wilthlem3  26980  ftalem1  26983  ftalem2  26984  ftalem3  26985  ftalem5  26987  basellem2  26992  basellem3  26993  basellem5  26995  basellem8  26998  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  chpp1  27065  vma1  27076  ppiltx  27087  musum  27101  0sgmppw  27109  1sgmprm  27110  ppiublem2  27114  chtublem  27122  fsumvma2  27125  chpchtsum  27130  logexprlim  27136  bposlem5  27199  lgscllem  27215  lgsval2lem  27218  lgsval4a  27230  lgsneg  27232  lgsdir2lem3  27238  lgsdir2lem5  27240  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  gausslemma2dlem3  27279  lgseisenlem1  27286  lgsquadlem2  27292  chebbnd1lem1  27380  chtppilimlem1  27384  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasum2lem  27407  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0flb  27421  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  mudivsum  27441  mulogsum  27443  mulog2sumlem2  27446  selberg2lem  27461  logdivbnd  27467  pntrsumo1  27476  pntrsumbnd2  27478  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem6a  27493  pntlemj  27514  pntlemf  27516  ostth2lem3  27546  madebdayim  27799  oldbdayim  27800  newbdayim  27814  noseqp1  28185  tglngne  28477  ltgseg  28523  eedimeq  28825  axlowdimlem16  28884  ebtwntg  28909  subgruhgredgd  29211  subumgredg2  29212  umgrres1lem  29237  wlkson  29584  wksonproplem  29632  wksonproplemOLD  29633  trlsonfval  29634  pthsonfval  29670  spthson  29671  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  eupth2lems  30167  numclwwlk1lem2foa  30283  numclwlk1lem2  30299  numclwwlk2lem1  30305  htthlem  30846  hhsscms  31207  shmodsi  31318  pjoc1i  31360  5oalem1  31583  mayete3i  31657  adj1  31862  iundisj2f  32519  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  33193  elrgspnlem2  33194  erler  33216  idomrcanOLD  33232  nsgmgc  33383  nsgqusf1olem2  33385  unitpidl1  33395  elrspunsn  33400  ssdifidllem  33427  mxidlirredi  33442  mxidlirred  33443  opprqusplusg  33460  opprqus0g  33461  opprqusmulr  33462  idlsrgmulrss1  33482  idlsrgmulrss2  33483  rprmcl  33489  rprmdvds  33490  rprmnz  33491  rprmnunit  33492  rprmasso  33496  rprmirredb  33503  pidufd  33514  1arithufdlem2  33516  1arithufdlem3  33517  zringfrac  33525  ply1dg3rt0irred  33551  m1pmeq  33552  ig1pmindeg  33567  exsslsb  33592  ply1degltdimlem  33618  lindsun  33621  fldextfld1  33643  fldextfld2  33644  rtelextdg2  33717  cos9thpiminplylem1  33772  1smat1  33794  submateqlem2  33798  lmatfval  33804  mdetlap1  33816  madjusmdetlem1  33817  madjusmdetlem2  33818  madjusmdetlem3  33819  madjusmdetlem4  33820  zarclssn  33863  zartopn  33865  zarmxt1  33870  rhmpreimacnlem  33874  rhmpreimacn  33875  pnfneige0  33941  pl1cn  33945  rrhqima  34004  esumfzf  34059  esumpcvgval  34068  esumpmono  34069  esumcvg  34076  ldgenpisyslem1  34153  ldgenpisys  34156  measbase  34187  dya2iocnei  34273  oddpwdc  34345  eulerpartlems  34351  eulerpartlemb  34359  sseqf  34383  fibp1  34392  orrvcval4  34456  orrvcoel  34457  orrvccel  34458  ballotlem2  34480  ballotlemfrceq  34520  signsplypnf  34541  signswch  34552  signstf0  34559  signstfvn  34560  signstfvneq0  34563  signstfvcl  34564  signstfveq0  34568  signsvfn  34573  fct2relem  34588  fsum2dsub  34598  reprsuc  34606  reprpmtf1o  34617  breprexplema  34621  breprexplemc  34623  hgt749d  34640  hgt750lemb  34647  tgoldbachgnn  34650  bnj1172  34991  bnj1245  35004  bnj1311  35014  bnj1450  35040  bnj1501  35057  subfacp1lem1  35166  subfacp1lem5  35171  subfacp1lem6  35172  subfacval2  35174  erdszelem7  35184  cvxpconn  35229  cvxsconn  35230  cvmliftlem5  35276  cvmliftlem7  35278  cvmliftlem10  35281  cvmliftlem13  35283  mrsubvrs  35509  msubrn  35516  msubco  35518  msubvrs  35547  r1peuqusdeg1  35630  imageval  35918  fwddifnp1  36153  knoppcnlem8  36488  knoppcnlem10  36490  bj-unirel  37039  icoreunrn  37347  istoprelowl  37348  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  mblfinlem2  37652  ftc1cnnc  37686  upixp  37723  sdclem2  37736  caushft  37755  ismtyres  37802  rrnmet  37823  rrndstprj1  37824  rrndstprj2  37825  rrncmslem  37826  rrnequiv  37829  iccbnd  37834  osumcllem7N  39956  pexmidlem4N  39967  lcfrlem4  41539  lcfrlem5  41540  lcfrlem6  41541  lcfrlem16  41552  lcfrlem38  41574  mapdrvallem2  41639  mapdh8ab  41771  mapdh8ad  41773  mapdh8e  41778  3factsumint3  42011  aks4d1p1p1  42051  fldhmf1  42078  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p7  42101  aks6d1c1p6  42102  aks6d1c1p8  42103  aks6d1c1  42104  evl1gprodd  42105  idomnnzpownz  42120  aks6d1c5lem1  42124  aks6d1c5lem3  42125  aks6d1c5lem2  42126  deg1gprod  42128  sticksstones10  42143  aks6d1c6lem3  42160  aks5lem2  42175  aks5lem3a  42177  unitscyglem5  42187  fz1sump1  42298  sumcubes  42301  evlselv  42575  mhphf2  42586  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  mapfzcons  42704  diophren  42801  irrapxlem1  42810  monotuz  42930  acongeq  42972  jm2.26lem3  42990  jm3.1lem2  43007  pw2f1ocnv  43026  idomodle  43180  trclfvdecomr  43717  imo72b2lem0  44154  imo72b2lem1  44158  scottelrankd  44236  dvgrat  44301  cvgdvgrat  44302  hashnzfz2  44310  fcnre  45019  refsumcn  45024  rfcnnnub  45030  disjf1o  45185  disjinfi  45186  ssmapsn  45210  ssuzfz  45345  nnsplit  45354  uzssd2  45413  uzublem  45426  fsumsermpt  45577  climsuselem1  45605  limcperiod  45626  sumnnodd  45628  lptioo2cn  45643  lptioo1cn  45644  climresmpt  45657  allbutfifvre  45673  climleltrp  45674  cnrefiisplem  45827  cncfshift  45872  cncfperiod  45877  cncfshiftioo  45890  fperdvper  45917  dvnmptdivc  45936  dvnmul  45941  dvmptfprod  45943  dvnprodlem3  45946  stoweidlem11  46009  stoweidlem15  46013  stoweidlem17  46015  stoweidlem20  46018  stoweidlem34  46032  stoweidlem35  46033  stoweidlem46  46044  stoweidlem47  46045  stoweidlem56  46054  stoweidlem59  46057  stoweidlem62  46060  stirlinglem5  46076  stirlinglem14  46085  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  fourierdlem11  46116  fourierdlem15  46120  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem25  46130  fourierdlem48  46152  fourierdlem52  46156  fourierdlem54  46158  fourierdlem58  46162  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem69  46173  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem80  46184  fourierdlem81  46185  fourierdlem83  46187  fourierdlem92  46196  fourierdlem93  46197  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  fouriercnp  46224  fouriersw  46229  elaa2lem  46231  etransclem4  46236  etransclem7  46239  etransclem10  46242  etransclem14  46246  etransclem15  46247  etransclem24  46256  etransclem25  46257  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem44  46276  etransclem46  46278  qndenserrnopnlem  46295  qndenserrn  46297  prsal  46316  salgencntex  46341  subsaliuncl  46356  subsalsal  46357  sge0tsms  46378  sge0fodjrnlem  46414  sge0isum  46425  iundjiunlem  46457  iundjiun  46458  meadjiunlem  46463  meaiunlelem  46466  meaiuninclem  46478  meaiininc2  46486  caragensplit  46498  carageneld  46500  carageniuncllem1  46519  caratheodorylem1  46524  caratheodorylem2  46525  hoicvr  46546  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem2  46594  hoiqssbllem2  46621  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  smflimlem3  46771  smfmullem4  46792  smfsupxr  46814  smflimsuplem2  46819  smflimsuplem5  46822  ormklocald  46872  natlocalincr  46874  elmod2  47356  isuspgrim0lem  47893  upgrimtrlslem2  47905  ssnn0ssfz  48337  zlmodzxzscm  48345  rmsupp0  48356  lincsum  48418  lincscm  48419  lindslinindimp2lem4  48450  lincresunit3  48470  elbigofrcl  48539  intubeu  48972  unilbeu  48973  cicrcl2  49032  cic1st2nd  49036  imaf1homlem  49096  oppfrcl  49117  eloppf  49122  imasubc  49140  imaid  49143  oppcuprcl5  49190  oppcup3  49198  uptrlem2  49200  uptrlem3  49201  natoppf  49218  elxpcbasex1ALT  49238  elxpcbasex2ALT  49240  swapf1a  49258  swapf2f1oa  49266  swapfida  49269  cofuswapf1  49283  cofuswapf2  49284  fucoppcco  49398  postc  49558  reldmlan2  49606  reldmran2  49607  lanrcl  49610  ranrcl  49611  setrec1  49680  aacllem  49790