Theorem eleqtrdi 2839

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 2831	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 2702

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

This theorem is referenced by:  eleqtrrdi  2840  3eltr3g  2845  prid2g  4728  ndmfvrcl  6897  fnwelem  8113  tz7.48-1  8414  brwitnlem  8474  oeeulem  8568  dffi3  9389  cnfcom3lem  9663  ttrclse  9687  alephgeom  10042  fpwwe2lem5  10595  canthwelem  10610  hargch  10633  r1wunlim  10697  eluzel2  12805  fseq1p1m1  13566  fznn0sub2  13603  nn0split  13611  seqp1d  13990  exple1  14149  digit1  14209  bcval5  14290  bcpasc  14293  hashf1  14429  seqcoll  14436  seqcoll2  14437  ccatrn  14561  swrdccat2  14641  cats1un  14693  pfxccatin12lem3  14704  splfv2a  14728  splval2  14729  caubnd  15332  limsupgre  15454  clim2ser  15628  clim2ser2  15629  iserex  15630  isermulc2  15631  iserle  15633  iserge0  15634  climub  15635  climserle  15636  isercolllem2  15639  isercolllem3  15640  isercoll  15641  isercoll2  15642  serf0  15654  iseraltlem2  15656  iseraltlem3  15657  iseralt  15658  sumeq2ii  15666  summolem3  15687  summolem2a  15688  fsum  15693  sum0  15694  fsumcl2lem  15704  fsumadd  15713  isumclim3  15732  isumadd  15740  fsump1i  15742  fsummulc2  15757  fsumrelem  15780  iserabs  15788  cvgcmp  15789  cvgcmpub  15790  cvgcmpce  15791  binom1dif  15806  isumshft  15812  isumsplit  15813  isumrpcl  15816  isumsup2  15819  climcndslem1  15822  climcndslem2  15823  climcnds  15824  arisum2  15834  trireciplem  15835  geoser  15840  pwdif  15841  geolim  15843  geo2lim  15848  cvgrat  15856  mertenslem1  15857  mertenslem2  15858  mertens  15859  clim2prod  15861  clim2div  15862  ntrivcvgfvn0  15872  ntrivcvgtail  15873  prodeq2ii  15884  prodmolem3  15906  prodmolem2a  15907  fprod  15914  fprodntriv  15915  fprodss  15921  fprodser  15922  fprodcl2lem  15923  fprodmul  15933  fproddiv  15934  fprodabs  15947  fprodeq0  15948  fprodn0  15952  iprodclim3  15973  iprodmul  15976  fallfacfwd  16009  0fallfac  16010  binomfallfaclem2  16013  fallfacval4  16016  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  efcvgfsum  16059  efcj  16065  fprodefsum  16068  effsumlt  16086  ruclem7  16211  bitsfzolem  16411  bitsfzo  16412  bitsfi  16414  bitsinv1lem  16418  bitsinv1  16419  bitsinvp1  16426  sadcp1  16432  sadadd  16444  sadass  16448  bitsres  16450  smupp1  16457  smuval2  16459  smupval  16465  smueqlem  16467  smumul  16470  algrp1  16551  phiprmpw  16753  crth  16755  phimullem  16756  eulerthlem2  16759  prmdiv  16762  pcpremul  16821  pcmpt  16870  pcfac  16877  pockthlem  16883  pockthg  16884  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  prmrec  16900  1arith  16905  vdwapun  16952  vdwlem1  16959  vdwlem2  16960  vdwlem3  16961  vdwlem6  16964  vdwlem8  16966  vdwlem10  16968  vdw  16972  imasvscafn  17507  oppccatid  17687  oppccomfpropd  17695  brcic  17767  funcoppc  17844  invfuc  17946  hofcl  18227  yonedalem4c  18245  gsumwsubmcl  18771  gsumsgrpccat  18774  gsumwmhm  18779  mulgnnp1  19021  mulgnnsubcl  19025  mulgnn0z  19040  mulgnndir  19042  ghmquskerlem1  19222  ghmquskerco  19223  psgnunilem4  19434  psgnran  19452  sylow1lem1  19535  lsmmod2  19613  lsmdisj2r  19622  efginvrel2  19664  efgsdmi  19669  efgsrel  19671  efgs1b  19673  efgsp1  19674  efgredleme  19680  efgredlemc  19682  efgcpbllemb  19692  frgpuplem  19709  mulgnn0di  19762  frgpnabllem1  19810  lt6abl  19832  cycsubgcyg  19838  gsumval3eu  19841  gsumval3  19844  gsumzcl2  19847  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsumzoppg  19881  telgsumfz0s  19928  dprdwd  19950  dprd2da  19981  pgpfaclem1  20020  srgbinom  20147  isirred  20335  idomdomd  20642  idomcringd  20643  lspprid2  20911  lspsnat  21062  lsppratlem1  21064  lsppratlem3  21066  lidl0cl  21137  lidlacl  21138  lidlnegcl  21139  elrspsn  21157  2idllidld  21171  2idlridld  21172  rng2idl1cntr  21222  psgnghm  21496  frlmvscavalb  21686  frlmvplusgscavalb  21687  psrbaglefi  21842  psrass23l  21883  psrass23  21885  mplcoe5lem  21953  mpfind  22021  selvval  22029  mhpvscacl  22048  psr1bascl  22092  ply1basf  22094  gsummoncoe1  22202  lply1binom  22204  lply1binomsc  22205  mpfpf1  22245  pf1mpf  22246  evl1scvarpw  22257  evl1maprhm  22273  matbas2i  22316  matecld  22320  matgsum  22331  mpomatmul  22340  dmatmul  22391  1mavmul  22442  mdetleib2  22482  m1detdiag  22491  marep01ma  22554  smadiadetlem4  22563  slesolinv  22574  pmatcollpw3fi1lem1  22680  chpscmat  22736  chpscmatgsumbin  22738  chp0mat  22740  chpidmat  22741  chfacfisf  22748  chfacfisfcpmat  22749  chfacfpmmulgsum2  22759  cldrcl  22920  ordtbas  23086  iscnp2  23133  dis1stc  23393  ptbasfi  23475  ptpjopn  23506  ptclsg  23509  ptcnp  23516  kqtop  23639  reghmph  23687  ptcmplem2  23947  ptcmplem3  23948  ptcmplem4  23949  tsmslem1  24023  utop2nei  24145  isucn2  24173  cuspcvg  24195  cnextucn  24197  imasdsf1olem  24268  blcvx  24693  xrhmeo  24851  cnrehmeo  24858  cnrehmeoOLD  24859  evth  24865  reparphti  24903  reparphtiOLD  24904  iscau4  25186  iscmet3lem1  25198  lmle  25208  rrxfsupp  25309  rrxdsfi  25318  pjthlem2  25345  ovollb2lem  25396  ovolunlem1a  25404  ovoliunlem1  25410  ovoliun2  25414  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem4  25428  iundisj2  25457  voliunlem1  25458  volsup  25464  ioombl1lem4  25469  uniioovol  25487  uniioombllem3  25493  uniioombllem4  25494  uniioombllem6  25496  vitalilem5  25520  mbfimaopnlem  25563  mbflimsup  25574  mbfi1fseqlem3  25625  iblitg  25676  dvcnp2  25828  dvnp1  25834  cpncn  25845  dvmulbr  25848  dvcobr  25856  dvlip2  25907  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumrlimge0  25944  dvfsumrlim2  25946  ftc1cn  25957  elplyd  26114  ply1termlem  26115  ply1term  26116  ply0  26120  plyeq0lem  26122  plyaddlem1  26125  plymullem1  26126  plyaddlem  26127  plymullem  26128  coeeulem  26136  plyco  26153  coeeq2  26154  coefv0  26160  coemulhi  26166  coemulc  26167  plycj  26190  plycjOLD  26192  dvply1  26198  vieta1lem2  26226  elqaalem2  26235  dvtaylp  26285  dvntaylp  26286  taylthlem1  26288  taylth  26291  ulmres  26304  ulmshftlem  26305  ulmshft  26306  ulmcau  26311  ulmdvlem1  26316  mtest  26320  mtestbdd  26321  pserulm  26338  psercn2  26339  psercn2OLD  26340  psercnlem1  26342  psercn  26343  pserdvlem2  26345  abelthlem6  26353  abelth  26358  efif1olem1  26458  efif1olem3  26460  efif1olem4  26461  logcn  26563  advlogexp  26571  efopn  26574  cxpeq  26674  asinsin  26809  atantayl  26854  leibpilem2  26858  birthdaylem2  26869  birthdaylem3  26870  efrlim  26886  efrlimOLD  26887  emcllem2  26914  emcllem5  26917  emcllem7  26919  harmonicbnd4  26928  fsumharmonic  26929  lgamgulm2  26953  lgamcvglem  26957  lgamcvg2  26972  gamcvg2lem  26976  wilthlem2  26986  wilthlem3  26987  ftalem1  26990  ftalem2  26991  ftalem3  26992  ftalem5  26994  basellem2  26999  basellem3  27000  basellem5  27002  basellem8  27005  ppiprm  27068  ppinprm  27069  chtprm  27070  chtnprm  27071  chpp1  27072  vma1  27083  ppiltx  27094  musum  27108  0sgmppw  27116  1sgmprm  27117  ppiublem2  27121  chtublem  27129  fsumvma2  27132  chpchtsum  27137  logexprlim  27143  bposlem5  27206  lgscllem  27222  lgsval2lem  27225  lgsval4a  27237  lgsneg  27239  lgsdir2lem3  27245  lgsdir2lem5  27247  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  gausslemma2dlem3  27286  lgseisenlem1  27293  lgsquadlem2  27299  chebbnd1lem1  27387  chtppilimlem1  27391  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrmusum2  27412  dchrvmasum2lem  27414  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0flb  27428  dchrisum0re  27431  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  mudivsum  27448  mulogsum  27450  mulog2sumlem2  27453  selberg2lem  27468  logdivbnd  27474  pntrsumo1  27483  pntrsumbnd2  27485  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem6a  27500  pntlemj  27521  pntlemf  27523  ostth2lem3  27553  madebdayim  27806  oldbdayim  27807  newbdayim  27821  noseqp1  28192  tglngne  28484  ltgseg  28530  eedimeq  28832  axlowdimlem16  28891  ebtwntg  28916  subgruhgredgd  29218  subumgredg2  29219  umgrres1lem  29244  wlkson  29591  wksonproplem  29639  wksonproplemOLD  29640  trlsonfval  29641  pthsonfval  29677  spthson  29678  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  eupth2lems  30174  numclwwlk1lem2foa  30290  numclwlk1lem2  30306  numclwwlk2lem1  30312  htthlem  30853  hhsscms  31214  shmodsi  31325  pjoc1i  31367  5oalem1  31590  mayete3i  31664  adj1  31869  iundisj2f  32526  fmptco1f1o  32564  fcnvgreu  32604  suppovss  32611  ssnnssfz  32717  iundisj2fi  32727  indpreima  32795  ccatws1f1o  32880  cshw1s2  32889  chnccats1  32948  gsumhashmul  33008  gsumwrd2dccat  33014  fzo0pmtrlast  33056  wrdpmtrlast  33057  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1st1  33066  cycpmfv1  33077  cycpmfv2  33078  cycpmco2rn  33089  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cyc3evpm  33114  cyc3genpm  33116  cycpmconjslem2  33119  cyc3conja  33121  elrgspnlem1  33200  elrgspnlem2  33201  erler  33223  idomrcanOLD  33239  nsgmgc  33390  nsgqusf1olem2  33392  unitpidl1  33402  elrspunsn  33407  ssdifidllem  33434  mxidlirredi  33449  mxidlirred  33450  opprqusplusg  33467  opprqus0g  33468  opprqusmulr  33469  idlsrgmulrss1  33489  idlsrgmulrss2  33490  rprmcl  33496  rprmdvds  33497  rprmnz  33498  rprmnunit  33499  rprmasso  33503  rprmirredb  33510  pidufd  33521  1arithufdlem2  33523  1arithufdlem3  33524  zringfrac  33532  ply1dg3rt0irred  33558  m1pmeq  33559  ig1pmindeg  33574  exsslsb  33599  ply1degltdimlem  33625  lindsun  33628  fldextfld1  33650  fldextfld2  33651  rtelextdg2  33724  cos9thpiminplylem1  33779  1smat1  33801  submateqlem2  33805  lmatfval  33811  mdetlap1  33823  madjusmdetlem1  33824  madjusmdetlem2  33825  madjusmdetlem3  33826  madjusmdetlem4  33827  zarclssn  33870  zartopn  33872  zarmxt1  33877  rhmpreimacnlem  33881  rhmpreimacn  33882  pnfneige0  33948  pl1cn  33952  rrhqima  34011  esumfzf  34066  esumpcvgval  34075  esumpmono  34076  esumcvg  34083  ldgenpisyslem1  34160  ldgenpisys  34163  measbase  34194  dya2iocnei  34280  oddpwdc  34352  eulerpartlems  34358  eulerpartlemb  34366  sseqf  34390  fibp1  34399  orrvcval4  34463  orrvcoel  34464  orrvccel  34465  ballotlem2  34487  ballotlemfrceq  34527  signsplypnf  34548  signswch  34559  signstf0  34566  signstfvn  34567  signstfvneq0  34570  signstfvcl  34571  signstfveq0  34575  signsvfn  34580  fct2relem  34595  fsum2dsub  34605  reprsuc  34613  reprpmtf1o  34624  breprexplema  34628  breprexplemc  34630  hgt749d  34647  hgt750lemb  34654  tgoldbachgnn  34657  bnj1172  34998  bnj1245  35011  bnj1311  35021  bnj1450  35047  bnj1501  35064  subfacp1lem1  35173  subfacp1lem5  35178  subfacp1lem6  35179  subfacval2  35181  erdszelem7  35191  cvxpconn  35236  cvxsconn  35237  cvmliftlem5  35283  cvmliftlem7  35285  cvmliftlem10  35288  cvmliftlem13  35290  mrsubvrs  35516  msubrn  35523  msubco  35525  msubvrs  35554  r1peuqusdeg1  35637  imageval  35925  fwddifnp1  36160  knoppcnlem8  36495  knoppcnlem10  36497  bj-unirel  37046  icoreunrn  37354  istoprelowl  37355  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  mblfinlem2  37659  ftc1cnnc  37693  upixp  37730  sdclem2  37743  caushft  37762  ismtyres  37809  rrnmet  37830  rrndstprj1  37831  rrndstprj2  37832  rrncmslem  37833  rrnequiv  37836  iccbnd  37841  osumcllem7N  39963  pexmidlem4N  39974  lcfrlem4  41546  lcfrlem5  41547  lcfrlem6  41548  lcfrlem16  41559  lcfrlem38  41581  mapdrvallem2  41646  mapdh8ab  41778  mapdh8ad  41780  mapdh8e  41785  3factsumint3  42018  aks4d1p1p1  42058  fldhmf1  42085  aks6d1c1p2  42104  aks6d1c1p3  42105  aks6d1c1p7  42108  aks6d1c1p6  42109  aks6d1c1p8  42110  aks6d1c1  42111  evl1gprodd  42112  idomnnzpownz  42127  aks6d1c5lem1  42131  aks6d1c5lem3  42132  aks6d1c5lem2  42133  deg1gprod  42135  sticksstones10  42150  aks6d1c6lem3  42167  aks5lem2  42182  aks5lem3a  42184  unitscyglem5  42194  fz1sump1  42305  sumcubes  42308  evlselv  42582  mhphf2  42593  prjspnfv01  42619  prjspner01  42620  prjspner1  42621  mapfzcons  42711  diophren  42808  irrapxlem1  42817  monotuz  42937  acongeq  42979  jm2.26lem3  42997  jm3.1lem2  43014  pw2f1ocnv  43033  idomodle  43187  trclfvdecomr  43724  imo72b2lem0  44161  imo72b2lem1  44165  scottelrankd  44243  dvgrat  44308  cvgdvgrat  44309  hashnzfz2  44317  fcnre  45026  refsumcn  45031  rfcnnnub  45037  disjf1o  45192  disjinfi  45193  ssmapsn  45217  ssuzfz  45352  nnsplit  45361  uzssd2  45420  uzublem  45433  fsumsermpt  45584  climsuselem1  45612  limcperiod  45633  sumnnodd  45635  lptioo2cn  45650  lptioo1cn  45651  climresmpt  45664  allbutfifvre  45680  climleltrp  45681  cnrefiisplem  45834  cncfshift  45879  cncfperiod  45884  cncfshiftioo  45897  fperdvper  45924  dvnmptdivc  45943  dvnmul  45948  dvmptfprod  45950  dvnprodlem3  45953  stoweidlem11  46016  stoweidlem15  46020  stoweidlem17  46022  stoweidlem20  46025  stoweidlem34  46039  stoweidlem35  46040  stoweidlem46  46051  stoweidlem47  46052  stoweidlem56  46061  stoweidlem59  46064  stoweidlem62  46067  stirlinglem5  46083  stirlinglem14  46092  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  fourierdlem11  46123  fourierdlem15  46127  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem25  46137  fourierdlem48  46159  fourierdlem52  46163  fourierdlem54  46165  fourierdlem58  46169  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem69  46180  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem80  46191  fourierdlem81  46192  fourierdlem83  46194  fourierdlem92  46203  fourierdlem93  46204  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  fouriercnp  46231  fouriersw  46236  elaa2lem  46238  etransclem4  46243  etransclem7  46246  etransclem10  46249  etransclem14  46253  etransclem15  46254  etransclem24  46263  etransclem25  46264  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem44  46283  etransclem46  46285  qndenserrnopnlem  46302  qndenserrn  46304  prsal  46323  salgencntex  46348  subsaliuncl  46363  subsalsal  46364  sge0tsms  46385  sge0fodjrnlem  46421  sge0isum  46432  iundjiunlem  46464  iundjiun  46465  meadjiunlem  46470  meaiunlelem  46473  meaiuninclem  46485  meaiininc2  46493  caragensplit  46505  carageneld  46507  carageniuncllem1  46526  caratheodorylem1  46531  caratheodorylem2  46532  hoicvr  46553  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem2  46601  hoiqssbllem2  46628  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  smflimlem3  46778  smfmullem4  46799  smfsupxr  46821  smflimsuplem2  46826  smflimsuplem5  46829  ormklocald  46879  natlocalincr  46881  elmod2  47360  isuspgrim0lem  47897  upgrimtrlslem2  47909  ssnn0ssfz  48341  zlmodzxzscm  48349  rmsupp0  48360  lincsum  48422  lincscm  48423  lindslinindimp2lem4  48454  lincresunit3  48474  elbigofrcl  48543  intubeu  48976  unilbeu  48977  cicrcl2  49036  cic1st2nd  49040  imaf1homlem  49100  oppfrcl  49121  eloppf  49126  imasubc  49144  imaid  49147  oppcuprcl5  49194  oppcup3  49202  uptrlem2  49204  uptrlem3  49205  natoppf  49222  elxpcbasex1ALT  49242  elxpcbasex2ALT  49244  swapf1a  49262  swapf2f1oa  49270  swapfida  49273  cofuswapf1  49287  cofuswapf2  49288  fucoppcco  49402  postc  49562  reldmlan2  49610  reldmran2  49611  lanrcl  49614  ranrcl  49615  setrec1  49684  aacllem  49794