Theorem eleqtrdi 2879

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eleqtrrdi  2880  3eltr3g  2885  prid2g  4732  ndmfvrcl  6915  fnwelem  8127  tz7.48-1  8430  brwitnlem  8492  oeeulem  8587  dffi3  9391  cnfcom3lem  9672  ttrclse  9696  scottelrankd  9873  alephgeom  10066  fpwwe2lem5  10620  canthwelem  10635  hargch  10658  r1wunlim  10722  eluzel2  12867  fseq1p1m1  13626  fznn0sub2  13663  nn0split  13671  seqp1d  14054  exple1  14213  digit1  14273  bcval5  14354  bcpasc  14357  hashf1  14494  seqcoll  14501  seqcoll2  14502  ccatrn  14627  swrdccat2  14707  cats1un  14758  pfxccatin12lem3  14769  splfv2a  14793  splval2  14794  caubnd  15410  limsupgre  15532  clim2ser  15706  clim2ser2  15707  iserex  15708  isermulc2  15709  iserle  15711  iserge0  15712  climub  15713  climserle  15714  isercolllem2  15717  isercolllem3  15718  isercoll  15719  isercoll2  15720  serf0  15732  iseraltlem2  15734  iseraltlem3  15735  iseralt  15736  sumeq2ii  15744  summolem3  15765  summolem2a  15766  fsum  15771  sum0  15772  fsumcl2lem  15782  fsumadd  15791  isumclim3  15810  isumadd  15818  fsump1i  15820  fsummulc2  15835  fsumrelem  15859  iserabs  15867  cvgcmp  15868  cvgcmpub  15869  cvgcmpce  15870  binom1dif  15887  isumshft  15893  isumsplit  15894  isumrpcl  15897  isumsup2  15900  climcndslem1  15903  climcndslem2  15904  climcnds  15905  arisum2  15915  trireciplem  15916  geoser  15921  pwdif  15922  geolim  15924  geo2lim  15929  cvgrat  15937  mertenslem1  15938  mertenslem2  15939  mertens  15940  clim2prod  15942  clim2div  15943  ntrivcvgfvn0  15953  ntrivcvgtail  15954  prodeq2ii  15965  prodmolem3  15987  prodmolem2a  15988  fprod  15995  fprodntriv  15996  fprodss  16002  fprodser  16003  fprodcl2lem  16004  fprodmul  16014  fproddiv  16015  fprodabs  16028  fprodeq0  16029  fprodn0  16033  iprodclim3  16054  iprodmul  16057  fallfacfwd  16090  0fallfac  16091  binomfallfaclem2  16094  fallfacval4  16097  bpolysum  16107  bpolydiflem  16108  fsumkthpow  16110  efcvgfsum  16140  efcj  16146  fprodefsum  16149  effsumlt  16167  ruclem7  16292  bitsfzolem  16492  bitsfzo  16493  bitsfi  16495  bitsinv1lem  16499  bitsinv1  16500  bitsinvp1  16507  sadcp1  16513  sadadd  16525  sadass  16529  bitsres  16531  smupp1  16538  smuval2  16540  smupval  16546  smueqlem  16548  smumul  16551  algrp1  16632  phiprmpw  16835  crth  16837  phimullem  16838  eulerthlem2  16841  prmdiv  16844  pcpremul  16903  pcmpt  16952  pcfac  16959  pockthlem  16965  pockthg  16966  prmreclem2  16977  prmreclem3  16978  prmreclem4  16979  prmreclem5  16980  prmreclem6  16981  prmrec  16982  1arith  16987  vdwapun  17034  vdwlem1  17041  vdwlem2  17042  vdwlem3  17043  vdwlem6  17046  vdwlem8  17048  vdwlem10  17050  vdw  17054  imasvscafn  17591  oppccatid  17775  oppccomfpropd  17783  brcic  17855  funcoppc  17932  invfuc  18034  hofcl  18315  yonedalem4c  18333  chnccats1  18681  gsumwsubmcl  18896  gsumsgrpccat  18899  gsumwmhm  18904  mulgnnp1  19148  mulgnnsubcl  19152  mulgnn0z  19167  mulgnndir  19169  ghmquskerlem1  19353  ghmquskerco  19354  psgnunilem4  19567  psgnran  19585  sylow1lem1  19668  lsmmod2  19746  lsmdisj2r  19755  efginvrel2  19797  efgsdmi  19802  efgsrel  19804  efgs1b  19806  efgsp1  19807  efgredleme  19813  efgredlemc  19815  efgcpbllemb  19825  frgpuplem  19842  mulgnn0di  19895  frgpnabllem1  19943  lt6abl  19965  cycsubgcyg  19971  gsumval3eu  19974  gsumval3  19977  gsumzcl2  19980  gsumzaddlem  19991  gsumconst  20004  gsumzmhm  20007  gsumzoppg  20014  telgsumfz0s  20061  dprdwd  20083  dprd2da  20114  pgpfaclem1  20153  srgbinom  20313  isirred  20501  idomdomd  20810  idomcringd  20811  lspprid2  21097  lspsnat  21247  lsppratlem1  21249  lsppratlem3  21251  lidl0cl  21323  lidlacl  21324  lidlnegcl  21325  elrspsn  21347  2idllidld  21364  2idlridld  21365  rng2idl1cntr  21416  ssdifidllem  21453  psgnghm  21699  frlmvscavalb  21889  frlmvplusgscavalb  21890  psrbaglefi  22045  psrass23l  22085  psrass23  22087  mplcoe5lem  22159  mpfind  22235  selvval  22240  mhpvscacl  22286  psr1bascl  22329  ply1basf  22331  gsummoncoe1  22437  lply1binom  22439  lply1binomsc  22440  mpfpf1  22480  pf1mpf  22481  evl1scvarpw  22492  evl1maprhm  22508  matbas2i  22548  matecld  22552  matgsum  22563  mpomatmul  22572  dmatmul  22623  1mavmul  22674  mdetleib2  22714  m1detdiag  22723  marep01ma  22786  smadiadetlem4  22795  slesolinv  22806  pmatcollpw3fi1lem1  22912  chpscmat  22968  chpscmatgsumbin  22970  chp0mat  22972  chpidmat  22973  chfacfisf  22980  chfacfisfcpmat  22981  chfacfpmmulgsum2  22991  cldrcl  23152  ordtbas  23318  iscnp2  23365  dis1stc  23625  ptbasfi  23707  ptpjopn  23738  ptclsg  23741  ptcnp  23748  kqtop  23871  reghmph  23919  ptcmplem2  24179  ptcmplem3  24180  ptcmplem4  24181  tsmslem1  24255  utop2nei  24376  isucn2  24404  cuspcvg  24426  cnextucn  24428  imasdsf1olem  24499  blcvx  24924  xrhmeo  25074  cnrehmeo  25081  evth  25087  reparphti  25125  iscau4  25407  iscmet3lem1  25419  lmle  25429  rrxfsupp  25530  rrxdsfi  25539  pjthlem2  25566  ovollb2lem  25616  ovolunlem1a  25624  ovoliunlem1  25630  ovoliun2  25634  ovolscalem1  25641  ovolicc1  25644  ovolicc2lem4  25648  iundisj2  25677  voliunlem1  25678  volsup  25684  ioombl1lem4  25689  uniioovol  25707  uniioombllem3  25713  uniioombllem4  25714  uniioombllem6  25716  vitalilem5  25740  mbfimaopnlem  25783  mbflimsup  25794  mbfi1fseqlem3  25845  iblitg  25896  dvcnp2  26048  dvnp1  26053  cpncn  26064  dvmulbr  26067  dvcobr  26074  dvlip2  26123  dvfsumlem2  26155  dvfsumlem3  26156  dvfsumrlimge0  26158  dvfsumrlim2  26160  ftc1cn  26171  elplyd  26328  ply1termlem  26329  ply1term  26330  ply0  26334  plyeq0lem  26336  plyaddlem1  26339  plymullem1  26340  plyaddlem  26341  plymullem  26342  coeeulem  26350  plyco  26367  coeeq2  26368  coefv0  26374  coemulhi  26380  coemulc  26381  plycj  26403  plycjOLD  26405  dvply1  26414  vieta1lem2  26441  elqaalem2  26450  dvtaylp  26499  dvntaylp  26500  taylthlem1  26502  taylth  26504  ulmres  26517  ulmshftlem  26518  ulmshft  26519  ulmcau  26524  ulmdvlem1  26529  mtest  26533  mtestbdd  26534  pserulm  26551  psercn2  26552  psercnlem1  26554  psercn  26555  pserdvlem2  26557  abelthlem6  26565  abelth  26570  efif1olem1  26673  efif1olem3  26675  efif1olem4  26676  logcn  26778  advlogexp  26786  efopn  26789  cxpeq  26888  asinsin  27023  atantayl  27068  leibpilem2  27072  birthdaylem2  27083  birthdaylem3  27084  efrlim  27100  emcllem2  27127  emcllem5  27130  emcllem7  27132  harmonicbnd4  27141  fsumharmonic  27142  lgamgulm2  27166  lgamcvglem  27170  lgamcvg2  27185  gamcvg2lem  27189  wilthlem2  27199  wilthlem3  27200  ftalem1  27203  ftalem2  27204  ftalem3  27205  ftalem5  27207  basellem2  27212  basellem3  27213  basellem5  27215  basellem8  27218  ppiprm  27281  ppinprm  27282  chtprm  27283  chtnprm  27284  chpp1  27285  vma1  27296  ppiltx  27307  musum  27321  0sgmppw  27328  1sgmprm  27329  ppiublem2  27333  chtublem  27341  fsumvma2  27344  chpchtsum  27349  logexprlim  27355  bposlem5  27418  lgscllem  27434  lgsval2lem  27437  lgsval4a  27449  lgsneg  27451  lgsdir2lem3  27457  lgsdir2lem5  27459  lgsdir  27462  lgsdilem2  27463  lgsdi  27464  lgsne0  27465  gausslemma2dlem3  27498  lgseisenlem1  27505  lgsquadlem2  27511  chebbnd1lem1  27599  chtppilimlem1  27603  rplogsumlem2  27615  rpvmasumlem  27617  dchrisumlem1  27619  dchrisumlem2  27620  dchrmusum2  27624  dchrvmasum2lem  27626  dchrvmasumiflem1  27631  dchrisum0flblem1  27638  dchrisum0flblem2  27639  dchrisum0flb  27640  dchrisum0re  27643  dchrisum0lem1b  27645  dchrisum0lem1  27646  dchrisum0lem2a  27647  dchrisum0lem2  27648  dchrisum0lem3  27649  mudivsum  27660  mulogsum  27662  mulog2sumlem2  27665  selberg2lem  27680  logdivbnd  27686  pntrsumo1  27695  pntrsumbnd2  27697  pntrlog2bndlem2  27708  pntrlog2bndlem4  27710  pntrlog2bndlem6a  27712  pntlemj  27733  pntlemf  27735  ostth2lem3  27765  madebdayim  28047  oldbdayim  28048  newbdayim  28062  cutminmax  28095  noseqp1  28450  tglngne  28785  ltgseg  28831  eedimeq  29189  axlowdimlem16  29248  ebtwntg  29273  subgruhgredgd  29575  subumgredg2  29576  umgrres1lem  29601  wlkson  29945  wksonproplem  29993  trlsonfval  29994  pthsonfval  30030  spthson  30031  crctcshwlkn0lem4  30103  crctcshwlkn0lem5  30104  eupth2lems  30530  numclwwlk1lem2foa  30646  numclwlk1lem2  30662  numclwwlk2lem1  30668  htthlem  31210  hhsscms  31571  shmodsi  31682  pjoc1i  31724  5oalem1  31947  mayete3i  32021  adj1  32226  iundisj2f  32876  fmptco1f1o  32919  fcnvgreu  32958  suppovss  32967  ssnnssfz  33073  nn0diffz0  33080  iundisj2fi  33083  indpreima  33126  ccatws1f1o  33212  cshw1s2  33221  gsumhashmul  33328  gsummulsubdishift1  33329  gsumwrd2dccat  33339  fzo0pmtrlast  33353  wrdpmtrlast  33354  pmtrto1cl  33360  psgnfzto1stlem  33361  fzto1st1  33363  cycpmfv1  33374  cycpmfv2  33375  cycpmco2rn  33386  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cyc3evpm  33411  cyc3genpm  33413  cycpmconjslem2  33416  cyc3conja  33418  elrgspnlem1  33503  elrgspnlem2  33504  erler  33526  nsgmgc  33665  nsgqusf1olem2  33667  unitpidl1  33676  elrspunsn  33681  mxidlirredi  33699  mxidlirred  33700  opprqusplusg  33716  opprqus0g  33717  opprqusmulr  33718  idlsrgmulrss1  33746  idlsrgmulrss2  33747  rprmcl  33753  rprmdvds  33754  rprmnz  33755  rprmnunit  33756  rprmasso  33760  rprmirredb  33767  pidufd  33778  1arithufdlem2  33780  1arithufdlem3  33781  zringfrac  33789  ply1dg3rt0irred  33819  m1pmeq  33820  ig1pmindeg  33837  selvply1rhmlem2  33856  selvply1rhmlem4  33858  selvply1rhm0  33861  extvfvvcl  33870  evlextv  33877  psrmonprod  33887  esplysply  33906  esplyind  33910  esplyfvn  33912  vietalem  33914  exsslsb  33932  ply1degltdimlem  33957  lindsun  33960  fldextfld1  33982  fldextfld2  33983  rtelextdg2  34062  cos9thpiminplylem1  34117  1smat1  34139  submateqlem2  34143  lmatfval  34149  mdetlap1  34161  madjusmdetlem1  34162  madjusmdetlem2  34163  madjusmdetlem3  34164  madjusmdetlem4  34165  zarclssn  34208  zartopn  34210  zarmxt1  34215  rhmpreimacnlem  34219  rhmpreimacn  34220  pnfneige0  34286  pl1cn  34290  rrhqima  34349  esumfzf  34404  esumpcvgval  34413  esumpmono  34414  esumcvg  34421  ldgenpisyslem1  34498  ldgenpisys  34501  measbase  34532  dya2iocnei  34617  oddpwdc  34689  eulerpartlems  34695  eulerpartlemb  34703  sseqf  34727  fibp1  34736  orrvcval4  34800  orrvcoel  34801  orrvccel  34802  ballotlem2  34824  ballotlemfrceq  34864  signsplypnf  34882  signswch  34893  signstf0  34900  signstfvn  34901  signstfvneq0  34904  signstfvcl  34905  signstfveq0  34909  signsvfn  34914  fct2relem  34929  fsum2dsub  34939  reprsuc  34947  reprpmtf1o  34958  breprexplema  34962  breprexplemc  34964  hgt749d  34981  hgt750lemb  34988  tgoldbachgnn  34991  bnj1172  35334  bnj1245  35347  bnj1311  35357  bnj1450  35383  bnj1501  35400  r1elcl  35434  subfacp1lem1  35604  subfacp1lem5  35609  subfacp1lem6  35610  subfacval2  35612  erdszelem7  35622  cvxpconn  35667  cvxsconn  35668  cvmliftlem5  35714  cvmliftlem7  35716  cvmliftlem10  35719  cvmliftlem13  35721  mrsubvrs  35947  msubrn  35954  msubco  35956  msubvrs  35985  r1peuqusdeg1  36068  imageval  36353  fwddifnp1  36590  knoppcnlem8  37012  knoppcnlem10  37014  bj-unirel  37609  icoreunrn  37927  istoprelowl  37928  poimirlem3  38196  poimirlem4  38197  poimirlem6  38199  poimirlem7  38200  poimirlem8  38201  poimirlem12  38205  poimirlem15  38208  poimirlem16  38209  poimirlem17  38210  poimirlem18  38211  poimirlem19  38212  poimirlem20  38213  poimirlem21  38214  poimirlem22  38215  poimirlem23  38216  poimirlem24  38217  poimirlem25  38218  poimirlem26  38219  poimirlem27  38220  poimirlem28  38221  poimirlem29  38222  poimirlem31  38224  mblfinlem2  38231  ftc1cnnc  38265  upixp  38302  sdclem2  38315  caushft  38334  ismtyres  38381  rrnmet  38402  rrndstprj1  38403  rrndstprj2  38404  rrncmslem  38405  rrnequiv  38408  iccbnd  38413  osumcllem7N  40660  pexmidlem4N  40671  lcfrlem4  42243  lcfrlem5  42244  lcfrlem6  42245  lcfrlem16  42256  lcfrlem38  42278  mapdrvallem2  42343  mapdh8ab  42475  mapdh8ad  42477  mapdh8e  42482  3factsumint3  42714  aks4d1p1p1  42754  fldhmf1  42781  aks6d1c1p2  42800  aks6d1c1p3  42801  aks6d1c1p7  42804  aks6d1c1p6  42805  aks6d1c1p8  42806  aks6d1c1  42807  evl1gprodd  42808  idomnnzpownz  42823  aks6d1c5lem1  42827  aks6d1c5lem3  42828  aks6d1c5lem2  42829  deg1gprod  42831  sticksstones10  42846  aks6d1c6lem3  42863  aks5lem2  42878  aks5lem3a  42880  unitscyglem5  42890  fz1sump1  42995  sumcubes  42998  evlselv  43247  mhphf2  43256  prjspnfv01  43282  prjspner01  43283  prjspner1  43284  mapfzcons  43373  diophren  43466  irrapxlem1  43475  monotuz  43594  acongeq  43636  jm2.26lem3  43654  jm3.1lem2  43671  pw2f1ocnv  43690  idomodle  43844  trclfvdecomr  44380  imo72b2lem0  44817  imo72b2lem1  44821  dvgrat  44948  cvgdvgrat  44949  hashnzfz2  44957  fcnre  45671  refsumcn  45676  rfcnnnub  45682  disjf1o  45835  disjinfi  45836  ssmapsn  45858  ssuzfz  45991  nnsplit  46000  uzssd2  46057  uzublem  46070  fsumsermpt  46221  climsuselem1  46249  limcperiod  46270  sumnnodd  46272  lptioo2cn  46285  lptioo1cn  46286  climresmpt  46299  allbutfifvre  46315  climleltrp  46316  cnrefiisplem  46469  cncfshift  46514  cncfperiod  46519  cncfshiftioo  46532  fperdvper  46559  dvnmptdivc  46578  dvnmul  46583  dvmptfprod  46585  dvnprodlem3  46588  stoweidlem11  46651  stoweidlem15  46655  stoweidlem17  46657  stoweidlem20  46660  stoweidlem34  46674  stoweidlem35  46675  stoweidlem46  46686  stoweidlem47  46687  stoweidlem56  46696  stoweidlem59  46699  stoweidlem62  46702  stirlinglem5  46718  stirlinglem14  46727  dirkertrigeqlem2  46739  dirkertrigeqlem3  46740  fourierdlem11  46758  fourierdlem15  46762  fourierdlem16  46763  fourierdlem21  46768  fourierdlem22  46769  fourierdlem25  46772  fourierdlem48  46794  fourierdlem49  46795  fourierdlem52  46798  fourierdlem54  46800  fourierdlem58  46804  fourierdlem62  46808  fourierdlem64  46810  fourierdlem65  46811  fourierdlem69  46815  fourierdlem70  46816  fourierdlem71  46817  fourierdlem73  46819  fourierdlem80  46826  fourierdlem81  46827  fourierdlem83  46829  fourierdlem92  46838  fourierdlem93  46839  fourierdlem97  46843  fourierdlem103  46849  fourierdlem104  46850  fourierdlem112  46858  fourierdlem113  46859  fouriercnp  46866  fouriersw  46871  elaa2lem  46873  etransclem4  46878  etransclem7  46881  etransclem10  46884  etransclem14  46888  etransclem15  46889  etransclem24  46898  etransclem25  46899  etransclem31  46905  etransclem32  46906  etransclem35  46909  etransclem44  46918  etransclem46  46920  qndenserrnopnlem  46937  qndenserrn  46939  prsal  46958  salgencntex  46983  subsaliuncl  46998  subsalsal  46999  sge0tsms  47020  sge0fodjrnlem  47056  sge0isum  47067  iundjiunlem  47099  iundjiun  47100  meadjiunlem  47105  meaiunlelem  47108  meaiuninclem  47120  meaiininc2  47128  caragensplit  47140  carageneld  47142  carageniuncllem1  47161  caratheodorylem1  47166  caratheodorylem2  47167  hoicvr  47188  hsphoidmvle2  47225  hsphoidmvle  47226  hoidmv1lelem2  47232  hoidmv1lelem3  47233  hoidmvlelem2  47236  hoiqssbllem2  47263  pimdecfgtioc  47355  pimincfltioc  47356  pimdecfgtioo  47357  pimincfltioo  47358  smflimlem3  47413  smfmullem4  47434  smfsupxr  47456  smflimsuplem2  47461  smflimsuplem5  47464  ormklocald  47516  natlocalincr  47518  elmod2  48021  isuspgrim0lem  48581  upgrimtrlslem2  48593  ssnn0ssfz  49048  zlmodzxzscm  49056  rmsupp0  49067  lincsum  49128  lincscm  49129  lindslinindimp2lem4  49160  lincresunit3  49180  elbigofrcl  49249  intubeu  49681  unilbeu  49682  cicrcl2  49740  cic1st2nd  49744  imaf1homlem  49804  oppfrcl  49825  eloppf  49830  imasubc  49848  imaid  49851  oppcuprcl5  49898  oppcup3  49906  uptrlem2  49908  uptrlem3  49909  natoppf  49926  elxpcbasex1ALT  49946  elxpcbasex2ALT  49948  swapf1a  49966  swapf2f1oa  49974  swapfida  49977  cofuswapf1  49991  cofuswapf2  49992  fucoppcco  50106  postc  50266  reldmlan2  50314  reldmran2  50315  lanrcl  50318  ranrcl  50319  setrec1  50388  aacllem  50509