Theorem eleqtrdi 2842

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  eleqtrrdi  2843  3eltr3g  2848  prid2g  4765  ndmfvrcl  6927  fnwelem  8120  tz7.48-1  8446  brwitnlem  8510  oeeulem  8604  dffi3  9429  cnfcom3lem  9701  ttrclse  9725  alephgeom  10080  fpwwe2lem5  10633  canthwelem  10648  hargch  10671  r1wunlim  10735  eluzel2  12832  fseq1p1m1  13580  fznn0sub2  13613  nn0split  13621  seqp1d  13988  exple1  14146  digit1  14205  bcval5  14283  bcpasc  14286  hashf1  14423  seqcoll  14430  seqcoll2  14431  ccatrn  14544  swrdccat2  14624  cats1un  14676  pfxccatin12lem3  14687  splfv2a  14711  splval2  14712  caubnd  15310  limsupgre  15430  clim2ser  15606  clim2ser2  15607  iserex  15608  isermulc2  15609  iserle  15611  iserge0  15612  climub  15613  climserle  15614  isercolllem2  15617  isercolllem3  15618  isercoll  15619  isercoll2  15620  serf0  15632  iseraltlem2  15634  iseraltlem3  15635  iseralt  15636  sumeq2ii  15644  summolem3  15665  summolem2a  15666  fsum  15671  sum0  15672  fsumcl2lem  15682  fsumadd  15691  isumclim3  15710  isumadd  15718  fsump1i  15720  fsummulc2  15735  fsumrelem  15758  iserabs  15766  cvgcmp  15767  cvgcmpub  15768  cvgcmpce  15769  binom1dif  15784  isumshft  15790  isumsplit  15791  isumrpcl  15794  isumsup2  15797  climcndslem1  15800  climcndslem2  15801  climcnds  15802  arisum2  15812  trireciplem  15813  geoser  15818  pwdif  15819  geolim  15821  geo2lim  15826  cvgrat  15834  mertenslem1  15835  mertenslem2  15836  mertens  15837  clim2prod  15839  clim2div  15840  ntrivcvgfvn0  15850  ntrivcvgtail  15851  prodeq2ii  15862  prodmolem3  15882  prodmolem2a  15883  fprod  15890  fprodntriv  15891  fprodss  15897  fprodser  15898  fprodcl2lem  15899  fprodmul  15909  fproddiv  15910  fprodabs  15923  fprodeq0  15924  fprodn0  15928  iprodclim3  15949  iprodmul  15952  fallfacfwd  15985  0fallfac  15986  binomfallfaclem2  15989  fallfacval4  15992  bpolysum  16002  bpolydiflem  16003  fsumkthpow  16005  efcvgfsum  16034  efcj  16040  fprodefsum  16043  effsumlt  16059  ruclem7  16184  bitsfzolem  16380  bitsfzo  16381  bitsfi  16383  bitsinv1lem  16387  bitsinv1  16388  bitsinvp1  16395  sadcp1  16401  sadadd  16413  sadass  16417  bitsres  16419  smupp1  16426  smuval2  16428  smupval  16434  smueqlem  16436  smumul  16439  algrp1  16516  phiprmpw  16714  crth  16716  phimullem  16717  eulerthlem2  16720  prmdiv  16723  pcpremul  16781  pcmpt  16830  pcfac  16837  pockthlem  16843  pockthg  16844  prmreclem2  16855  prmreclem3  16856  prmreclem4  16857  prmreclem5  16858  prmreclem6  16859  prmrec  16860  1arith  16865  vdwapun  16912  vdwlem1  16919  vdwlem2  16920  vdwlem3  16921  vdwlem6  16924  vdwlem8  16926  vdwlem10  16928  vdw  16932  imasvscafn  17488  oppccatid  17670  oppccomfpropd  17678  brcic  17750  funcoppc  17830  invfuc  17932  hofcl  18217  yonedalem4c  18235  gsumwsubmcl  18755  gsumsgrpccat  18758  gsumwmhm  18763  mulgnnp1  18999  mulgnnsubcl  19003  mulgnn0z  19018  mulgnndir  19020  psgnunilem4  19407  psgnran  19425  sylow1lem1  19508  lsmmod2  19586  lsmdisj2r  19595  efginvrel2  19637  efgsdmi  19642  efgsrel  19644  efgs1b  19646  efgsp1  19647  efgredleme  19653  efgredlemc  19655  efgcpbllemb  19665  frgpuplem  19682  mulgnn0di  19735  frgpnabllem1  19783  lt6abl  19805  cycsubgcyg  19811  gsumval3eu  19814  gsumval3  19817  gsumzcl2  19820  gsumzaddlem  19831  gsumconst  19844  gsumzmhm  19847  gsumzoppg  19854  telgsumfz0s  19901  dprdwd  19923  dprd2da  19954  pgpfaclem1  19993  srgbinom  20126  isirred  20311  lspprid2  20754  lspsnat  20904  lsppratlem1  20906  lsppratlem3  20908  lidl0cl  20985  lidlacl  20986  lidlnegcl  20987  2idllidld  21016  2idlridld  21017  rng2idl1cntr  21065  psgnghm  21353  frlmvscavalb  21545  frlmvplusgscavalb  21546  psrbaglefi  21705  psrbaglefiOLD  21706  psrass23l  21748  psrass23  21750  mplcoe5lem  21814  mpfind  21890  selvval  21901  mhpvscacl  21917  psr1bascl  21944  ply1basf  21946  gsummoncoe1  22049  lply1binom  22051  lply1binomsc  22052  mpfpf1  22091  pf1mpf  22092  evl1scvarpw  22103  matbas2i  22145  matecld  22149  matgsum  22160  mpomatmul  22169  dmatmul  22220  1mavmul  22271  mdetleib2  22311  m1detdiag  22320  marep01ma  22383  smadiadetlem4  22392  slesolinv  22403  pmatcollpw3fi1lem1  22509  chpscmat  22565  chpscmatgsumbin  22567  chp0mat  22569  chpidmat  22570  chfacfisf  22577  chfacfisfcpmat  22578  chfacfpmmulgsum2  22588  cldrcl  22751  ordtbas  22917  iscnp2  22964  dis1stc  23224  ptbasfi  23306  ptpjopn  23337  ptclsg  23340  ptcnp  23347  kqtop  23470  reghmph  23518  ptcmplem2  23778  ptcmplem3  23779  ptcmplem4  23780  tsmslem1  23854  utop2nei  23976  isucn2  24005  cuspcvg  24027  cnextucn  24029  imasdsf1olem  24100  blcvx  24535  xrhmeo  24692  cnrehmeo  24699  cnrehmeoOLD  24700  evth  24706  reparphti  24744  reparphtiOLD  24745  iscau4  25028  iscmet3lem1  25040  lmle  25050  rrxfsupp  25151  rrxdsfi  25160  pjthlem2  25187  ovollb2lem  25238  ovolunlem1a  25246  ovoliunlem1  25252  ovoliun2  25256  ovolscalem1  25263  ovolicc1  25266  ovolicc2lem4  25270  iundisj2  25299  voliunlem1  25300  volsup  25306  ioombl1lem4  25311  uniioovol  25329  uniioombllem3  25335  uniioombllem4  25336  uniioombllem6  25338  vitalilem5  25362  mbfimaopnlem  25405  mbflimsup  25416  mbfi1fseqlem3  25468  iblitg  25519  dvcnp2  25670  dvnp1  25676  cpncn  25687  dvmulbr  25690  dvcobr  25698  dvlip2  25748  dvfsumlem2  25780  dvfsumlem3  25781  dvfsumrlimge0  25783  dvfsumrlim2  25785  ftc1cn  25796  elplyd  25952  ply1termlem  25953  ply1term  25954  ply0  25958  plyeq0lem  25960  plyaddlem1  25963  plymullem1  25964  plyaddlem  25965  plymullem  25966  coeeulem  25974  plyco  25991  coeeq2  25992  coefv0  25998  coemulhi  26004  coemulc  26005  plycj  26028  dvply1  26034  vieta1lem2  26061  elqaalem2  26070  dvtaylp  26119  dvntaylp  26120  taylthlem1  26122  taylth  26124  ulmres  26137  ulmshftlem  26138  ulmshft  26139  ulmcau  26144  ulmdvlem1  26149  mtest  26153  mtestbdd  26154  pserulm  26171  psercn2  26172  psercnlem1  26174  psercn  26175  pserdvlem2  26177  abelthlem6  26185  abelth  26190  efif1olem1  26288  efif1olem3  26290  efif1olem4  26291  logcn  26392  advlogexp  26400  efopn  26403  cxpeq  26502  asinsin  26634  atantayl  26679  leibpilem2  26683  birthdaylem2  26694  birthdaylem3  26695  efrlim  26711  emcllem2  26738  emcllem5  26741  emcllem7  26743  harmonicbnd4  26752  fsumharmonic  26753  lgamgulm2  26777  lgamcvglem  26781  lgamcvg2  26796  gamcvg2lem  26800  wilthlem2  26810  wilthlem3  26811  ftalem1  26814  ftalem2  26815  ftalem3  26816  ftalem5  26818  basellem2  26823  basellem3  26824  basellem5  26826  basellem8  26829  ppiprm  26892  ppinprm  26893  chtprm  26894  chtnprm  26895  chpp1  26896  vma1  26907  ppiltx  26918  musum  26932  0sgmppw  26938  1sgmprm  26939  ppiublem2  26943  chtublem  26951  fsumvma2  26954  chpchtsum  26959  logexprlim  26965  bposlem5  27028  lgscllem  27044  lgsval2lem  27047  lgsval4a  27059  lgsneg  27061  lgsdir2lem3  27067  lgsdir2lem5  27069  lgsdir  27072  lgsdilem2  27073  lgsdi  27074  lgsne0  27075  gausslemma2dlem3  27108  lgseisenlem1  27115  lgsquadlem2  27121  chebbnd1lem1  27209  chtppilimlem1  27213  rplogsumlem2  27225  rpvmasumlem  27227  dchrisumlem1  27229  dchrisumlem2  27230  dchrmusum2  27234  dchrvmasum2lem  27236  dchrvmasumiflem1  27241  dchrisum0flblem1  27248  dchrisum0flblem2  27249  dchrisum0flb  27250  dchrisum0re  27253  dchrisum0lem1b  27255  dchrisum0lem1  27256  dchrisum0lem2a  27257  dchrisum0lem2  27258  dchrisum0lem3  27259  mudivsum  27270  mulogsum  27272  mulog2sumlem2  27275  selberg2lem  27290  logdivbnd  27296  pntrsumo1  27305  pntrsumbnd2  27307  pntrlog2bndlem2  27318  pntrlog2bndlem4  27320  pntrlog2bndlem6a  27322  pntlemj  27343  pntlemf  27345  ostth2lem3  27375  madebdayim  27620  oldbdayim  27621  tglngne  28069  ltgseg  28115  eedimeq  28424  axlowdimlem16  28483  ebtwntg  28508  subgruhgredgd  28809  subumgredg2  28810  umgrres1lem  28835  wlkson  29181  wksonproplem  29229  wksonproplemOLD  29230  trlsonfval  29231  pthsonfval  29265  spthson  29266  crctcshwlkn0lem4  29335  crctcshwlkn0lem5  29336  eupth2lems  29759  numclwwlk1lem2foa  29875  numclwlk1lem2  29891  numclwwlk2lem1  29897  htthlem  30438  hhsscms  30799  shmodsi  30910  pjoc1i  30952  5oalem1  31175  mayete3i  31249  adj1  31454  iundisj2f  32089  fmptco1f1o  32125  fcnvgreu  32166  suppovss  32174  ssnnssfz  32266  iundisj2fi  32276  cshw1s2  32392  gsumhashmul  32479  pmtrto1cl  32529  psgnfzto1stlem  32530  fzto1st1  32532  cycpmfv1  32543  cycpmfv2  32544  cycpmco2rn  32555  cycpmco2lem4  32559  cycpmco2lem5  32560  cycpmco2lem6  32561  cyc3evpm  32580  cyc3genpm  32582  cycpmconjslem2  32585  cyc3conja  32587  idomdomd  32645  idomringd  32646  idomrcan  32648  rspsnel  32759  nsgmgc  32798  nsgqusf1olem2  32800  ghmquskerlem1  32803  ghmquskerco  32804  unitpidl1  32817  elrspunsn  32822  mxidlirredi  32862  mxidlirred  32863  opprqusplusg  32878  opprqus0g  32879  opprqusmulr  32880  idlsrgmulrss1  32900  idlsrgmulrss2  32901  ig1pmindeg  32948  ply1degltdimlem  32996  lindsun  32999  fldextfld1  33017  fldextfld2  33018  1smat1  33083  submateqlem2  33087  lmatfval  33093  mdetlap1  33105  madjusmdetlem1  33106  madjusmdetlem2  33107  madjusmdetlem3  33108  madjusmdetlem4  33109  zarclssn  33152  zartopn  33154  zarmxt1  33159  rhmpreimacnlem  33163  rhmpreimacn  33164  pnfneige0  33230  pl1cn  33234  rrhqima  33293  indpreima  33322  esumfzf  33366  esumpcvgval  33375  esumpmono  33376  esumcvg  33383  ldgenpisyslem1  33460  ldgenpisys  33463  measbase  33494  dya2iocnei  33580  oddpwdc  33652  eulerpartlems  33658  eulerpartlemb  33666  sseqf  33690  fibp1  33699  orrvcval4  33762  orrvcoel  33763  orrvccel  33764  ballotlem2  33786  ballotlemfrceq  33826  signsplypnf  33860  signswch  33871  signstf0  33878  signstfvn  33879  signstfvneq0  33882  signstfvcl  33883  signstfveq0  33887  signsvfn  33892  fct2relem  33908  fsum2dsub  33918  reprsuc  33926  reprpmtf1o  33937  breprexplema  33941  breprexplemc  33943  hgt749d  33960  hgt750lemb  33967  tgoldbachgnn  33970  bnj1172  34311  bnj1245  34324  bnj1311  34334  bnj1450  34360  bnj1501  34377  subfacp1lem1  34469  subfacp1lem5  34474  subfacp1lem6  34475  subfacval2  34477  erdszelem7  34487  cvxsconn  34533  cvmliftlem5  34579  cvmliftlem7  34581  cvmliftlem10  34584  cvmliftlem13  34586  mrsubvrs  34812  msubrn  34819  msubco  34821  msubvrs  34850  imageval  35207  fwddifnp1  35442  gg-psercn2  35465  gg-dvfsumlem2  35470  knoppcnlem8  35680  knoppcnlem10  35682  bj-unirel  36236  icoreunrn  36544  istoprelowl  36545  poimirlem3  36795  poimirlem4  36796  poimirlem6  36798  poimirlem7  36799  poimirlem8  36800  poimirlem12  36804  poimirlem15  36807  poimirlem16  36808  poimirlem17  36809  poimirlem18  36810  poimirlem19  36811  poimirlem20  36812  poimirlem21  36813  poimirlem22  36814  poimirlem23  36815  poimirlem24  36816  poimirlem25  36817  poimirlem26  36818  poimirlem27  36819  poimirlem28  36820  poimirlem29  36821  poimirlem31  36823  mblfinlem2  36830  ftc1cnnc  36864  upixp  36901  sdclem2  36914  caushft  36933  ismtyres  36980  rrnmet  37001  rrndstprj1  37002  rrndstprj2  37003  rrncmslem  37004  rrnequiv  37007  iccbnd  37012  osumcllem7N  39137  pexmidlem4N  39148  lcfrlem4  40720  lcfrlem5  40721  lcfrlem6  40722  lcfrlem16  40733  lcfrlem38  40755  mapdrvallem2  40820  mapdh8ab  40952  mapdh8ad  40954  mapdh8e  40959  3factsumint3  41195  aks4d1p1p1  41235  fldhmf1  41262  sticksstones10  41278  metakunt20  41311  evlselv  41462  mhphf2  41473  fz1sump1  41511  sumcubes  41514  prjspnfv01  41669  prjspner01  41670  prjspner1  41671  mapfzcons  41757  diophren  41854  irrapxlem1  41863  monotuz  41983  acongeq  42025  jm2.26lem3  42043  jm3.1lem2  42060  pw2f1ocnv  42079  idomodle  42241  trclfvdecomr  42782  imo72b2lem1  43224  scottelrankd  43309  dvgrat  43374  cvgdvgrat  43375  hashnzfz2  43383  fcnre  44012  refsumcn  44017  rfcnnnub  44023  disjf1o  44189  disjinfi  44190  ssmapsn  44214  ssuzfz  44358  nnsplit  44367  uzssd2  44426  uzublem  44439  fsumsermpt  44594  climsuselem1  44622  limcperiod  44643  sumnnodd  44645  lptioo2cn  44660  lptioo1cn  44661  climresmpt  44674  allbutfifvre  44690  climleltrp  44691  cnrefiisplem  44844  cncfshift  44889  cncfperiod  44894  cncfshiftioo  44907  fperdvper  44934  dvnmptdivc  44953  dvnmul  44958  dvmptfprod  44960  dvnprodlem3  44963  stoweidlem11  45026  stoweidlem15  45030  stoweidlem17  45032  stoweidlem20  45035  stoweidlem34  45049  stoweidlem35  45050  stoweidlem46  45061  stoweidlem47  45062  stoweidlem56  45071  stoweidlem59  45074  stoweidlem62  45077  stirlinglem5  45093  stirlinglem14  45102  dirkertrigeqlem2  45114  dirkertrigeqlem3  45115  fourierdlem11  45133  fourierdlem15  45137  fourierdlem16  45138  fourierdlem21  45143  fourierdlem22  45144  fourierdlem25  45147  fourierdlem48  45169  fourierdlem52  45173  fourierdlem54  45175  fourierdlem58  45179  fourierdlem62  45183  fourierdlem64  45185  fourierdlem65  45186  fourierdlem69  45190  fourierdlem70  45191  fourierdlem71  45192  fourierdlem73  45194  fourierdlem80  45201  fourierdlem81  45202  fourierdlem83  45204  fourierdlem92  45213  fourierdlem93  45214  fourierdlem97  45218  fourierdlem103  45224  fourierdlem104  45225  fourierdlem112  45233  fourierdlem113  45234  fouriercnp  45241  fouriersw  45246  elaa2lem  45248  etransclem4  45253  etransclem7  45256  etransclem10  45259  etransclem14  45263  etransclem15  45264  etransclem24  45273  etransclem25  45274  etransclem31  45280  etransclem32  45281  etransclem35  45284  etransclem44  45293  etransclem46  45295  qndenserrnopnlem  45312  qndenserrn  45314  prsal  45333  salgencntex  45358  subsaliuncl  45373  subsalsal  45374  sge0tsms  45395  sge0fodjrnlem  45431  sge0isum  45442  iundjiunlem  45474  iundjiun  45475  meadjiunlem  45480  meaiunlelem  45483  meaiuninclem  45495  meaiininc2  45503  caragensplit  45515  carageneld  45517  carageniuncllem1  45536  caratheodorylem1  45541  caratheodorylem2  45542  hoicvr  45563  hsphoidmvle2  45600  hsphoidmvle  45601  hoidmv1lelem2  45607  hoidmv1lelem3  45608  hoidmvlelem2  45611  hoiqssbllem2  45638  pimdecfgtioc  45730  pimincfltioc  45731  pimdecfgtioo  45732  pimincfltioo  45733  smflimlem3  45788  smfmullem4  45809  smfsupxr  45831  smflimsuplem2  45836  smflimsuplem5  45839  natlocalincr  45889  elmod2  46337  ssnn0ssfz  47114  zlmodzxzscm  47122  rmsupp0  47133  lincsum  47198  lincscm  47199  lindslinindimp2lem4  47230  lincresunit3  47250  elbigofrcl  47324  intubeu  47697  unilbeu  47698  postc  47790  setrec1  47824  aacllem  47936