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  4721  ndmfvrcl  6876  fnwelem  8087  tz7.48-1  8388  brwitnlem  8448  oeeulem  8542  dffi3  9358  cnfcom3lem  9632  ttrclse  9656  alephgeom  10011  fpwwe2lem5  10564  canthwelem  10579  hargch  10602  r1wunlim  10666  eluzel2  12774  fseq1p1m1  13535  fznn0sub2  13572  nn0split  13580  seqp1d  13959  exple1  14118  digit1  14178  bcval5  14259  bcpasc  14262  hashf1  14398  seqcoll  14405  seqcoll2  14406  ccatrn  14530  swrdccat2  14610  cats1un  14662  pfxccatin12lem3  14673  splfv2a  14697  splval2  14698  caubnd  15301  limsupgre  15423  clim2ser  15597  clim2ser2  15598  iserex  15599  isermulc2  15600  iserle  15602  iserge0  15603  climub  15604  climserle  15605  isercolllem2  15608  isercolllem3  15609  isercoll  15610  isercoll2  15611  serf0  15623  iseraltlem2  15625  iseraltlem3  15626  iseralt  15627  sumeq2ii  15635  summolem3  15656  summolem2a  15657  fsum  15662  sum0  15663  fsumcl2lem  15673  fsumadd  15682  isumclim3  15701  isumadd  15709  fsump1i  15711  fsummulc2  15726  fsumrelem  15749  iserabs  15757  cvgcmp  15758  cvgcmpub  15759  cvgcmpce  15760  binom1dif  15775  isumshft  15781  isumsplit  15782  isumrpcl  15785  isumsup2  15788  climcndslem1  15791  climcndslem2  15792  climcnds  15793  arisum2  15803  trireciplem  15804  geoser  15809  pwdif  15810  geolim  15812  geo2lim  15817  cvgrat  15825  mertenslem1  15826  mertenslem2  15827  mertens  15828  clim2prod  15830  clim2div  15831  ntrivcvgfvn0  15841  ntrivcvgtail  15842  prodeq2ii  15853  prodmolem3  15875  prodmolem2a  15876  fprod  15883  fprodntriv  15884  fprodss  15890  fprodser  15891  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodabs  15916  fprodeq0  15917  fprodn0  15921  iprodclim3  15942  iprodmul  15945  fallfacfwd  15978  0fallfac  15979  binomfallfaclem2  15982  fallfacval4  15985  bpolysum  15995  bpolydiflem  15996  fsumkthpow  15998  efcvgfsum  16028  efcj  16034  fprodefsum  16037  effsumlt  16055  ruclem7  16180  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  16520  phiprmpw  16722  crth  16724  phimullem  16725  eulerthlem2  16728  prmdiv  16731  pcpremul  16790  pcmpt  16839  pcfac  16846  pockthlem  16852  pockthg  16853  prmreclem2  16864  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  prmrec  16869  1arith  16874  vdwapun  16921  vdwlem1  16928  vdwlem2  16929  vdwlem3  16930  vdwlem6  16933  vdwlem8  16935  vdwlem10  16937  vdw  16941  imasvscafn  17476  oppccatid  17660  oppccomfpropd  17668  brcic  17740  funcoppc  17817  invfuc  17919  hofcl  18200  yonedalem4c  18218  gsumwsubmcl  18746  gsumsgrpccat  18749  gsumwmhm  18754  mulgnnp1  18996  mulgnnsubcl  19000  mulgnn0z  19015  mulgnndir  19017  ghmquskerlem1  19197  ghmquskerco  19198  psgnunilem4  19411  psgnran  19429  sylow1lem1  19512  lsmmod2  19590  lsmdisj2r  19599  efginvrel2  19641  efgsdmi  19646  efgsrel  19648  efgs1b  19650  efgsp1  19651  efgredleme  19657  efgredlemc  19659  efgcpbllemb  19669  frgpuplem  19686  mulgnn0di  19739  frgpnabllem1  19787  lt6abl  19809  cycsubgcyg  19815  gsumval3eu  19818  gsumval3  19821  gsumzcl2  19824  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  telgsumfz0s  19905  dprdwd  19927  dprd2da  19958  pgpfaclem1  19997  srgbinom  20151  isirred  20339  idomdomd  20646  idomcringd  20647  lspprid2  20936  lspsnat  21087  lsppratlem1  21089  lsppratlem3  21091  lidl0cl  21162  lidlacl  21163  lidlnegcl  21164  elrspsn  21182  2idllidld  21196  2idlridld  21197  rng2idl1cntr  21247  psgnghm  21522  frlmvscavalb  21712  frlmvplusgscavalb  21713  psrbaglefi  21868  psrass23l  21909  psrass23  21911  mplcoe5lem  21979  mpfind  22047  selvval  22055  mhpvscacl  22074  psr1bascl  22118  ply1basf  22120  gsummoncoe1  22228  lply1binom  22230  lply1binomsc  22231  mpfpf1  22271  pf1mpf  22272  evl1scvarpw  22283  evl1maprhm  22299  matbas2i  22342  matecld  22346  matgsum  22357  mpomatmul  22366  dmatmul  22417  1mavmul  22468  mdetleib2  22508  m1detdiag  22517  marep01ma  22580  smadiadetlem4  22589  slesolinv  22600  pmatcollpw3fi1lem1  22706  chpscmat  22762  chpscmatgsumbin  22764  chp0mat  22766  chpidmat  22767  chfacfisf  22774  chfacfisfcpmat  22775  chfacfpmmulgsum2  22785  cldrcl  22946  ordtbas  23112  iscnp2  23159  dis1stc  23419  ptbasfi  23501  ptpjopn  23532  ptclsg  23535  ptcnp  23542  kqtop  23665  reghmph  23713  ptcmplem2  23973  ptcmplem3  23974  ptcmplem4  23975  tsmslem1  24049  utop2nei  24171  isucn2  24199  cuspcvg  24221  cnextucn  24223  imasdsf1olem  24294  blcvx  24719  xrhmeo  24877  cnrehmeo  24884  cnrehmeoOLD  24885  evth  24891  reparphti  24929  reparphtiOLD  24930  iscau4  25212  iscmet3lem1  25224  lmle  25234  rrxfsupp  25335  rrxdsfi  25344  pjthlem2  25371  ovollb2lem  25422  ovolunlem1a  25430  ovoliunlem1  25436  ovoliun2  25440  ovolscalem1  25447  ovolicc1  25450  ovolicc2lem4  25454  iundisj2  25483  voliunlem1  25484  volsup  25490  ioombl1lem4  25495  uniioovol  25513  uniioombllem3  25519  uniioombllem4  25520  uniioombllem6  25522  vitalilem5  25546  mbfimaopnlem  25589  mbflimsup  25600  mbfi1fseqlem3  25651  iblitg  25702  dvcnp2  25854  dvnp1  25860  cpncn  25871  dvmulbr  25874  dvcobr  25882  dvlip2  25933  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumrlimge0  25970  dvfsumrlim2  25972  ftc1cn  25983  elplyd  26140  ply1termlem  26141  ply1term  26142  ply0  26146  plyeq0lem  26148  plyaddlem1  26151  plymullem1  26152  plyaddlem  26153  plymullem  26154  coeeulem  26162  plyco  26179  coeeq2  26180  coefv0  26186  coemulhi  26192  coemulc  26193  plycj  26216  plycjOLD  26218  dvply1  26224  vieta1lem2  26252  elqaalem2  26261  dvtaylp  26311  dvntaylp  26312  taylthlem1  26314  taylth  26317  ulmres  26330  ulmshftlem  26331  ulmshft  26332  ulmcau  26337  ulmdvlem1  26342  mtest  26346  mtestbdd  26347  pserulm  26364  psercn2  26365  psercn2OLD  26366  psercnlem1  26368  psercn  26369  pserdvlem2  26371  abelthlem6  26379  abelth  26384  efif1olem1  26484  efif1olem3  26486  efif1olem4  26487  logcn  26589  advlogexp  26597  efopn  26600  cxpeq  26700  asinsin  26835  atantayl  26880  leibpilem2  26884  birthdaylem2  26895  birthdaylem3  26896  efrlim  26912  efrlimOLD  26913  emcllem2  26940  emcllem5  26943  emcllem7  26945  harmonicbnd4  26954  fsumharmonic  26955  lgamgulm2  26979  lgamcvglem  26983  lgamcvg2  26998  gamcvg2lem  27002  wilthlem2  27012  wilthlem3  27013  ftalem1  27016  ftalem2  27017  ftalem3  27018  ftalem5  27020  basellem2  27025  basellem3  27026  basellem5  27028  basellem8  27031  ppiprm  27094  ppinprm  27095  chtprm  27096  chtnprm  27097  chpp1  27098  vma1  27109  ppiltx  27120  musum  27134  0sgmppw  27142  1sgmprm  27143  ppiublem2  27147  chtublem  27155  fsumvma2  27158  chpchtsum  27163  logexprlim  27169  bposlem5  27232  lgscllem  27248  lgsval2lem  27251  lgsval4a  27263  lgsneg  27265  lgsdir2lem3  27271  lgsdir2lem5  27273  lgsdir  27276  lgsdilem2  27277  lgsdi  27278  lgsne0  27279  gausslemma2dlem3  27312  lgseisenlem1  27319  lgsquadlem2  27325  chebbnd1lem1  27413  chtppilimlem1  27417  rplogsumlem2  27429  rpvmasumlem  27431  dchrisumlem1  27433  dchrisumlem2  27434  dchrmusum2  27438  dchrvmasum2lem  27440  dchrvmasumiflem1  27445  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0flb  27454  dchrisum0re  27457  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  dchrisum0lem3  27463  mudivsum  27474  mulogsum  27476  mulog2sumlem2  27479  selberg2lem  27494  logdivbnd  27500  pntrsumo1  27509  pntrsumbnd2  27511  pntrlog2bndlem2  27522  pntrlog2bndlem4  27524  pntrlog2bndlem6a  27526  pntlemj  27547  pntlemf  27549  ostth2lem3  27579  madebdayim  27837  oldbdayim  27838  newbdayim  27852  noseqp1  28225  tglngne  28530  ltgseg  28576  eedimeq  28878  axlowdimlem16  28937  ebtwntg  28962  subgruhgredgd  29264  subumgredg2  29265  umgrres1lem  29290  wlkson  29635  wksonproplem  29683  trlsonfval  29684  pthsonfval  29720  spthson  29721  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  eupth2lems  30217  numclwwlk1lem2foa  30333  numclwlk1lem2  30349  numclwwlk2lem1  30355  htthlem  30896  hhsscms  31257  shmodsi  31368  pjoc1i  31410  5oalem1  31633  mayete3i  31707  adj1  31912  iundisj2f  32569  fmptco1f1o  32607  fcnvgreu  32647  suppovss  32654  ssnnssfz  32760  iundisj2fi  32770  indpreima  32838  ccatws1f1o  32923  cshw1s2  32932  chnccats1  32987  gsumhashmul  33044  gsumwrd2dccat  33050  fzo0pmtrlast  33064  wrdpmtrlast  33065  pmtrto1cl  33071  psgnfzto1stlem  33072  fzto1st1  33074  cycpmfv1  33085  cycpmfv2  33086  cycpmco2rn  33097  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cyc3evpm  33122  cyc3genpm  33124  cycpmconjslem2  33127  cyc3conja  33129  elrgspnlem1  33209  elrgspnlem2  33210  erler  33232  idomrcanOLD  33248  nsgmgc  33376  nsgqusf1olem2  33378  unitpidl1  33388  elrspunsn  33393  ssdifidllem  33420  mxidlirredi  33435  mxidlirred  33436  opprqusplusg  33453  opprqus0g  33454  opprqusmulr  33455  idlsrgmulrss1  33475  idlsrgmulrss2  33476  rprmcl  33482  rprmdvds  33483  rprmnz  33484  rprmnunit  33485  rprmasso  33489  rprmirredb  33496  pidufd  33507  1arithufdlem2  33509  1arithufdlem3  33510  zringfrac  33518  ply1dg3rt0irred  33544  m1pmeq  33545  ig1pmindeg  33560  exsslsb  33585  ply1degltdimlem  33611  lindsun  33614  fldextfld1  33636  fldextfld2  33637  rtelextdg2  33710  cos9thpiminplylem1  33765  1smat1  33787  submateqlem2  33791  lmatfval  33797  mdetlap1  33809  madjusmdetlem1  33810  madjusmdetlem2  33811  madjusmdetlem3  33812  madjusmdetlem4  33813  zarclssn  33856  zartopn  33858  zarmxt1  33863  rhmpreimacnlem  33867  rhmpreimacn  33868  pnfneige0  33934  pl1cn  33938  rrhqima  33997  esumfzf  34052  esumpcvgval  34061  esumpmono  34062  esumcvg  34069  ldgenpisyslem1  34146  ldgenpisys  34149  measbase  34180  dya2iocnei  34266  oddpwdc  34338  eulerpartlems  34344  eulerpartlemb  34352  sseqf  34376  fibp1  34385  orrvcval4  34449  orrvcoel  34450  orrvccel  34451  ballotlem2  34473  ballotlemfrceq  34513  signsplypnf  34534  signswch  34545  signstf0  34552  signstfvn  34553  signstfvneq0  34556  signstfvcl  34557  signstfveq0  34561  signsvfn  34566  fct2relem  34581  fsum2dsub  34591  reprsuc  34599  reprpmtf1o  34610  breprexplema  34614  breprexplemc  34616  hgt749d  34633  hgt750lemb  34640  tgoldbachgnn  34643  bnj1172  34984  bnj1245  34997  bnj1311  35007  bnj1450  35033  bnj1501  35050  subfacp1lem1  35159  subfacp1lem5  35164  subfacp1lem6  35165  subfacval2  35167  erdszelem7  35177  cvxpconn  35222  cvxsconn  35223  cvmliftlem5  35269  cvmliftlem7  35271  cvmliftlem10  35274  cvmliftlem13  35276  mrsubvrs  35502  msubrn  35509  msubco  35511  msubvrs  35540  r1peuqusdeg1  35623  imageval  35911  fwddifnp1  36146  knoppcnlem8  36481  knoppcnlem10  36483  bj-unirel  37032  icoreunrn  37340  istoprelowl  37341  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem12  37619  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  poimirlem29  37636  poimirlem31  37638  mblfinlem2  37645  ftc1cnnc  37679  upixp  37716  sdclem2  37729  caushft  37748  ismtyres  37795  rrnmet  37816  rrndstprj1  37817  rrndstprj2  37818  rrncmslem  37819  rrnequiv  37822  iccbnd  37827  osumcllem7N  39949  pexmidlem4N  39960  lcfrlem4  41532  lcfrlem5  41533  lcfrlem6  41534  lcfrlem16  41545  lcfrlem38  41567  mapdrvallem2  41632  mapdh8ab  41764  mapdh8ad  41766  mapdh8e  41771  3factsumint3  42004  aks4d1p1p1  42044  fldhmf1  42071  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c1  42097  evl1gprodd  42098  idomnnzpownz  42113  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  sticksstones10  42136  aks6d1c6lem3  42153  aks5lem2  42168  aks5lem3a  42170  unitscyglem5  42180  fz1sump1  42291  sumcubes  42294  evlselv  42568  mhphf2  42579  prjspnfv01  42605  prjspner01  42606  prjspner1  42607  mapfzcons  42697  diophren  42794  irrapxlem1  42803  monotuz  42923  acongeq  42965  jm2.26lem3  42983  jm3.1lem2  43000  pw2f1ocnv  43019  idomodle  43173  trclfvdecomr  43710  imo72b2lem0  44147  imo72b2lem1  44151  scottelrankd  44229  dvgrat  44294  cvgdvgrat  44295  hashnzfz2  44303  fcnre  45012  refsumcn  45017  rfcnnnub  45023  disjf1o  45178  disjinfi  45179  ssmapsn  45203  ssuzfz  45338  nnsplit  45347  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  47886  upgrimtrlslem2  47898  ssnn0ssfz  48330  zlmodzxzscm  48338  rmsupp0  48349  lincsum  48411  lincscm  48412  lindslinindimp2lem4  48443  lincresunit3  48463  elbigofrcl  48532  intubeu  48965  unilbeu  48966  cicrcl2  49025  cic1st2nd  49029  imaf1homlem  49089  oppfrcl  49110  eloppf  49115  imasubc  49133  imaid  49136  oppcuprcl5  49183  oppcup3  49191  uptrlem2  49193  uptrlem3  49194  natoppf  49211  elxpcbasex1ALT  49231  elxpcbasex2ALT  49233  swapf1a  49251  swapf2f1oa  49259  swapfida  49262  cofuswapf1  49276  cofuswapf2  49277  fucoppcco  49391  postc  49551  reldmlan2  49599  reldmran2  49600  lanrcl  49603  ranrcl  49604  setrec1  49673  aacllem  49783