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  4713  ndmfvrcl  6856  fnwelem  8064  tz7.48-1  8365  brwitnlem  8425  oeeulem  8519  dffi3  9321  cnfcom3lem  9599  ttrclse  9623  alephgeom  9976  fpwwe2lem5  10529  canthwelem  10544  hargch  10567  r1wunlim  10631  eluzel2  12740  fseq1p1m1  13501  fznn0sub2  13538  nn0split  13546  seqp1d  13925  exple1  14084  digit1  14144  bcval5  14225  bcpasc  14228  hashf1  14364  seqcoll  14371  seqcoll2  14372  ccatrn  14496  swrdccat2  14576  cats1un  14627  pfxccatin12lem3  14638  splfv2a  14662  splval2  14663  caubnd  15266  limsupgre  15388  clim2ser  15562  clim2ser2  15563  iserex  15564  isermulc2  15565  iserle  15567  iserge0  15568  climub  15569  climserle  15570  isercolllem2  15573  isercolllem3  15574  isercoll  15575  isercoll2  15576  serf0  15588  iseraltlem2  15590  iseraltlem3  15591  iseralt  15592  sumeq2ii  15600  summolem3  15621  summolem2a  15622  fsum  15627  sum0  15628  fsumcl2lem  15638  fsumadd  15647  isumclim3  15666  isumadd  15674  fsump1i  15676  fsummulc2  15691  fsumrelem  15714  iserabs  15722  cvgcmp  15723  cvgcmpub  15724  cvgcmpce  15725  binom1dif  15740  isumshft  15746  isumsplit  15747  isumrpcl  15750  isumsup2  15753  climcndslem1  15756  climcndslem2  15757  climcnds  15758  arisum2  15768  trireciplem  15769  geoser  15774  pwdif  15775  geolim  15777  geo2lim  15782  cvgrat  15790  mertenslem1  15791  mertenslem2  15792  mertens  15793  clim2prod  15795  clim2div  15796  ntrivcvgfvn0  15806  ntrivcvgtail  15807  prodeq2ii  15818  prodmolem3  15840  prodmolem2a  15841  fprod  15848  fprodntriv  15849  fprodss  15855  fprodser  15856  fprodcl2lem  15857  fprodmul  15867  fproddiv  15868  fprodabs  15881  fprodeq0  15882  fprodn0  15886  iprodclim3  15907  iprodmul  15910  fallfacfwd  15943  0fallfac  15944  binomfallfaclem2  15947  fallfacval4  15950  bpolysum  15960  bpolydiflem  15961  fsumkthpow  15963  efcvgfsum  15993  efcj  15999  fprodefsum  16002  effsumlt  16020  ruclem7  16145  bitsfzolem  16345  bitsfzo  16346  bitsfi  16348  bitsinv1lem  16352  bitsinv1  16353  bitsinvp1  16360  sadcp1  16366  sadadd  16378  sadass  16382  bitsres  16384  smupp1  16391  smuval2  16393  smupval  16399  smueqlem  16401  smumul  16404  algrp1  16485  phiprmpw  16687  crth  16689  phimullem  16690  eulerthlem2  16693  prmdiv  16696  pcpremul  16755  pcmpt  16804  pcfac  16811  pockthlem  16817  pockthg  16818  prmreclem2  16829  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  prmrec  16834  1arith  16839  vdwapun  16886  vdwlem1  16893  vdwlem2  16894  vdwlem3  16895  vdwlem6  16898  vdwlem8  16900  vdwlem10  16902  vdw  16906  imasvscafn  17441  oppccatid  17625  oppccomfpropd  17633  brcic  17705  funcoppc  17782  invfuc  17884  hofcl  18165  yonedalem4c  18183  gsumwsubmcl  18711  gsumsgrpccat  18714  gsumwmhm  18719  mulgnnp1  18961  mulgnnsubcl  18965  mulgnn0z  18980  mulgnndir  18982  ghmquskerlem1  19162  ghmquskerco  19163  psgnunilem4  19376  psgnran  19394  sylow1lem1  19477  lsmmod2  19555  lsmdisj2r  19564  efginvrel2  19606  efgsdmi  19611  efgsrel  19613  efgs1b  19615  efgsp1  19616  efgredleme  19622  efgredlemc  19624  efgcpbllemb  19634  frgpuplem  19651  mulgnn0di  19704  frgpnabllem1  19752  lt6abl  19774  cycsubgcyg  19780  gsumval3eu  19783  gsumval3  19786  gsumzcl2  19789  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  telgsumfz0s  19870  dprdwd  19892  dprd2da  19923  pgpfaclem1  19962  srgbinom  20116  isirred  20304  idomdomd  20611  idomcringd  20612  lspprid2  20901  lspsnat  21052  lsppratlem1  21054  lsppratlem3  21056  lidl0cl  21127  lidlacl  21128  lidlnegcl  21129  elrspsn  21147  2idllidld  21161  2idlridld  21162  rng2idl1cntr  21212  psgnghm  21487  frlmvscavalb  21677  frlmvplusgscavalb  21678  psrbaglefi  21833  psrass23l  21874  psrass23  21876  mplcoe5lem  21944  mpfind  22012  selvval  22020  mhpvscacl  22039  psr1bascl  22083  ply1basf  22085  gsummoncoe1  22193  lply1binom  22195  lply1binomsc  22196  mpfpf1  22236  pf1mpf  22237  evl1scvarpw  22248  evl1maprhm  22264  matbas2i  22307  matecld  22311  matgsum  22322  mpomatmul  22331  dmatmul  22382  1mavmul  22433  mdetleib2  22473  m1detdiag  22482  marep01ma  22545  smadiadetlem4  22554  slesolinv  22565  pmatcollpw3fi1lem1  22671  chpscmat  22727  chpscmatgsumbin  22729  chp0mat  22731  chpidmat  22732  chfacfisf  22739  chfacfisfcpmat  22740  chfacfpmmulgsum2  22750  cldrcl  22911  ordtbas  23077  iscnp2  23124  dis1stc  23384  ptbasfi  23466  ptpjopn  23497  ptclsg  23500  ptcnp  23507  kqtop  23630  reghmph  23678  ptcmplem2  23938  ptcmplem3  23939  ptcmplem4  23940  tsmslem1  24014  utop2nei  24136  isucn2  24164  cuspcvg  24186  cnextucn  24188  imasdsf1olem  24259  blcvx  24684  xrhmeo  24842  cnrehmeo  24849  cnrehmeoOLD  24850  evth  24856  reparphti  24894  reparphtiOLD  24895  iscau4  25177  iscmet3lem1  25189  lmle  25199  rrxfsupp  25300  rrxdsfi  25309  pjthlem2  25336  ovollb2lem  25387  ovolunlem1a  25395  ovoliunlem1  25401  ovoliun2  25405  ovolscalem1  25412  ovolicc1  25415  ovolicc2lem4  25419  iundisj2  25448  voliunlem1  25449  volsup  25455  ioombl1lem4  25460  uniioovol  25478  uniioombllem3  25484  uniioombllem4  25485  uniioombllem6  25487  vitalilem5  25511  mbfimaopnlem  25554  mbflimsup  25565  mbfi1fseqlem3  25616  iblitg  25667  dvcnp2  25819  dvnp1  25825  cpncn  25836  dvmulbr  25839  dvcobr  25847  dvlip2  25898  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumrlimge0  25935  dvfsumrlim2  25937  ftc1cn  25948  elplyd  26105  ply1termlem  26106  ply1term  26107  ply0  26111  plyeq0lem  26113  plyaddlem1  26116  plymullem1  26117  plyaddlem  26118  plymullem  26119  coeeulem  26127  plyco  26144  coeeq2  26145  coefv0  26151  coemulhi  26157  coemulc  26158  plycj  26181  plycjOLD  26183  dvply1  26189  vieta1lem2  26217  elqaalem2  26226  dvtaylp  26276  dvntaylp  26277  taylthlem1  26279  taylth  26282  ulmres  26295  ulmshftlem  26296  ulmshft  26297  ulmcau  26302  ulmdvlem1  26307  mtest  26311  mtestbdd  26312  pserulm  26329  psercn2  26330  psercn2OLD  26331  psercnlem1  26333  psercn  26334  pserdvlem2  26336  abelthlem6  26344  abelth  26349  efif1olem1  26449  efif1olem3  26451  efif1olem4  26452  logcn  26554  advlogexp  26562  efopn  26565  cxpeq  26665  asinsin  26800  atantayl  26845  leibpilem2  26849  birthdaylem2  26860  birthdaylem3  26861  efrlim  26877  efrlimOLD  26878  emcllem2  26905  emcllem5  26908  emcllem7  26910  harmonicbnd4  26919  fsumharmonic  26920  lgamgulm2  26944  lgamcvglem  26948  lgamcvg2  26963  gamcvg2lem  26967  wilthlem2  26977  wilthlem3  26978  ftalem1  26981  ftalem2  26982  ftalem3  26983  ftalem5  26985  basellem2  26990  basellem3  26991  basellem5  26993  basellem8  26996  ppiprm  27059  ppinprm  27060  chtprm  27061  chtnprm  27062  chpp1  27063  vma1  27074  ppiltx  27085  musum  27099  0sgmppw  27107  1sgmprm  27108  ppiublem2  27112  chtublem  27120  fsumvma2  27123  chpchtsum  27128  logexprlim  27134  bposlem5  27197  lgscllem  27213  lgsval2lem  27216  lgsval4a  27228  lgsneg  27230  lgsdir2lem3  27236  lgsdir2lem5  27238  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  gausslemma2dlem3  27277  lgseisenlem1  27284  lgsquadlem2  27290  chebbnd1lem1  27378  chtppilimlem1  27382  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlem1  27398  dchrisumlem2  27399  dchrmusum2  27403  dchrvmasum2lem  27405  dchrvmasumiflem1  27410  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0flb  27419  dchrisum0re  27422  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0lem3  27428  mudivsum  27439  mulogsum  27441  mulog2sumlem2  27444  selberg2lem  27459  logdivbnd  27465  pntrsumo1  27474  pntrsumbnd2  27476  pntrlog2bndlem2  27487  pntrlog2bndlem4  27489  pntrlog2bndlem6a  27491  pntlemj  27512  pntlemf  27514  ostth2lem3  27544  madebdayim  27802  oldbdayim  27803  newbdayim  27817  noseqp1  28190  tglngne  28495  ltgseg  28541  eedimeq  28843  axlowdimlem16  28902  ebtwntg  28927  subgruhgredgd  29229  subumgredg2  29230  umgrres1lem  29255  wlkson  29600  wksonproplem  29648  trlsonfval  29649  pthsonfval  29685  spthson  29686  crctcshwlkn0lem4  29758  crctcshwlkn0lem5  29759  eupth2lems  30182  numclwwlk1lem2foa  30298  numclwlk1lem2  30314  numclwwlk2lem1  30320  htthlem  30861  hhsscms  31222  shmodsi  31333  pjoc1i  31375  5oalem1  31598  mayete3i  31672  adj1  31877  iundisj2f  32534  fmptco1f1o  32577  fcnvgreu  32617  suppovss  32624  ssnnssfz  32731  iundisj2fi  32741  indpreima  32809  ccatws1f1o  32894  cshw1s2  32903  chnccats1  32958  gsumhashmul  33015  gsumwrd2dccat  33021  fzo0pmtrlast  33035  wrdpmtrlast  33036  pmtrto1cl  33042  psgnfzto1stlem  33043  fzto1st1  33045  cycpmfv1  33056  cycpmfv2  33057  cycpmco2rn  33068  cycpmco2lem4  33072  cycpmco2lem5  33073  cycpmco2lem6  33074  cyc3evpm  33093  cyc3genpm  33095  cycpmconjslem2  33098  cyc3conja  33100  elrgspnlem1  33183  elrgspnlem2  33184  erler  33206  idomrcanOLD  33222  nsgmgc  33350  nsgqusf1olem2  33352  unitpidl1  33362  elrspunsn  33367  ssdifidllem  33394  mxidlirredi  33409  mxidlirred  33410  opprqusplusg  33427  opprqus0g  33428  opprqusmulr  33429  idlsrgmulrss1  33449  idlsrgmulrss2  33450  rprmcl  33456  rprmdvds  33457  rprmnz  33458  rprmnunit  33459  rprmasso  33463  rprmirredb  33470  pidufd  33481  1arithufdlem2  33483  1arithufdlem3  33484  zringfrac  33492  ply1dg3rt0irred  33519  m1pmeq  33520  ig1pmindeg  33535  exsslsb  33569  ply1degltdimlem  33595  lindsun  33598  fldextfld1  33620  fldextfld2  33621  rtelextdg2  33700  cos9thpiminplylem1  33755  1smat1  33777  submateqlem2  33781  lmatfval  33787  mdetlap1  33799  madjusmdetlem1  33800  madjusmdetlem2  33801  madjusmdetlem3  33802  madjusmdetlem4  33803  zarclssn  33846  zartopn  33848  zarmxt1  33853  rhmpreimacnlem  33857  rhmpreimacn  33858  pnfneige0  33924  pl1cn  33928  rrhqima  33987  esumfzf  34042  esumpcvgval  34051  esumpmono  34052  esumcvg  34059  ldgenpisyslem1  34136  ldgenpisys  34139  measbase  34170  dya2iocnei  34256  oddpwdc  34328  eulerpartlems  34334  eulerpartlemb  34342  sseqf  34366  fibp1  34375  orrvcval4  34439  orrvcoel  34440  orrvccel  34441  ballotlem2  34463  ballotlemfrceq  34503  signsplypnf  34524  signswch  34535  signstf0  34542  signstfvn  34543  signstfvneq0  34546  signstfvcl  34547  signstfveq0  34551  signsvfn  34556  fct2relem  34571  fsum2dsub  34581  reprsuc  34589  reprpmtf1o  34600  breprexplema  34604  breprexplemc  34606  hgt749d  34623  hgt750lemb  34630  tgoldbachgnn  34633  bnj1172  34974  bnj1245  34987  bnj1311  34997  bnj1450  35023  bnj1501  35040  subfacp1lem1  35162  subfacp1lem5  35167  subfacp1lem6  35168  subfacval2  35170  erdszelem7  35180  cvxpconn  35225  cvxsconn  35226  cvmliftlem5  35272  cvmliftlem7  35274  cvmliftlem10  35277  cvmliftlem13  35279  mrsubvrs  35505  msubrn  35512  msubco  35514  msubvrs  35543  r1peuqusdeg1  35626  imageval  35914  fwddifnp1  36149  knoppcnlem8  36484  knoppcnlem10  36486  bj-unirel  37035  icoreunrn  37343  istoprelowl  37344  poimirlem3  37613  poimirlem4  37614  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem12  37622  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem21  37631  poimirlem22  37632  poimirlem23  37633  poimirlem24  37634  poimirlem25  37635  poimirlem26  37636  poimirlem27  37637  poimirlem28  37638  poimirlem29  37639  poimirlem31  37641  mblfinlem2  37648  ftc1cnnc  37682  upixp  37719  sdclem2  37732  caushft  37751  ismtyres  37798  rrnmet  37819  rrndstprj1  37820  rrndstprj2  37821  rrncmslem  37822  rrnequiv  37825  iccbnd  37830  osumcllem7N  39951  pexmidlem4N  39962  lcfrlem4  41534  lcfrlem5  41535  lcfrlem6  41536  lcfrlem16  41547  lcfrlem38  41569  mapdrvallem2  41634  mapdh8ab  41766  mapdh8ad  41768  mapdh8e  41773  3factsumint3  42006  aks4d1p1p1  42046  fldhmf1  42073  aks6d1c1p2  42092  aks6d1c1p3  42093  aks6d1c1p7  42096  aks6d1c1p6  42097  aks6d1c1p8  42098  aks6d1c1  42099  evl1gprodd  42100  idomnnzpownz  42115  aks6d1c5lem1  42119  aks6d1c5lem3  42120  aks6d1c5lem2  42121  deg1gprod  42123  sticksstones10  42138  aks6d1c6lem3  42155  aks5lem2  42170  aks5lem3a  42172  unitscyglem5  42182  fz1sump1  42293  sumcubes  42296  evlselv  42570  mhphf2  42581  prjspnfv01  42607  prjspner01  42608  prjspner1  42609  mapfzcons  42699  diophren  42796  irrapxlem1  42805  monotuz  42924  acongeq  42966  jm2.26lem3  42984  jm3.1lem2  43001  pw2f1ocnv  43020  idomodle  43174  trclfvdecomr  43711  imo72b2lem0  44148  imo72b2lem1  44152  scottelrankd  44230  dvgrat  44295  cvgdvgrat  44296  hashnzfz2  44304  fcnre  45013  refsumcn  45018  rfcnnnub  45024  disjf1o  45179  disjinfi  45180  ssmapsn  45204  ssuzfz  45339  nnsplit  45348  uzssd2  45406  uzublem  45419  fsumsermpt  45570  climsuselem1  45598  limcperiod  45619  sumnnodd  45621  lptioo2cn  45636  lptioo1cn  45637  climresmpt  45650  allbutfifvre  45666  climleltrp  45667  cnrefiisplem  45820  cncfshift  45865  cncfperiod  45870  cncfshiftioo  45883  fperdvper  45910  dvnmptdivc  45929  dvnmul  45934  dvmptfprod  45936  dvnprodlem3  45939  stoweidlem11  46002  stoweidlem15  46006  stoweidlem17  46008  stoweidlem20  46011  stoweidlem34  46025  stoweidlem35  46026  stoweidlem46  46037  stoweidlem47  46038  stoweidlem56  46047  stoweidlem59  46050  stoweidlem62  46053  stirlinglem5  46069  stirlinglem14  46078  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  fourierdlem11  46109  fourierdlem15  46113  fourierdlem16  46114  fourierdlem21  46119  fourierdlem22  46120  fourierdlem25  46123  fourierdlem48  46145  fourierdlem52  46149  fourierdlem54  46151  fourierdlem58  46155  fourierdlem62  46159  fourierdlem64  46161  fourierdlem65  46162  fourierdlem69  46166  fourierdlem70  46167  fourierdlem71  46168  fourierdlem73  46170  fourierdlem80  46177  fourierdlem81  46178  fourierdlem83  46180  fourierdlem92  46189  fourierdlem93  46190  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  fourierdlem113  46210  fouriercnp  46217  fouriersw  46222  elaa2lem  46224  etransclem4  46229  etransclem7  46232  etransclem10  46235  etransclem14  46239  etransclem15  46240  etransclem24  46249  etransclem25  46250  etransclem31  46256  etransclem32  46257  etransclem35  46260  etransclem44  46269  etransclem46  46271  qndenserrnopnlem  46288  qndenserrn  46290  prsal  46309  salgencntex  46334  subsaliuncl  46349  subsalsal  46350  sge0tsms  46371  sge0fodjrnlem  46407  sge0isum  46418  iundjiunlem  46450  iundjiun  46451  meadjiunlem  46456  meaiunlelem  46459  meaiuninclem  46471  meaiininc2  46479  caragensplit  46491  carageneld  46493  carageniuncllem1  46512  caratheodorylem1  46517  caratheodorylem2  46518  hoicvr  46539  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmvlelem2  46587  hoiqssbllem2  46614  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  smflimlem3  46764  smfmullem4  46785  smfsupxr  46807  smflimsuplem2  46812  smflimsuplem5  46815  ormklocald  46865  natlocalincr  46867  elmod2  47349  isuspgrim0lem  47887  upgrimtrlslem2  47899  ssnn0ssfz  48343  zlmodzxzscm  48351  rmsupp0  48362  lincsum  48424  lincscm  48425  lindslinindimp2lem4  48456  lincresunit3  48476  elbigofrcl  48545  intubeu  48978  unilbeu  48979  cicrcl2  49038  cic1st2nd  49042  imaf1homlem  49102  oppfrcl  49123  eloppf  49128  imasubc  49146  imaid  49149  oppcuprcl5  49196  oppcup3  49204  uptrlem2  49206  uptrlem3  49207  natoppf  49224  elxpcbasex1ALT  49244  elxpcbasex2ALT  49246  swapf1a  49264  swapf2f1oa  49272  swapfida  49275  cofuswapf1  49289  cofuswapf2  49290  fucoppcco  49404  postc  49564  reldmlan2  49612  reldmran2  49613  lanrcl  49616  ranrcl  49617  setrec1  49686  aacllem  49796