Theorem eleqtrdi 2847

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleqtrrdi  2848  3eltr3g  2853  prid2g  4720  ndmfvrcl  6877  fnwelem  8085  tz7.48-1  8386  brwitnlem  8446  oeeulem  8541  dffi3  9348  cnfcom3lem  9626  ttrclse  9650  alephgeom  10006  fpwwe2lem5  10560  canthwelem  10575  hargch  10598  r1wunlim  10662  eluzel2  12770  fseq1p1m1  13528  fznn0sub2  13565  nn0split  13573  seqp1d  13955  exple1  14114  digit1  14174  bcval5  14255  bcpasc  14258  hashf1  14394  seqcoll  14401  seqcoll2  14402  ccatrn  14527  swrdccat2  14607  cats1un  14658  pfxccatin12lem3  14669  splfv2a  14693  splval2  14694  caubnd  15296  limsupgre  15418  clim2ser  15592  clim2ser2  15593  iserex  15594  isermulc2  15595  iserle  15597  iserge0  15598  climub  15599  climserle  15600  isercolllem2  15603  isercolllem3  15604  isercoll  15605  isercoll2  15606  serf0  15618  iseraltlem2  15620  iseraltlem3  15621  iseralt  15622  sumeq2ii  15630  summolem3  15651  summolem2a  15652  fsum  15657  sum0  15658  fsumcl2lem  15668  fsumadd  15677  isumclim3  15696  isumadd  15704  fsump1i  15706  fsummulc2  15721  fsumrelem  15744  iserabs  15752  cvgcmp  15753  cvgcmpub  15754  cvgcmpce  15755  binom1dif  15770  isumshft  15776  isumsplit  15777  isumrpcl  15780  isumsup2  15783  climcndslem1  15786  climcndslem2  15787  climcnds  15788  arisum2  15798  trireciplem  15799  geoser  15804  pwdif  15805  geolim  15807  geo2lim  15812  cvgrat  15820  mertenslem1  15821  mertenslem2  15822  mertens  15823  clim2prod  15825  clim2div  15826  ntrivcvgfvn0  15836  ntrivcvgtail  15837  prodeq2ii  15848  prodmolem3  15870  prodmolem2a  15871  fprod  15878  fprodntriv  15879  fprodss  15885  fprodser  15886  fprodcl2lem  15887  fprodmul  15897  fproddiv  15898  fprodabs  15911  fprodeq0  15912  fprodn0  15916  iprodclim3  15937  iprodmul  15940  fallfacfwd  15973  0fallfac  15974  binomfallfaclem2  15977  fallfacval4  15980  bpolysum  15990  bpolydiflem  15991  fsumkthpow  15993  efcvgfsum  16023  efcj  16029  fprodefsum  16032  effsumlt  16050  ruclem7  16175  bitsfzolem  16375  bitsfzo  16376  bitsfi  16378  bitsinv1lem  16382  bitsinv1  16383  bitsinvp1  16390  sadcp1  16396  sadadd  16408  sadass  16412  bitsres  16414  smupp1  16421  smuval2  16423  smupval  16429  smueqlem  16431  smumul  16434  algrp1  16515  phiprmpw  16717  crth  16719  phimullem  16720  eulerthlem2  16723  prmdiv  16726  pcpremul  16785  pcmpt  16834  pcfac  16841  pockthlem  16847  pockthg  16848  prmreclem2  16859  prmreclem3  16860  prmreclem4  16861  prmreclem5  16862  prmreclem6  16863  prmrec  16864  1arith  16869  vdwapun  16916  vdwlem1  16923  vdwlem2  16924  vdwlem3  16925  vdwlem6  16928  vdwlem8  16930  vdwlem10  16932  vdw  16936  imasvscafn  17472  oppccatid  17656  oppccomfpropd  17664  brcic  17736  funcoppc  17813  invfuc  17915  hofcl  18196  yonedalem4c  18214  chnccats1  18562  gsumwsubmcl  18776  gsumsgrpccat  18779  gsumwmhm  18784  mulgnnp1  19029  mulgnnsubcl  19033  mulgnn0z  19048  mulgnndir  19050  ghmquskerlem1  19229  ghmquskerco  19230  psgnunilem4  19443  psgnran  19461  sylow1lem1  19544  lsmmod2  19622  lsmdisj2r  19631  efginvrel2  19673  efgsdmi  19678  efgsrel  19680  efgs1b  19682  efgsp1  19683  efgredleme  19689  efgredlemc  19691  efgcpbllemb  19701  frgpuplem  19718  mulgnn0di  19771  frgpnabllem1  19819  lt6abl  19841  cycsubgcyg  19847  gsumval3eu  19850  gsumval3  19853  gsumzcl2  19856  gsumzaddlem  19867  gsumconst  19880  gsumzmhm  19883  gsumzoppg  19890  telgsumfz0s  19937  dprdwd  19959  dprd2da  19990  pgpfaclem1  20029  srgbinom  20183  isirred  20372  idomdomd  20676  idomcringd  20677  lspprid2  20966  lspsnat  21117  lsppratlem1  21119  lsppratlem3  21121  lidl0cl  21192  lidlacl  21193  lidlnegcl  21194  elrspsn  21212  2idllidld  21226  2idlridld  21227  rng2idl1cntr  21277  psgnghm  21552  frlmvscavalb  21742  frlmvplusgscavalb  21743  psrbaglefi  21899  psrass23l  21939  psrass23  21941  mplcoe5lem  22011  mpfind  22087  selvval  22095  mhpvscacl  22114  psr1bascl  22158  ply1basf  22160  gsummoncoe1  22269  lply1binom  22271  lply1binomsc  22272  mpfpf1  22312  pf1mpf  22313  evl1scvarpw  22324  evl1maprhm  22340  matbas2i  22383  matecld  22387  matgsum  22398  mpomatmul  22407  dmatmul  22458  1mavmul  22509  mdetleib2  22549  m1detdiag  22558  marep01ma  22621  smadiadetlem4  22630  slesolinv  22641  pmatcollpw3fi1lem1  22747  chpscmat  22803  chpscmatgsumbin  22805  chp0mat  22807  chpidmat  22808  chfacfisf  22815  chfacfisfcpmat  22816  chfacfpmmulgsum2  22826  cldrcl  22987  ordtbas  23153  iscnp2  23200  dis1stc  23460  ptbasfi  23542  ptpjopn  23573  ptclsg  23576  ptcnp  23583  kqtop  23706  reghmph  23754  ptcmplem2  24014  ptcmplem3  24015  ptcmplem4  24016  tsmslem1  24090  utop2nei  24211  isucn2  24239  cuspcvg  24261  cnextucn  24263  imasdsf1olem  24334  blcvx  24759  xrhmeo  24917  cnrehmeo  24924  cnrehmeoOLD  24925  evth  24931  reparphti  24969  reparphtiOLD  24970  iscau4  25252  iscmet3lem1  25264  lmle  25274  rrxfsupp  25375  rrxdsfi  25384  pjthlem2  25411  ovollb2lem  25462  ovolunlem1a  25470  ovoliunlem1  25476  ovoliun2  25480  ovolscalem1  25487  ovolicc1  25490  ovolicc2lem4  25494  iundisj2  25523  voliunlem1  25524  volsup  25530  ioombl1lem4  25535  uniioovol  25553  uniioombllem3  25559  uniioombllem4  25560  uniioombllem6  25562  vitalilem5  25586  mbfimaopnlem  25629  mbflimsup  25640  mbfi1fseqlem3  25691  iblitg  25742  dvcnp2  25894  dvnp1  25900  cpncn  25911  dvmulbr  25914  dvcobr  25922  dvlip2  25973  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem3  26008  dvfsumrlimge0  26010  dvfsumrlim2  26012  ftc1cn  26023  elplyd  26180  ply1termlem  26181  ply1term  26182  ply0  26186  plyeq0lem  26188  plyaddlem1  26191  plymullem1  26192  plyaddlem  26193  plymullem  26194  coeeulem  26202  plyco  26219  coeeq2  26220  coefv0  26226  coemulhi  26232  coemulc  26233  plycj  26256  plycjOLD  26258  dvply1  26264  vieta1lem2  26292  elqaalem2  26301  dvtaylp  26351  dvntaylp  26352  taylthlem1  26354  taylth  26357  ulmres  26370  ulmshftlem  26371  ulmshft  26372  ulmcau  26377  ulmdvlem1  26382  mtest  26386  mtestbdd  26387  pserulm  26404  psercn2  26405  psercn2OLD  26406  psercnlem1  26408  psercn  26409  pserdvlem2  26411  abelthlem6  26419  abelth  26424  efif1olem1  26524  efif1olem3  26526  efif1olem4  26527  logcn  26629  advlogexp  26637  efopn  26640  cxpeq  26740  asinsin  26875  atantayl  26920  leibpilem2  26924  birthdaylem2  26935  birthdaylem3  26936  efrlim  26952  efrlimOLD  26953  emcllem2  26980  emcllem5  26983  emcllem7  26985  harmonicbnd4  26994  fsumharmonic  26995  lgamgulm2  27019  lgamcvglem  27023  lgamcvg2  27038  gamcvg2lem  27042  wilthlem2  27052  wilthlem3  27053  ftalem1  27056  ftalem2  27057  ftalem3  27058  ftalem5  27060  basellem2  27065  basellem3  27066  basellem5  27068  basellem8  27071  ppiprm  27134  ppinprm  27135  chtprm  27136  chtnprm  27137  chpp1  27138  vma1  27149  ppiltx  27160  musum  27174  0sgmppw  27182  1sgmprm  27183  ppiublem2  27187  chtublem  27195  fsumvma2  27198  chpchtsum  27203  logexprlim  27209  bposlem5  27272  lgscllem  27288  lgsval2lem  27291  lgsval4a  27303  lgsneg  27305  lgsdir2lem3  27311  lgsdir2lem5  27313  lgsdir  27316  lgsdilem2  27317  lgsdi  27318  lgsne0  27319  gausslemma2dlem3  27352  lgseisenlem1  27359  lgsquadlem2  27365  chebbnd1lem1  27453  chtppilimlem1  27457  rplogsumlem2  27469  rpvmasumlem  27471  dchrisumlem1  27473  dchrisumlem2  27474  dchrmusum2  27478  dchrvmasum2lem  27480  dchrvmasumiflem1  27485  dchrisum0flblem1  27492  dchrisum0flblem2  27493  dchrisum0flb  27494  dchrisum0re  27497  dchrisum0lem1b  27499  dchrisum0lem1  27500  dchrisum0lem2a  27501  dchrisum0lem2  27502  dchrisum0lem3  27503  mudivsum  27514  mulogsum  27516  mulog2sumlem2  27519  selberg2lem  27534  logdivbnd  27540  pntrsumo1  27549  pntrsumbnd2  27551  pntrlog2bndlem2  27562  pntrlog2bndlem4  27564  pntrlog2bndlem6a  27566  pntlemj  27587  pntlemf  27589  ostth2lem3  27619  madebdayim  27901  oldbdayim  27902  newbdayim  27916  cutminmax  27949  noseqp1  28304  tglngne  28640  ltgseg  28686  eedimeq  28989  axlowdimlem16  29048  ebtwntg  29073  subgruhgredgd  29375  subumgredg2  29376  umgrres1lem  29401  wlkson  29746  wksonproplem  29794  trlsonfval  29795  pthsonfval  29831  spthson  29832  crctcshwlkn0lem4  29904  crctcshwlkn0lem5  29905  eupth2lems  30331  numclwwlk1lem2foa  30447  numclwlk1lem2  30463  numclwwlk2lem1  30469  htthlem  31011  hhsscms  31372  shmodsi  31483  pjoc1i  31525  5oalem1  31748  mayete3i  31822  adj1  32027  iundisj2f  32683  fmptco1f1o  32729  fcnvgreu  32768  suppovss  32777  ssnnssfz  32884  nn0diffz0  32891  iundisj2fi  32894  indpreima  32964  ccatws1f1o  33050  cshw1s2  33059  gsumhashmul  33167  gsummulsubdishift1  33168  gsumwrd2dccat  33178  fzo0pmtrlast  33192  wrdpmtrlast  33193  pmtrto1cl  33199  psgnfzto1stlem  33200  fzto1st1  33202  cycpmfv1  33213  cycpmfv2  33214  cycpmco2rn  33225  cycpmco2lem4  33229  cycpmco2lem5  33230  cycpmco2lem6  33231  cyc3evpm  33250  cyc3genpm  33252  cycpmconjslem2  33255  cyc3conja  33257  elrgspnlem1  33342  elrgspnlem2  33343  erler  33365  idomrcanOLD  33382  nsgmgc  33511  nsgqusf1olem2  33513  unitpidl1  33523  elrspunsn  33528  ssdifidllem  33555  mxidlirredi  33570  mxidlirred  33571  opprqusplusg  33588  opprqus0g  33589  opprqusmulr  33590  idlsrgmulrss1  33610  idlsrgmulrss2  33611  rprmcl  33617  rprmdvds  33618  rprmnz  33619  rprmnunit  33620  rprmasso  33624  rprmirredb  33631  pidufd  33642  1arithufdlem2  33644  1arithufdlem3  33645  zringfrac  33653  ply1dg3rt0irred  33683  m1pmeq  33684  ig1pmindeg  33701  extvfvvcl  33718  evlextv  33725  psrmonprod  33735  esplysply  33754  esplyind  33758  esplyfvn  33760  vietalem  33762  exsslsb  33780  ply1degltdimlem  33806  lindsun  33809  fldextfld1  33831  fldextfld2  33832  rtelextdg2  33911  cos9thpiminplylem1  33966  1smat1  33988  submateqlem2  33992  lmatfval  33998  mdetlap1  34010  madjusmdetlem1  34011  madjusmdetlem2  34012  madjusmdetlem3  34013  madjusmdetlem4  34014  zarclssn  34057  zartopn  34059  zarmxt1  34064  rhmpreimacnlem  34068  rhmpreimacn  34069  pnfneige0  34135  pl1cn  34139  rrhqima  34198  esumfzf  34253  esumpcvgval  34262  esumpmono  34263  esumcvg  34270  ldgenpisyslem1  34347  ldgenpisys  34350  measbase  34381  dya2iocnei  34466  oddpwdc  34538  eulerpartlems  34544  eulerpartlemb  34552  sseqf  34576  fibp1  34585  orrvcval4  34649  orrvcoel  34650  orrvccel  34651  ballotlem2  34673  ballotlemfrceq  34713  signsplypnf  34734  signswch  34745  signstf0  34752  signstfvn  34753  signstfvneq0  34756  signstfvcl  34757  signstfveq0  34761  signsvfn  34766  fct2relem  34781  fsum2dsub  34791  reprsuc  34799  reprpmtf1o  34810  breprexplema  34814  breprexplemc  34816  hgt749d  34833  hgt750lemb  34840  tgoldbachgnn  34843  bnj1172  35183  bnj1245  35196  bnj1311  35206  bnj1450  35232  bnj1501  35249  r1elcl  35281  subfacp1lem1  35401  subfacp1lem5  35406  subfacp1lem6  35407  subfacval2  35409  erdszelem7  35419  cvxpconn  35464  cvxsconn  35465  cvmliftlem5  35511  cvmliftlem7  35513  cvmliftlem10  35516  cvmliftlem13  35518  mrsubvrs  35744  msubrn  35751  msubco  35753  msubvrs  35782  r1peuqusdeg1  35865  imageval  36150  fwddifnp1  36387  knoppcnlem8  36728  knoppcnlem10  36730  bj-unirel  37326  icoreunrn  37641  istoprelowl  37642  poimirlem3  37903  poimirlem4  37904  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem12  37912  poimirlem15  37915  poimirlem16  37916  poimirlem17  37917  poimirlem18  37918  poimirlem19  37919  poimirlem20  37920  poimirlem21  37921  poimirlem22  37922  poimirlem23  37923  poimirlem24  37924  poimirlem25  37925  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  poimirlem29  37929  poimirlem31  37931  mblfinlem2  37938  ftc1cnnc  37972  upixp  38009  sdclem2  38022  caushft  38041  ismtyres  38088  rrnmet  38109  rrndstprj1  38110  rrndstprj2  38111  rrncmslem  38112  rrnequiv  38115  iccbnd  38120  osumcllem7N  40367  pexmidlem4N  40378  lcfrlem4  41950  lcfrlem5  41951  lcfrlem6  41952  lcfrlem16  41963  lcfrlem38  41985  mapdrvallem2  42050  mapdh8ab  42182  mapdh8ad  42184  mapdh8e  42189  3factsumint3  42422  aks4d1p1p1  42462  fldhmf1  42489  aks6d1c1p2  42508  aks6d1c1p3  42509  aks6d1c1p7  42512  aks6d1c1p6  42513  aks6d1c1p8  42514  aks6d1c1  42515  evl1gprodd  42516  idomnnzpownz  42531  aks6d1c5lem1  42535  aks6d1c5lem3  42536  aks6d1c5lem2  42537  deg1gprod  42539  sticksstones10  42554  aks6d1c6lem3  42571  aks5lem2  42586  aks5lem3a  42588  unitscyglem5  42598  fz1sump1  42709  sumcubes  42712  evlselv  42974  mhphf2  42985  prjspnfv01  43011  prjspner01  43012  prjspner1  43013  mapfzcons  43102  diophren  43199  irrapxlem1  43208  monotuz  43327  acongeq  43369  jm2.26lem3  43387  jm3.1lem2  43404  pw2f1ocnv  43423  idomodle  43577  trclfvdecomr  44113  imo72b2lem0  44550  imo72b2lem1  44554  scottelrankd  44632  dvgrat  44697  cvgdvgrat  44698  hashnzfz2  44706  fcnre  45414  refsumcn  45419  rfcnnnub  45425  disjf1o  45579  disjinfi  45580  ssmapsn  45603  ssuzfz  45737  nnsplit  45746  uzssd2  45804  uzublem  45817  fsumsermpt  45968  climsuselem1  45996  limcperiod  46017  sumnnodd  46019  lptioo2cn  46032  lptioo1cn  46033  climresmpt  46046  allbutfifvre  46062  climleltrp  46063  cnrefiisplem  46216  cncfshift  46261  cncfperiod  46266  cncfshiftioo  46279  fperdvper  46306  dvnmptdivc  46325  dvnmul  46330  dvmptfprod  46332  dvnprodlem3  46335  stoweidlem11  46398  stoweidlem15  46402  stoweidlem17  46404  stoweidlem20  46407  stoweidlem34  46421  stoweidlem35  46422  stoweidlem46  46433  stoweidlem47  46434  stoweidlem56  46443  stoweidlem59  46446  stoweidlem62  46449  stirlinglem5  46465  stirlinglem14  46474  dirkertrigeqlem2  46486  dirkertrigeqlem3  46487  fourierdlem11  46505  fourierdlem15  46509  fourierdlem16  46510  fourierdlem21  46515  fourierdlem22  46516  fourierdlem25  46519  fourierdlem48  46541  fourierdlem52  46545  fourierdlem54  46547  fourierdlem58  46551  fourierdlem62  46555  fourierdlem64  46557  fourierdlem65  46558  fourierdlem69  46562  fourierdlem70  46563  fourierdlem71  46564  fourierdlem73  46566  fourierdlem80  46573  fourierdlem81  46574  fourierdlem83  46576  fourierdlem92  46585  fourierdlem93  46586  fourierdlem97  46590  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem113  46606  fouriercnp  46613  fouriersw  46618  elaa2lem  46620  etransclem4  46625  etransclem7  46628  etransclem10  46631  etransclem14  46635  etransclem15  46636  etransclem24  46645  etransclem25  46646  etransclem31  46652  etransclem32  46653  etransclem35  46656  etransclem44  46665  etransclem46  46667  qndenserrnopnlem  46684  qndenserrn  46686  prsal  46705  salgencntex  46730  subsaliuncl  46745  subsalsal  46746  sge0tsms  46767  sge0fodjrnlem  46803  sge0isum  46814  iundjiunlem  46846  iundjiun  46847  meadjiunlem  46852  meaiunlelem  46855  meaiuninclem  46867  meaiininc2  46875  caragensplit  46887  carageneld  46889  carageniuncllem1  46908  caratheodorylem1  46913  caratheodorylem2  46914  hoicvr  46935  hsphoidmvle2  46972  hsphoidmvle  46973  hoidmv1lelem2  46979  hoidmv1lelem3  46980  hoidmvlelem2  46983  hoiqssbllem2  47010  pimdecfgtioc  47102  pimincfltioc  47103  pimdecfgtioo  47104  pimincfltioo  47105  smflimlem3  47160  smfmullem4  47181  smfsupxr  47203  smflimsuplem2  47208  smflimsuplem5  47211  ormklocald  47261  natlocalincr  47263  elmod2  47744  isuspgrim0lem  48282  upgrimtrlslem2  48294  ssnn0ssfz  48738  zlmodzxzscm  48746  rmsupp0  48757  lincsum  48818  lincscm  48819  lindslinindimp2lem4  48850  lincresunit3  48870  elbigofrcl  48939  intubeu  49372  unilbeu  49373  cicrcl2  49431  cic1st2nd  49435  imaf1homlem  49495  oppfrcl  49516  eloppf  49521  imasubc  49539  imaid  49542  oppcuprcl5  49589  oppcup3  49597  uptrlem2  49599  uptrlem3  49600  natoppf  49617  elxpcbasex1ALT  49637  elxpcbasex2ALT  49639  swapf1a  49657  swapf2f1oa  49665  swapfida  49668  cofuswapf1  49682  cofuswapf2  49683  fucoppcco  49797  postc  49957  reldmlan2  50005  reldmran2  50006  lanrcl  50009  ranrcl  50010  setrec1  50079  aacllem  50189