Theorem eleqtrdi 2841

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

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

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  eleqtrrdi  2842  3eltr3g  2847  prid2g  4711  ndmfvrcl  6855  fnwelem  8061  tz7.48-1  8362  brwitnlem  8422  oeeulem  8516  dffi3  9315  cnfcom3lem  9593  ttrclse  9617  alephgeom  9973  fpwwe2lem5  10526  canthwelem  10541  hargch  10564  r1wunlim  10628  eluzel2  12737  fseq1p1m1  13498  fznn0sub2  13535  nn0split  13543  seqp1d  13925  exple1  14084  digit1  14144  bcval5  14225  bcpasc  14228  hashf1  14364  seqcoll  14371  seqcoll2  14372  ccatrn  14497  swrdccat2  14577  cats1un  14628  pfxccatin12lem3  14639  splfv2a  14663  splval2  14664  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  chnccats1  18531  gsumwsubmcl  18745  gsumsgrpccat  18748  gsumwmhm  18753  mulgnnp1  18995  mulgnnsubcl  18999  mulgnn0z  19014  mulgnndir  19016  ghmquskerlem1  19195  ghmquskerco  19196  psgnunilem4  19409  psgnran  19427  sylow1lem1  19510  lsmmod2  19588  lsmdisj2r  19597  efginvrel2  19639  efgsdmi  19644  efgsrel  19646  efgs1b  19648  efgsp1  19649  efgredleme  19655  efgredlemc  19657  efgcpbllemb  19667  frgpuplem  19684  mulgnn0di  19737  frgpnabllem1  19785  lt6abl  19807  cycsubgcyg  19813  gsumval3eu  19816  gsumval3  19819  gsumzcl2  19822  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  telgsumfz0s  19903  dprdwd  19925  dprd2da  19956  pgpfaclem1  19995  srgbinom  20149  isirred  20337  idomdomd  20641  idomcringd  20642  lspprid2  20931  lspsnat  21082  lsppratlem1  21084  lsppratlem3  21086  lidl0cl  21157  lidlacl  21158  lidlnegcl  21159  elrspsn  21177  2idllidld  21191  2idlridld  21192  rng2idl1cntr  21242  psgnghm  21517  frlmvscavalb  21707  frlmvplusgscavalb  21708  psrbaglefi  21863  psrass23l  21904  psrass23  21906  mplcoe5lem  21974  mpfind  22042  selvval  22050  mhpvscacl  22069  psr1bascl  22113  ply1basf  22115  gsummoncoe1  22223  lply1binom  22225  lply1binomsc  22226  mpfpf1  22266  pf1mpf  22267  evl1scvarpw  22278  evl1maprhm  22294  matbas2i  22337  matecld  22341  matgsum  22352  mpomatmul  22361  dmatmul  22412  1mavmul  22463  mdetleib2  22503  m1detdiag  22512  marep01ma  22575  smadiadetlem4  22584  slesolinv  22595  pmatcollpw3fi1lem1  22701  chpscmat  22757  chpscmatgsumbin  22759  chp0mat  22761  chpidmat  22762  chfacfisf  22769  chfacfisfcpmat  22770  chfacfpmmulgsum2  22780  cldrcl  22941  ordtbas  23107  iscnp2  23154  dis1stc  23414  ptbasfi  23496  ptpjopn  23527  ptclsg  23530  ptcnp  23537  kqtop  23660  reghmph  23708  ptcmplem2  23968  ptcmplem3  23969  ptcmplem4  23970  tsmslem1  24044  utop2nei  24165  isucn2  24193  cuspcvg  24215  cnextucn  24217  imasdsf1olem  24288  blcvx  24713  xrhmeo  24871  cnrehmeo  24878  cnrehmeoOLD  24879  evth  24885  reparphti  24923  reparphtiOLD  24924  iscau4  25206  iscmet3lem1  25218  lmle  25228  rrxfsupp  25329  rrxdsfi  25338  pjthlem2  25365  ovollb2lem  25416  ovolunlem1a  25424  ovoliunlem1  25430  ovoliun2  25434  ovolscalem1  25441  ovolicc1  25444  ovolicc2lem4  25448  iundisj2  25477  voliunlem1  25478  volsup  25484  ioombl1lem4  25489  uniioovol  25507  uniioombllem3  25513  uniioombllem4  25514  uniioombllem6  25516  vitalilem5  25540  mbfimaopnlem  25583  mbflimsup  25594  mbfi1fseqlem3  25645  iblitg  25696  dvcnp2  25848  dvnp1  25854  cpncn  25865  dvmulbr  25868  dvcobr  25876  dvlip2  25927  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumrlimge0  25964  dvfsumrlim2  25966  ftc1cn  25977  elplyd  26134  ply1termlem  26135  ply1term  26136  ply0  26140  plyeq0lem  26142  plyaddlem1  26145  plymullem1  26146  plyaddlem  26147  plymullem  26148  coeeulem  26156  plyco  26173  coeeq2  26174  coefv0  26180  coemulhi  26186  coemulc  26187  plycj  26210  plycjOLD  26212  dvply1  26218  vieta1lem2  26246  elqaalem2  26255  dvtaylp  26305  dvntaylp  26306  taylthlem1  26308  taylth  26311  ulmres  26324  ulmshftlem  26325  ulmshft  26326  ulmcau  26331  ulmdvlem1  26336  mtest  26340  mtestbdd  26341  pserulm  26358  psercn2  26359  psercn2OLD  26360  psercnlem1  26362  psercn  26363  pserdvlem2  26365  abelthlem6  26373  abelth  26378  efif1olem1  26478  efif1olem3  26480  efif1olem4  26481  logcn  26583  advlogexp  26591  efopn  26594  cxpeq  26694  asinsin  26829  atantayl  26874  leibpilem2  26878  birthdaylem2  26889  birthdaylem3  26890  efrlim  26906  efrlimOLD  26907  emcllem2  26934  emcllem5  26937  emcllem7  26939  harmonicbnd4  26948  fsumharmonic  26949  lgamgulm2  26973  lgamcvglem  26977  lgamcvg2  26992  gamcvg2lem  26996  wilthlem2  27006  wilthlem3  27007  ftalem1  27010  ftalem2  27011  ftalem3  27012  ftalem5  27014  basellem2  27019  basellem3  27020  basellem5  27022  basellem8  27025  ppiprm  27088  ppinprm  27089  chtprm  27090  chtnprm  27091  chpp1  27092  vma1  27103  ppiltx  27114  musum  27128  0sgmppw  27136  1sgmprm  27137  ppiublem2  27141  chtublem  27149  fsumvma2  27152  chpchtsum  27157  logexprlim  27163  bposlem5  27226  lgscllem  27242  lgsval2lem  27245  lgsval4a  27257  lgsneg  27259  lgsdir2lem3  27265  lgsdir2lem5  27267  lgsdir  27270  lgsdilem2  27271  lgsdi  27272  lgsne0  27273  gausslemma2dlem3  27306  lgseisenlem1  27313  lgsquadlem2  27319  chebbnd1lem1  27407  chtppilimlem1  27411  rplogsumlem2  27423  rpvmasumlem  27425  dchrisumlem1  27427  dchrisumlem2  27428  dchrmusum2  27432  dchrvmasum2lem  27434  dchrvmasumiflem1  27439  dchrisum0flblem1  27446  dchrisum0flblem2  27447  dchrisum0flb  27448  dchrisum0re  27451  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  dchrisum0lem3  27457  mudivsum  27468  mulogsum  27470  mulog2sumlem2  27473  selberg2lem  27488  logdivbnd  27494  pntrsumo1  27503  pntrsumbnd2  27505  pntrlog2bndlem2  27516  pntrlog2bndlem4  27518  pntrlog2bndlem6a  27520  pntlemj  27541  pntlemf  27543  ostth2lem3  27573  madebdayim  27833  oldbdayim  27834  newbdayim  27848  noseqp1  28221  tglngne  28528  ltgseg  28574  eedimeq  28876  axlowdimlem16  28935  ebtwntg  28960  subgruhgredgd  29262  subumgredg2  29263  umgrres1lem  29288  wlkson  29633  wksonproplem  29681  trlsonfval  29682  pthsonfval  29718  spthson  29719  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  eupth2lems  30218  numclwwlk1lem2foa  30334  numclwlk1lem2  30350  numclwwlk2lem1  30356  htthlem  30897  hhsscms  31258  shmodsi  31369  pjoc1i  31411  5oalem1  31634  mayete3i  31708  adj1  31913  iundisj2f  32570  fmptco1f1o  32615  fcnvgreu  32655  suppovss  32662  ssnnssfz  32770  iundisj2fi  32779  indpreima  32846  ccatws1f1o  32932  cshw1s2  32941  gsumhashmul  33041  gsumwrd2dccat  33047  fzo0pmtrlast  33061  wrdpmtrlast  33062  pmtrto1cl  33068  psgnfzto1stlem  33069  fzto1st1  33071  cycpmfv1  33082  cycpmfv2  33083  cycpmco2rn  33094  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cyc3evpm  33119  cyc3genpm  33121  cycpmconjslem2  33124  cyc3conja  33126  elrgspnlem1  33209  elrgspnlem2  33210  erler  33232  idomrcanOLD  33248  nsgmgc  33377  nsgqusf1olem2  33379  unitpidl1  33389  elrspunsn  33394  ssdifidllem  33421  mxidlirredi  33436  mxidlirred  33437  opprqusplusg  33454  opprqus0g  33455  opprqusmulr  33456  idlsrgmulrss1  33476  idlsrgmulrss2  33477  rprmcl  33483  rprmdvds  33484  rprmnz  33485  rprmnunit  33486  rprmasso  33490  rprmirredb  33497  pidufd  33508  1arithufdlem2  33510  1arithufdlem3  33511  zringfrac  33519  ply1dg3rt0irred  33546  m1pmeq  33547  ig1pmindeg  33562  esplysply  33592  exsslsb  33609  ply1degltdimlem  33635  lindsun  33638  fldextfld1  33660  fldextfld2  33661  rtelextdg2  33740  cos9thpiminplylem1  33795  1smat1  33817  submateqlem2  33821  lmatfval  33827  mdetlap1  33839  madjusmdetlem1  33840  madjusmdetlem2  33841  madjusmdetlem3  33842  madjusmdetlem4  33843  zarclssn  33886  zartopn  33888  zarmxt1  33893  rhmpreimacnlem  33897  rhmpreimacn  33898  pnfneige0  33964  pl1cn  33968  rrhqima  34027  esumfzf  34082  esumpcvgval  34091  esumpmono  34092  esumcvg  34099  ldgenpisyslem1  34176  ldgenpisys  34179  measbase  34210  dya2iocnei  34295  oddpwdc  34367  eulerpartlems  34373  eulerpartlemb  34381  sseqf  34405  fibp1  34414  orrvcval4  34478  orrvcoel  34479  orrvccel  34480  ballotlem2  34502  ballotlemfrceq  34542  signsplypnf  34563  signswch  34574  signstf0  34581  signstfvn  34582  signstfvneq0  34585  signstfvcl  34586  signstfveq0  34590  signsvfn  34595  fct2relem  34610  fsum2dsub  34620  reprsuc  34628  reprpmtf1o  34639  breprexplema  34643  breprexplemc  34645  hgt749d  34662  hgt750lemb  34669  tgoldbachgnn  34672  bnj1172  35013  bnj1245  35026  bnj1311  35036  bnj1450  35062  bnj1501  35079  r1elcl  35109  subfacp1lem1  35223  subfacp1lem5  35228  subfacp1lem6  35229  subfacval2  35231  erdszelem7  35241  cvxpconn  35286  cvxsconn  35287  cvmliftlem5  35333  cvmliftlem7  35335  cvmliftlem10  35338  cvmliftlem13  35340  mrsubvrs  35566  msubrn  35573  msubco  35575  msubvrs  35604  r1peuqusdeg1  35687  imageval  35972  fwddifnp1  36209  knoppcnlem8  36544  knoppcnlem10  36546  bj-unirel  37095  icoreunrn  37403  istoprelowl  37404  poimirlem3  37673  poimirlem4  37674  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem12  37682  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  poimirlem28  37698  poimirlem29  37699  poimirlem31  37701  mblfinlem2  37708  ftc1cnnc  37742  upixp  37779  sdclem2  37792  caushft  37811  ismtyres  37858  rrnmet  37879  rrndstprj1  37880  rrndstprj2  37881  rrncmslem  37882  rrnequiv  37885  iccbnd  37890  osumcllem7N  40071  pexmidlem4N  40082  lcfrlem4  41654  lcfrlem5  41655  lcfrlem6  41656  lcfrlem16  41667  lcfrlem38  41689  mapdrvallem2  41754  mapdh8ab  41886  mapdh8ad  41888  mapdh8e  41893  3factsumint3  42126  aks4d1p1p1  42166  fldhmf1  42193  aks6d1c1p2  42212  aks6d1c1p3  42213  aks6d1c1p7  42216  aks6d1c1p6  42217  aks6d1c1p8  42218  aks6d1c1  42219  evl1gprodd  42220  idomnnzpownz  42235  aks6d1c5lem1  42239  aks6d1c5lem3  42240  aks6d1c5lem2  42241  deg1gprod  42243  sticksstones10  42258  aks6d1c6lem3  42275  aks5lem2  42290  aks5lem3a  42292  unitscyglem5  42302  fz1sump1  42413  sumcubes  42416  evlselv  42690  mhphf2  42701  prjspnfv01  42727  prjspner01  42728  prjspner1  42729  mapfzcons  42819  diophren  42916  irrapxlem1  42925  monotuz  43044  acongeq  43086  jm2.26lem3  43104  jm3.1lem2  43121  pw2f1ocnv  43140  idomodle  43294  trclfvdecomr  43831  imo72b2lem0  44268  imo72b2lem1  44272  scottelrankd  44350  dvgrat  44415  cvgdvgrat  44416  hashnzfz2  44424  fcnre  45132  refsumcn  45137  rfcnnnub  45143  disjf1o  45298  disjinfi  45299  ssmapsn  45323  ssuzfz  45458  nnsplit  45467  uzssd2  45525  uzublem  45538  fsumsermpt  45689  climsuselem1  45717  limcperiod  45738  sumnnodd  45740  lptioo2cn  45753  lptioo1cn  45754  climresmpt  45767  allbutfifvre  45783  climleltrp  45784  cnrefiisplem  45937  cncfshift  45982  cncfperiod  45987  cncfshiftioo  46000  fperdvper  46027  dvnmptdivc  46046  dvnmul  46051  dvmptfprod  46053  dvnprodlem3  46056  stoweidlem11  46119  stoweidlem15  46123  stoweidlem17  46125  stoweidlem20  46128  stoweidlem34  46142  stoweidlem35  46143  stoweidlem46  46154  stoweidlem47  46155  stoweidlem56  46164  stoweidlem59  46167  stoweidlem62  46170  stirlinglem5  46186  stirlinglem14  46195  dirkertrigeqlem2  46207  dirkertrigeqlem3  46208  fourierdlem11  46226  fourierdlem15  46230  fourierdlem16  46231  fourierdlem21  46236  fourierdlem22  46237  fourierdlem25  46240  fourierdlem48  46262  fourierdlem52  46266  fourierdlem54  46268  fourierdlem58  46272  fourierdlem62  46276  fourierdlem64  46278  fourierdlem65  46279  fourierdlem69  46283  fourierdlem70  46284  fourierdlem71  46285  fourierdlem73  46287  fourierdlem80  46294  fourierdlem81  46295  fourierdlem83  46297  fourierdlem92  46306  fourierdlem93  46307  fourierdlem97  46311  fourierdlem103  46317  fourierdlem104  46318  fourierdlem112  46326  fourierdlem113  46327  fouriercnp  46334  fouriersw  46339  elaa2lem  46341  etransclem4  46346  etransclem7  46349  etransclem10  46352  etransclem14  46356  etransclem15  46357  etransclem24  46366  etransclem25  46367  etransclem31  46373  etransclem32  46374  etransclem35  46377  etransclem44  46386  etransclem46  46388  qndenserrnopnlem  46405  qndenserrn  46407  prsal  46426  salgencntex  46451  subsaliuncl  46466  subsalsal  46467  sge0tsms  46488  sge0fodjrnlem  46524  sge0isum  46535  iundjiunlem  46567  iundjiun  46568  meadjiunlem  46573  meaiunlelem  46576  meaiuninclem  46588  meaiininc2  46596  caragensplit  46608  carageneld  46610  carageniuncllem1  46629  caratheodorylem1  46634  caratheodorylem2  46635  hoicvr  46656  hsphoidmvle2  46693  hsphoidmvle  46694  hoidmv1lelem2  46700  hoidmv1lelem3  46701  hoidmvlelem2  46704  hoiqssbllem2  46731  pimdecfgtioc  46823  pimincfltioc  46824  pimdecfgtioo  46825  pimincfltioo  46826  smflimlem3  46881  smfmullem4  46902  smfsupxr  46924  smflimsuplem2  46929  smflimsuplem5  46932  ormklocald  46982  natlocalincr  46984  elmod2  47465  isuspgrim0lem  48003  upgrimtrlslem2  48015  ssnn0ssfz  48459  zlmodzxzscm  48467  rmsupp0  48478  lincsum  48540  lincscm  48541  lindslinindimp2lem4  48572  lincresunit3  48592  elbigofrcl  48661  intubeu  49094  unilbeu  49095  cicrcl2  49154  cic1st2nd  49158  imaf1homlem  49218  oppfrcl  49239  eloppf  49244  imasubc  49262  imaid  49265  oppcuprcl5  49312  oppcup3  49320  uptrlem2  49322  uptrlem3  49323  natoppf  49340  elxpcbasex1ALT  49360  elxpcbasex2ALT  49362  swapf1a  49380  swapf2f1oa  49388  swapfida  49391  cofuswapf1  49405  cofuswapf2  49406  fucoppcco  49520  postc  49680  reldmlan2  49728  reldmran2  49729  lanrcl  49732  ranrcl  49733  setrec1  49802  aacllem  49912