Theorem eleqtrdi 2851

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 2843	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 2708

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

This theorem is referenced by:  eleqtrrdi  2852  3eltr3g  2857  prid2g  4761  ndmfvrcl  6942  fnwelem  8156  tz7.48-1  8483  brwitnlem  8545  oeeulem  8639  dffi3  9471  cnfcom3lem  9743  ttrclse  9767  alephgeom  10122  fpwwe2lem5  10675  canthwelem  10690  hargch  10713  r1wunlim  10777  eluzel2  12883  fseq1p1m1  13638  fznn0sub2  13675  nn0split  13683  seqp1d  14059  exple1  14216  digit1  14276  bcval5  14357  bcpasc  14360  hashf1  14496  seqcoll  14503  seqcoll2  14504  ccatrn  14627  swrdccat2  14707  cats1un  14759  pfxccatin12lem3  14770  splfv2a  14794  splval2  14795  caubnd  15397  limsupgre  15517  clim2ser  15691  clim2ser2  15692  iserex  15693  isermulc2  15694  iserle  15696  iserge0  15697  climub  15698  climserle  15699  isercolllem2  15702  isercolllem3  15703  isercoll  15704  isercoll2  15705  serf0  15717  iseraltlem2  15719  iseraltlem3  15720  iseralt  15721  sumeq2ii  15729  summolem3  15750  summolem2a  15751  fsum  15756  sum0  15757  fsumcl2lem  15767  fsumadd  15776  isumclim3  15795  isumadd  15803  fsump1i  15805  fsummulc2  15820  fsumrelem  15843  iserabs  15851  cvgcmp  15852  cvgcmpub  15853  cvgcmpce  15854  binom1dif  15869  isumshft  15875  isumsplit  15876  isumrpcl  15879  isumsup2  15882  climcndslem1  15885  climcndslem2  15886  climcnds  15887  arisum2  15897  trireciplem  15898  geoser  15903  pwdif  15904  geolim  15906  geo2lim  15911  cvgrat  15919  mertenslem1  15920  mertenslem2  15921  mertens  15922  clim2prod  15924  clim2div  15925  ntrivcvgfvn0  15935  ntrivcvgtail  15936  prodeq2ii  15947  prodmolem3  15969  prodmolem2a  15970  fprod  15977  fprodntriv  15978  fprodss  15984  fprodser  15985  fprodcl2lem  15986  fprodmul  15996  fproddiv  15997  fprodabs  16010  fprodeq0  16011  fprodn0  16015  iprodclim3  16036  iprodmul  16039  fallfacfwd  16072  0fallfac  16073  binomfallfaclem2  16076  fallfacval4  16079  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  efcvgfsum  16122  efcj  16128  fprodefsum  16131  effsumlt  16147  ruclem7  16272  bitsfzolem  16471  bitsfzo  16472  bitsfi  16474  bitsinv1lem  16478  bitsinv1  16479  bitsinvp1  16486  sadcp1  16492  sadadd  16504  sadass  16508  bitsres  16510  smupp1  16517  smuval2  16519  smupval  16525  smueqlem  16527  smumul  16530  algrp1  16611  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  17582  oppccatid  17762  oppccomfpropd  17770  brcic  17842  funcoppc  17920  invfuc  18022  hofcl  18304  yonedalem4c  18322  gsumwsubmcl  18850  gsumsgrpccat  18853  gsumwmhm  18858  mulgnnp1  19100  mulgnnsubcl  19104  mulgnn0z  19119  mulgnndir  19121  ghmquskerlem1  19301  ghmquskerco  19302  psgnunilem4  19515  psgnran  19533  sylow1lem1  19616  lsmmod2  19694  lsmdisj2r  19703  efginvrel2  19745  efgsdmi  19750  efgsrel  19752  efgs1b  19754  efgsp1  19755  efgredleme  19761  efgredlemc  19763  efgcpbllemb  19773  frgpuplem  19790  mulgnn0di  19843  frgpnabllem1  19891  lt6abl  19913  cycsubgcyg  19919  gsumval3eu  19922  gsumval3  19925  gsumzcl2  19928  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsumzoppg  19962  telgsumfz0s  20009  dprdwd  20031  dprd2da  20062  pgpfaclem1  20101  srgbinom  20228  isirred  20419  idomdomd  20726  idomcringd  20727  lspprid2  20996  lspsnat  21147  lsppratlem1  21149  lsppratlem3  21151  lidl0cl  21230  lidlacl  21231  lidlnegcl  21232  elrspsn  21250  2idllidld  21264  2idlridld  21265  rng2idl1cntr  21315  psgnghm  21598  frlmvscavalb  21790  frlmvplusgscavalb  21791  psrbaglefi  21946  psrass23l  21987  psrass23  21989  mplcoe5lem  22057  mpfind  22131  selvval  22139  mhpvscacl  22158  psr1bascl  22202  ply1basf  22204  gsummoncoe1  22312  lply1binom  22314  lply1binomsc  22315  mpfpf1  22355  pf1mpf  22356  evl1scvarpw  22367  evl1maprhm  22383  matbas2i  22428  matecld  22432  matgsum  22443  mpomatmul  22452  dmatmul  22503  1mavmul  22554  mdetleib2  22594  m1detdiag  22603  marep01ma  22666  smadiadetlem4  22675  slesolinv  22686  pmatcollpw3fi1lem1  22792  chpscmat  22848  chpscmatgsumbin  22850  chp0mat  22852  chpidmat  22853  chfacfisf  22860  chfacfisfcpmat  22861  chfacfpmmulgsum2  22871  cldrcl  23034  ordtbas  23200  iscnp2  23247  dis1stc  23507  ptbasfi  23589  ptpjopn  23620  ptclsg  23623  ptcnp  23630  kqtop  23753  reghmph  23801  ptcmplem2  24061  ptcmplem3  24062  ptcmplem4  24063  tsmslem1  24137  utop2nei  24259  isucn2  24288  cuspcvg  24310  cnextucn  24312  imasdsf1olem  24383  blcvx  24819  xrhmeo  24977  cnrehmeo  24984  cnrehmeoOLD  24985  evth  24991  reparphti  25029  reparphtiOLD  25030  iscau4  25313  iscmet3lem1  25325  lmle  25335  rrxfsupp  25436  rrxdsfi  25445  pjthlem2  25472  ovollb2lem  25523  ovolunlem1a  25531  ovoliunlem1  25537  ovoliun2  25541  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem4  25555  iundisj2  25584  voliunlem1  25585  volsup  25591  ioombl1lem4  25596  uniioovol  25614  uniioombllem3  25620  uniioombllem4  25621  uniioombllem6  25623  vitalilem5  25647  mbfimaopnlem  25690  mbflimsup  25701  mbfi1fseqlem3  25752  iblitg  25803  dvcnp2  25955  dvnp1  25961  cpncn  25972  dvmulbr  25975  dvcobr  25983  dvlip2  26034  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumrlimge0  26071  dvfsumrlim2  26073  ftc1cn  26084  elplyd  26241  ply1termlem  26242  ply1term  26243  ply0  26247  plyeq0lem  26249  plyaddlem1  26252  plymullem1  26253  plyaddlem  26254  plymullem  26255  coeeulem  26263  plyco  26280  coeeq2  26281  coefv0  26287  coemulhi  26293  coemulc  26294  plycj  26317  plycjOLD  26319  dvply1  26325  vieta1lem2  26353  elqaalem2  26362  dvtaylp  26412  dvntaylp  26413  taylthlem1  26415  taylth  26418  ulmres  26431  ulmshftlem  26432  ulmshft  26433  ulmcau  26438  ulmdvlem1  26443  mtest  26447  mtestbdd  26448  pserulm  26465  psercn2  26466  psercn2OLD  26467  psercnlem1  26469  psercn  26470  pserdvlem2  26472  abelthlem6  26480  abelth  26485  efif1olem1  26584  efif1olem3  26586  efif1olem4  26587  logcn  26689  advlogexp  26697  efopn  26700  cxpeq  26800  asinsin  26935  atantayl  26980  leibpilem2  26984  birthdaylem2  26995  birthdaylem3  26996  efrlim  27012  efrlimOLD  27013  emcllem2  27040  emcllem5  27043  emcllem7  27045  harmonicbnd4  27054  fsumharmonic  27055  lgamgulm2  27079  lgamcvglem  27083  lgamcvg2  27098  gamcvg2lem  27102  wilthlem2  27112  wilthlem3  27113  ftalem1  27116  ftalem2  27117  ftalem3  27118  ftalem5  27120  basellem2  27125  basellem3  27126  basellem5  27128  basellem8  27131  ppiprm  27194  ppinprm  27195  chtprm  27196  chtnprm  27197  chpp1  27198  vma1  27209  ppiltx  27220  musum  27234  0sgmppw  27242  1sgmprm  27243  ppiublem2  27247  chtublem  27255  fsumvma2  27258  chpchtsum  27263  logexprlim  27269  bposlem5  27332  lgscllem  27348  lgsval2lem  27351  lgsval4a  27363  lgsneg  27365  lgsdir2lem3  27371  lgsdir2lem5  27373  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  gausslemma2dlem3  27412  lgseisenlem1  27419  lgsquadlem2  27425  chebbnd1lem1  27513  chtppilimlem1  27517  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasum2lem  27540  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0flb  27554  dchrisum0re  27557  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  mudivsum  27574  mulogsum  27576  mulog2sumlem2  27579  selberg2lem  27594  logdivbnd  27600  pntrsumo1  27609  pntrsumbnd2  27611  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem6a  27626  pntlemj  27647  pntlemf  27649  ostth2lem3  27679  madebdayim  27926  oldbdayim  27927  noseqp1  28297  tglngne  28558  ltgseg  28604  eedimeq  28913  axlowdimlem16  28972  ebtwntg  28997  subgruhgredgd  29301  subumgredg2  29302  umgrres1lem  29327  wlkson  29674  wksonproplem  29722  wksonproplemOLD  29723  trlsonfval  29724  pthsonfval  29760  spthson  29761  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  eupth2lems  30257  numclwwlk1lem2foa  30373  numclwlk1lem2  30389  numclwwlk2lem1  30395  htthlem  30936  hhsscms  31297  shmodsi  31408  pjoc1i  31450  5oalem1  31673  mayete3i  31747  adj1  31952  iundisj2f  32603  fmptco1f1o  32643  fcnvgreu  32683  suppovss  32690  ssnnssfz  32789  iundisj2fi  32799  indpreima  32850  ccatws1f1o  32936  cshw1s2  32945  chnccats1  33005  gsumhashmul  33064  gsumwrd2dccat  33070  fzo0pmtrlast  33112  wrdpmtrlast  33113  pmtrto1cl  33119  psgnfzto1stlem  33120  fzto1st1  33122  cycpmfv1  33133  cycpmfv2  33134  cycpmco2rn  33145  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cyc3evpm  33170  cyc3genpm  33172  cycpmconjslem2  33175  cyc3conja  33177  elrgspnlem1  33246  elrgspnlem2  33247  erler  33269  idomrcanOLD  33285  nsgmgc  33440  nsgqusf1olem2  33442  unitpidl1  33452  elrspunsn  33457  ssdifidllem  33484  mxidlirredi  33499  mxidlirred  33500  opprqusplusg  33517  opprqus0g  33518  opprqusmulr  33519  idlsrgmulrss1  33539  idlsrgmulrss2  33540  rprmcl  33546  rprmdvds  33547  rprmnz  33548  rprmnunit  33549  rprmasso  33553  rprmirredb  33560  pidufd  33571  1arithufdlem2  33573  1arithufdlem3  33574  zringfrac  33582  ply1dg3rt0irred  33607  m1pmeq  33608  ig1pmindeg  33622  exsslsb  33647  ply1degltdimlem  33673  lindsun  33676  fldextfld1  33700  fldextfld2  33701  rtelextdg2  33768  1smat1  33803  submateqlem2  33807  lmatfval  33813  mdetlap1  33825  madjusmdetlem1  33826  madjusmdetlem2  33827  madjusmdetlem3  33828  madjusmdetlem4  33829  zarclssn  33872  zartopn  33874  zarmxt1  33879  rhmpreimacnlem  33883  rhmpreimacn  33884  pnfneige0  33950  pl1cn  33954  rrhqima  34015  esumfzf  34070  esumpcvgval  34079  esumpmono  34080  esumcvg  34087  ldgenpisyslem1  34164  ldgenpisys  34167  measbase  34198  dya2iocnei  34284  oddpwdc  34356  eulerpartlems  34362  eulerpartlemb  34370  sseqf  34394  fibp1  34403  orrvcval4  34467  orrvcoel  34468  orrvccel  34469  ballotlem2  34491  ballotlemfrceq  34531  signsplypnf  34565  signswch  34576  signstf0  34583  signstfvn  34584  signstfvneq0  34587  signstfvcl  34588  signstfveq0  34592  signsvfn  34597  fct2relem  34612  fsum2dsub  34622  reprsuc  34630  reprpmtf1o  34641  breprexplema  34645  breprexplemc  34647  hgt749d  34664  hgt750lemb  34671  tgoldbachgnn  34674  bnj1172  35015  bnj1245  35028  bnj1311  35038  bnj1450  35064  bnj1501  35081  subfacp1lem1  35184  subfacp1lem5  35189  subfacp1lem6  35190  subfacval2  35192  erdszelem7  35202  cvxpconn  35247  cvxsconn  35248  cvmliftlem5  35294  cvmliftlem7  35296  cvmliftlem10  35299  cvmliftlem13  35301  mrsubvrs  35527  msubrn  35534  msubco  35536  msubvrs  35565  r1peuqusdeg1  35648  imageval  35931  fwddifnp1  36166  knoppcnlem8  36501  knoppcnlem10  36503  bj-unirel  37052  icoreunrn  37360  istoprelowl  37361  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  mblfinlem2  37665  ftc1cnnc  37699  upixp  37736  sdclem2  37749  caushft  37768  ismtyres  37815  rrnmet  37836  rrndstprj1  37837  rrndstprj2  37838  rrncmslem  37839  rrnequiv  37842  iccbnd  37847  osumcllem7N  39964  pexmidlem4N  39975  lcfrlem4  41547  lcfrlem5  41548  lcfrlem6  41549  lcfrlem16  41560  lcfrlem38  41582  mapdrvallem2  41647  mapdh8ab  41779  mapdh8ad  41781  mapdh8e  41786  3factsumint3  42024  aks4d1p1p1  42064  fldhmf1  42091  aks6d1c1p2  42110  aks6d1c1p3  42111  aks6d1c1p7  42114  aks6d1c1p6  42115  aks6d1c1p8  42116  aks6d1c1  42117  evl1gprodd  42118  idomnnzpownz  42133  aks6d1c5lem1  42137  aks6d1c5lem3  42138  aks6d1c5lem2  42139  deg1gprod  42141  sticksstones10  42156  aks6d1c6lem3  42173  aks5lem2  42188  aks5lem3a  42190  unitscyglem5  42200  metakunt20  42225  fz1sump1  42344  sumcubes  42347  evlselv  42597  mhphf2  42608  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  mapfzcons  42727  diophren  42824  irrapxlem1  42833  monotuz  42953  acongeq  42995  jm2.26lem3  43013  jm3.1lem2  43030  pw2f1ocnv  43049  idomodle  43203  trclfvdecomr  43741  imo72b2lem0  44178  imo72b2lem1  44182  scottelrankd  44266  dvgrat  44331  cvgdvgrat  44332  hashnzfz2  44340  fcnre  45030  refsumcn  45035  rfcnnnub  45041  disjf1o  45196  disjinfi  45197  ssmapsn  45221  ssuzfz  45360  nnsplit  45369  uzssd2  45428  uzublem  45441  fsumsermpt  45594  climsuselem1  45622  limcperiod  45643  sumnnodd  45645  lptioo2cn  45660  lptioo1cn  45661  climresmpt  45674  allbutfifvre  45690  climleltrp  45691  cnrefiisplem  45844  cncfshift  45889  cncfperiod  45894  cncfshiftioo  45907  fperdvper  45934  dvnmptdivc  45953  dvnmul  45958  dvmptfprod  45960  dvnprodlem3  45963  stoweidlem11  46026  stoweidlem15  46030  stoweidlem17  46032  stoweidlem20  46035  stoweidlem34  46049  stoweidlem35  46050  stoweidlem46  46061  stoweidlem47  46062  stoweidlem56  46071  stoweidlem59  46074  stoweidlem62  46077  stirlinglem5  46093  stirlinglem14  46102  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  fourierdlem11  46133  fourierdlem15  46137  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem25  46147  fourierdlem48  46169  fourierdlem52  46173  fourierdlem54  46175  fourierdlem58  46179  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem69  46190  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem80  46201  fourierdlem81  46202  fourierdlem83  46204  fourierdlem92  46213  fourierdlem93  46214  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  fouriercnp  46241  fouriersw  46246  elaa2lem  46248  etransclem4  46253  etransclem7  46256  etransclem10  46259  etransclem14  46263  etransclem15  46264  etransclem24  46273  etransclem25  46274  etransclem31  46280  etransclem32  46281  etransclem35  46284  etransclem44  46293  etransclem46  46295  qndenserrnopnlem  46312  qndenserrn  46314  prsal  46333  salgencntex  46358  subsaliuncl  46373  subsalsal  46374  sge0tsms  46395  sge0fodjrnlem  46431  sge0isum  46442  iundjiunlem  46474  iundjiun  46475  meadjiunlem  46480  meaiunlelem  46483  meaiuninclem  46495  meaiininc2  46503  caragensplit  46515  carageneld  46517  carageniuncllem1  46536  caratheodorylem1  46541  caratheodorylem2  46542  hoicvr  46563  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmvlelem2  46611  hoiqssbllem2  46638  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  smflimlem3  46788  smfmullem4  46809  smfsupxr  46831  smflimsuplem2  46836  smflimsuplem5  46839  ormklocald  46889  natlocalincr  46891  elmod2  47357  isuspgrim0lem  47871  ssnn0ssfz  48265  zlmodzxzscm  48273  rmsupp0  48284  lincsum  48346  lincscm  48347  lindslinindimp2lem4  48378  lincresunit3  48398  elbigofrcl  48471  intubeu  48873  unilbeu  48874  elxpcbasex1ALT  48955  elxpcbasex2ALT  48957  swapf1a  48975  swapf2f1oa  48983  swapfida  48986  cofuswapf1  48994  cofuswapf2  48995  postc  49173  setrec1  49210  aacllem  49320