Theorem eleqtrdi 2900

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eleqtrrdi  2901  3eltr3g  2906  prid2g  4657  ndmfvrcl  6676  fnwelem  7808  tz7.48-1  8062  brwitnlem  8115  oeeulem  8210  dffi3  8879  cnfcom3lem  9150  alephgeom  9493  fpwwe2lem6  10046  canthwelem  10061  hargch  10084  r1wunlim  10148  eluzel2  12236  fseq1p1m1  12976  fznn0sub2  13009  nn0split  13017  seqp1d  13381  exple1  13536  digit1  13594  bcval5  13674  bcpasc  13677  hashf1  13811  seqcoll  13818  seqcoll2  13819  ccatrn  13934  swrdccat2  14022  cats1un  14074  pfxccatin12lem3  14085  splfv2a  14109  splval2  14110  caubnd  14710  limsupgre  14830  clim2ser  15003  clim2ser2  15004  iserex  15005  isermulc2  15006  iserle  15008  iserge0  15009  climub  15010  climserle  15011  isercolllem2  15014  isercolllem3  15015  isercoll  15016  isercoll2  15017  serf0  15029  iseraltlem2  15031  iseraltlem3  15032  iseralt  15033  sumeq2ii  15042  summolem3  15063  summolem2a  15064  fsum  15069  sum0  15070  fsumcl2lem  15080  fsumadd  15088  isumclim3  15106  isumadd  15114  fsump1i  15116  fsummulc2  15131  fsumrelem  15154  iserabs  15162  cvgcmp  15163  cvgcmpub  15164  cvgcmpce  15165  binom1dif  15180  isumshft  15186  isumsplit  15187  isumrpcl  15190  isumsup2  15193  climcndslem1  15196  climcndslem2  15197  climcnds  15198  arisum2  15208  trireciplem  15209  geoser  15214  pwdif  15215  geolim  15218  geo2lim  15223  cvgrat  15231  mertenslem1  15232  mertenslem2  15233  mertens  15234  clim2prod  15236  clim2div  15237  ntrivcvgfvn0  15247  ntrivcvgtail  15248  prodeq2ii  15259  prodmolem3  15279  prodmolem2a  15280  fprod  15287  fprodntriv  15288  fprodss  15294  fprodser  15295  fprodcl2lem  15296  fprodmul  15306  fproddiv  15307  fprodabs  15320  fprodeq0  15321  fprodn0  15325  iprodclim3  15346  iprodmul  15349  fallfacfwd  15382  0fallfac  15383  binomfallfaclem2  15386  fallfacval4  15389  bpolysum  15399  bpolydiflem  15400  fsumkthpow  15402  efcvgfsum  15431  efcj  15437  fprodefsum  15440  effsumlt  15456  ruclem7  15581  bitsfzolem  15773  bitsfzo  15774  bitsfi  15776  bitsinv1lem  15780  bitsinv1  15781  bitsinvp1  15788  sadcp1  15794  sadadd  15806  sadass  15810  bitsres  15812  smupp1  15819  smuval2  15821  smupval  15827  smueqlem  15829  smumul  15832  algrp1  15908  phiprmpw  16103  crth  16105  phimullem  16106  eulerthlem2  16109  prmdiv  16112  pcpremul  16170  pcmpt  16218  pcfac  16225  pockthlem  16231  pockthg  16232  prmreclem2  16243  prmreclem3  16244  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  prmrec  16248  1arith  16253  vdwapun  16300  vdwlem1  16307  vdwlem2  16308  vdwlem3  16309  vdwlem6  16312  vdwlem8  16314  vdwlem10  16316  vdw  16320  imasvscafn  16802  oppccatid  16981  oppccomfpropd  16989  brcic  17060  funcoppc  17137  invfuc  17236  hofcl  17501  yonedalem4c  17519  gsumwsubmcl  17993  gsumsgrpccat  17996  gsumccatOLD  17997  gsumwmhm  18002  mulgnnp1  18228  mulgnnsubcl  18232  mulgnn0z  18246  mulgnndir  18248  psgnunilem4  18617  psgnran  18635  sylow1lem1  18715  lsmmod2  18794  lsmdisj2r  18803  efginvrel2  18845  efgsdmi  18850  efgsrel  18852  efgs1b  18854  efgsp1  18855  efgredleme  18861  efgredlemc  18863  efgcpbllemb  18873  frgpuplem  18890  mulgnn0di  18939  frgpnabllem1  18986  lt6abl  19008  cycsubgcyg  19014  gsumval3eu  19017  gsumval3  19020  gsumzcl2  19023  gsumzaddlem  19034  gsumconst  19047  gsumzmhm  19050  gsumzoppg  19057  telgsumfz0s  19104  dprdwd  19126  dprd2da  19157  pgpfaclem1  19196  srgbinom  19288  isirred  19445  lspprid2  19763  lspsnat  19910  lsppratlem1  19912  lsppratlem3  19914  lidl0cl  19978  lidlacl  19979  lidlnegcl  19980  lidlmcl  19983  psgnghm  20269  frlmvscavalb  20459  frlmvplusgscavalb  20460  psrbaglefi  20610  psrass23l  20646  psrass23  20648  mplcoe5lem  20707  mpfind  20779  selvval  20790  mhpvscacl  20802  psr1bascl  20829  ply1basf  20831  gsummoncoe1  20933  lply1binom  20935  lply1binomsc  20936  mpfpf1  20975  pf1mpf  20976  evl1scvarpw  20987  matbas2i  21027  matecld  21031  matgsum  21042  mpomatmul  21051  dmatmul  21102  1mavmul  21153  mdetleib2  21193  m1detdiag  21202  marep01ma  21265  smadiadetlem4  21274  slesolinv  21285  pmatcollpw3fi1lem1  21391  chpscmat  21447  chpscmatgsumbin  21449  chp0mat  21451  chpidmat  21452  chfacfisf  21459  chfacfisfcpmat  21460  chfacfpmmulgsum2  21470  cldrcl  21631  ordtbas  21797  iscnp2  21844  dis1stc  22104  ptbasfi  22186  ptpjopn  22217  ptclsg  22220  ptcnp  22227  kqtop  22350  reghmph  22398  ptcmplem2  22658  ptcmplem3  22659  ptcmplem4  22660  tsmslem1  22734  utop2nei  22856  isucn2  22885  cuspcvg  22907  cnextucn  22909  imasdsf1olem  22980  blcvx  23403  xrhmeo  23551  cnrehmeo  23558  evth  23564  reparphti  23602  iscau4  23883  iscmet3lem1  23895  lmle  23905  rrxfsupp  24006  rrxdsfi  24015  pjthlem2  24042  ovollb2lem  24092  ovolunlem1a  24100  ovoliunlem1  24106  ovoliun2  24110  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem4  24124  iundisj2  24153  voliunlem1  24154  volsup  24160  ioombl1lem4  24165  uniioovol  24183  uniioombllem3  24189  uniioombllem4  24190  uniioombllem6  24192  vitalilem5  24216  mbfimaopnlem  24259  mbflimsup  24270  mbfi1fseqlem3  24321  iblitg  24372  dvnp1  24528  cpncn  24539  dvlip2  24598  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumrlimge0  24633  dvfsumrlim2  24635  ftc1cn  24646  elplyd  24799  ply1termlem  24800  ply1term  24801  ply0  24805  plyeq0lem  24807  plyaddlem1  24810  plymullem1  24811  plyaddlem  24812  plymullem  24813  coeeulem  24821  plyco  24838  coeeq2  24839  coefv0  24845  coemulhi  24851  coemulc  24852  plycj  24874  dvply1  24880  vieta1lem2  24907  elqaalem2  24916  dvtaylp  24965  dvntaylp  24966  taylthlem1  24968  taylth  24970  ulmres  24983  ulmshftlem  24984  ulmshft  24985  ulmcau  24990  ulmdvlem1  24995  mtest  24999  mtestbdd  25000  pserulm  25017  psercn2  25018  psercnlem1  25020  psercn  25021  pserdvlem2  25023  abelthlem6  25031  abelth  25036  efif1olem1  25134  efif1olem3  25136  efif1olem4  25137  logcn  25238  advlogexp  25246  efopn  25249  cxpeq  25346  asinsin  25478  atantayl  25523  leibpilem2  25527  birthdaylem2  25538  birthdaylem3  25539  efrlim  25555  emcllem2  25582  emcllem5  25585  emcllem7  25587  harmonicbnd4  25596  fsumharmonic  25597  lgamgulm2  25621  lgamcvglem  25625  lgamcvg2  25640  gamcvg2lem  25644  wilthlem2  25654  wilthlem3  25655  ftalem1  25658  ftalem2  25659  ftalem3  25660  ftalem5  25662  basellem2  25667  basellem3  25668  basellem5  25670  basellem8  25673  ppiprm  25736  ppinprm  25737  chtprm  25738  chtnprm  25739  chpp1  25740  vma1  25751  ppiltx  25762  musum  25776  0sgmppw  25782  1sgmprm  25783  ppiublem2  25787  chtublem  25795  fsumvma2  25798  chpchtsum  25803  logexprlim  25809  bposlem5  25872  lgscllem  25888  lgsval2lem  25891  lgsval4a  25903  lgsneg  25905  lgsdir2lem3  25911  lgsdir2lem5  25913  lgsdir  25916  lgsdilem2  25917  lgsdi  25918  lgsne0  25919  gausslemma2dlem3  25952  lgseisenlem1  25959  lgsquadlem2  25965  chebbnd1lem1  26053  chtppilimlem1  26057  rplogsumlem2  26069  rpvmasumlem  26071  dchrisumlem1  26073  dchrisumlem2  26074  dchrmusum2  26078  dchrvmasum2lem  26080  dchrvmasumiflem1  26085  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dchrisum0flb  26094  dchrisum0re  26097  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0lem3  26103  mudivsum  26114  mulogsum  26116  mulog2sumlem2  26119  selberg2lem  26134  logdivbnd  26140  pntrsumo1  26149  pntrsumbnd2  26151  pntrlog2bndlem2  26162  pntrlog2bndlem4  26164  pntrlog2bndlem6a  26166  pntlemj  26187  pntlemf  26189  ostth2lem3  26219  tglngne  26344  ltgseg  26390  eedimeq  26692  axlowdimlem16  26751  ebtwntg  26776  subgruhgredgd  27074  subumgredg2  27075  umgrres1lem  27100  wlkson  27446  wksonproplem  27494  trlsonfval  27495  pthsonfval  27529  spthson  27530  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  eupth2lems  28023  numclwwlk1lem2foa  28139  numclwlk1lem2  28155  numclwwlk2lem1  28161  htthlem  28700  hhsscms  29061  shmodsi  29172  pjoc1i  29214  5oalem1  29437  mayete3i  29511  adj1  29716  iundisj2f  30353  fmptco1f1o  30392  fcnvgreu  30436  suppovss  30443  ssnnssfz  30536  iundisj2fi  30546  cshw1s2  30660  gsumhashmul  30741  pmtrto1cl  30791  psgnfzto1stlem  30792  fzto1st1  30794  cycpmfv1  30805  cycpmfv2  30806  cycpmco2rn  30817  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cyc3evpm  30842  cyc3genpm  30844  cycpmconjslem2  30847  cyc3conja  30849  rspsnel  30987  idlsrgmulrss1  31064  idlsrgmulrss2  31065  lindsun  31109  fldextfld1  31127  fldextfld2  31128  1smat1  31157  submateqlem2  31161  lmatfval  31167  mdetlap1  31179  madjusmdetlem1  31180  madjusmdetlem2  31181  madjusmdetlem3  31182  madjusmdetlem4  31183  zarclssn  31226  zartopn  31228  zarmxt1  31233  rhmpreimacnlem  31237  rhmpreimacn  31238  pnfneige0  31304  pl1cn  31308  rrhqima  31365  indpreima  31394  esumfzf  31438  esumpcvgval  31447  esumpmono  31448  esumcvg  31455  ldgenpisyslem1  31532  ldgenpisys  31535  measbase  31566  dya2iocnei  31650  oddpwdc  31722  eulerpartlems  31728  eulerpartlemb  31736  sseqf  31760  fibp1  31769  orrvcval4  31832  orrvcoel  31833  orrvccel  31834  ballotlem2  31856  ballotlemfrceq  31896  signsplypnf  31930  signswch  31941  signstf0  31948  signstfvn  31949  signstfvneq0  31952  signstfvcl  31953  signstfveq0  31957  signsvfn  31962  fct2relem  31978  fsum2dsub  31988  reprsuc  31996  reprpmtf1o  32007  breprexplema  32011  breprexplemc  32013  hgt749d  32030  hgt750lemb  32037  tgoldbachgnn  32040  bnj1172  32383  bnj1245  32396  bnj1311  32406  bnj1450  32432  bnj1501  32449  subfacp1lem1  32539  subfacp1lem5  32544  subfacp1lem6  32545  subfacval2  32547  erdszelem7  32557  cvxsconn  32603  cvmliftlem5  32649  cvmliftlem7  32651  cvmliftlem10  32654  cvmliftlem13  32656  mrsubvrs  32882  msubrn  32889  msubco  32891  msubvrs  32920  imageval  33504  fwddifnp1  33739  knoppcnlem8  33952  knoppcnlem10  33954  bj-unirel  34468  icoreunrn  34776  istoprelowl  34777  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem12  35069  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  mblfinlem2  35095  ftc1cnnc  35129  upixp  35167  sdclem2  35180  caushft  35199  ismtyres  35246  rrnmet  35267  rrndstprj1  35268  rrndstprj2  35269  rrncmslem  35270  rrnequiv  35273  iccbnd  35278  osumcllem7N  37258  pexmidlem4N  37269  lcfrlem4  38841  lcfrlem5  38842  lcfrlem6  38843  lcfrlem16  38854  lcfrlem38  38876  mapdrvallem2  38941  mapdh8ab  39073  mapdh8ad  39075  mapdh8e  39080  3factsumint3  39311  aks4d1p1p1  39345  metakunt20  39369  mapfzcons  39657  diophren  39754  irrapxlem1  39763  monotuz  39882  acongeq  39924  jm2.26lem3  39942  jm3.1lem2  39959  pw2f1ocnv  39978  idomodle  40140  trclfvdecomr  40429  imo72b2lem1  40874  scottelrankd  40955  dvgrat  41016  cvgdvgrat  41017  hashnzfz2  41025  fcnre  41654  refsumcn  41659  rfcnnnub  41665  disjf1o  41818  disjinfi  41820  ssmapsn  41845  ssuzfz  41981  nnsplit  41990  uzssd2  42054  uzublem  42067  fsumsermpt  42221  climsuselem1  42249  limcperiod  42270  sumnnodd  42272  lptioo2cn  42287  lptioo1cn  42288  climresmpt  42301  allbutfifvre  42317  climleltrp  42318  cnrefiisplem  42471  cncfshift  42516  cncfperiod  42521  cncfshiftioo  42534  fperdvper  42561  dvnmptdivc  42580  dvnmul  42585  dvmptfprod  42587  dvnprodlem3  42590  stoweidlem11  42653  stoweidlem15  42657  stoweidlem17  42659  stoweidlem20  42662  stoweidlem34  42676  stoweidlem35  42677  stoweidlem46  42688  stoweidlem47  42689  stoweidlem56  42698  stoweidlem59  42701  stoweidlem62  42704  stirlinglem5  42720  stirlinglem14  42729  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  fourierdlem11  42760  fourierdlem15  42764  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem25  42774  fourierdlem48  42796  fourierdlem52  42800  fourierdlem54  42802  fourierdlem58  42806  fourierdlem62  42810  fourierdlem64  42812  fourierdlem65  42813  fourierdlem69  42817  fourierdlem70  42818  fourierdlem71  42819  fourierdlem73  42821  fourierdlem80  42828  fourierdlem81  42829  fourierdlem83  42831  fourierdlem92  42840  fourierdlem93  42841  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  fouriercnp  42868  fouriersw  42873  elaa2lem  42875  etransclem4  42880  etransclem7  42883  etransclem10  42886  etransclem14  42890  etransclem15  42891  etransclem24  42900  etransclem25  42901  etransclem31  42907  etransclem32  42908  etransclem35  42911  etransclem44  42920  etransclem46  42922  qndenserrnopnlem  42939  qndenserrn  42941  prsal  42960  salgencntex  42983  subsaliuncl  42998  subsalsal  42999  sge0tsms  43019  sge0fodjrnlem  43055  sge0isum  43066  iundjiunlem  43098  iundjiun  43099  meadjiunlem  43104  meaiunlelem  43107  meaiuninclem  43119  meaiininc2  43127  caragensplit  43139  carageneld  43141  carageniuncllem1  43160  caratheodorylem1  43165  caratheodorylem2  43166  hoicvr  43187  hsphoidmvle2  43224  hsphoidmvle  43225  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmvlelem2  43235  hoiqssbllem2  43262  pimdecfgtioc  43350  pimincfltioc  43351  pimdecfgtioo  43352  pimincfltioo  43353  smflimlem3  43406  smfmullem4  43426  smfsupxr  43447  smflimsuplem2  43452  smflimsuplem5  43455  elmod2  43887  ssnn0ssfz  44751  zlmodzxzscm  44759  rmsupp0  44770  lincsum  44838  lincscm  44839  lindslinindimp2lem4  44870  lincresunit3  44890  elbigofrcl  44964  setrec1  45221  aacllem  45329