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  4706  ndmfvrcl  6865  fnwelem  8072  tz7.48-1  8373  brwitnlem  8433  oeeulem  8528  dffi3  9335  cnfcom3lem  9613  ttrclse  9637  alephgeom  9993  fpwwe2lem5  10547  canthwelem  10562  hargch  10585  r1wunlim  10649  eluzel2  12757  fseq1p1m1  13515  fznn0sub2  13552  nn0split  13560  seqp1d  13942  exple1  14101  digit1  14161  bcval5  14242  bcpasc  14245  hashf1  14381  seqcoll  14388  seqcoll2  14389  ccatrn  14514  swrdccat2  14594  cats1un  14645  pfxccatin12lem3  14656  splfv2a  14680  splval2  14681  caubnd  15283  limsupgre  15405  clim2ser  15579  clim2ser2  15580  iserex  15581  isermulc2  15582  iserle  15584  iserge0  15585  climub  15586  climserle  15587  isercolllem2  15590  isercolllem3  15591  isercoll  15592  isercoll2  15593  serf0  15605  iseraltlem2  15607  iseraltlem3  15608  iseralt  15609  sumeq2ii  15617  summolem3  15638  summolem2a  15639  fsum  15644  sum0  15645  fsumcl2lem  15655  fsumadd  15664  isumclim3  15683  isumadd  15691  fsump1i  15693  fsummulc2  15708  fsumrelem  15731  iserabs  15739  cvgcmp  15740  cvgcmpub  15741  cvgcmpce  15742  binom1dif  15757  isumshft  15763  isumsplit  15764  isumrpcl  15767  isumsup2  15770  climcndslem1  15773  climcndslem2  15774  climcnds  15775  arisum2  15785  trireciplem  15786  geoser  15791  pwdif  15792  geolim  15794  geo2lim  15799  cvgrat  15807  mertenslem1  15808  mertenslem2  15809  mertens  15810  clim2prod  15812  clim2div  15813  ntrivcvgfvn0  15823  ntrivcvgtail  15824  prodeq2ii  15835  prodmolem3  15857  prodmolem2a  15858  fprod  15865  fprodntriv  15866  fprodss  15872  fprodser  15873  fprodcl2lem  15874  fprodmul  15884  fproddiv  15885  fprodabs  15898  fprodeq0  15899  fprodn0  15903  iprodclim3  15924  iprodmul  15927  fallfacfwd  15960  0fallfac  15961  binomfallfaclem2  15964  fallfacval4  15967  bpolysum  15977  bpolydiflem  15978  fsumkthpow  15980  efcvgfsum  16010  efcj  16016  fprodefsum  16019  effsumlt  16037  ruclem7  16162  bitsfzolem  16362  bitsfzo  16363  bitsfi  16365  bitsinv1lem  16369  bitsinv1  16370  bitsinvp1  16377  sadcp1  16383  sadadd  16395  sadass  16399  bitsres  16401  smupp1  16408  smuval2  16410  smupval  16416  smueqlem  16418  smumul  16421  algrp1  16502  phiprmpw  16704  crth  16706  phimullem  16707  eulerthlem2  16710  prmdiv  16713  pcpremul  16772  pcmpt  16821  pcfac  16828  pockthlem  16834  pockthg  16835  prmreclem2  16846  prmreclem3  16847  prmreclem4  16848  prmreclem5  16849  prmreclem6  16850  prmrec  16851  1arith  16856  vdwapun  16903  vdwlem1  16910  vdwlem2  16911  vdwlem3  16912  vdwlem6  16915  vdwlem8  16917  vdwlem10  16919  vdw  16923  imasvscafn  17459  oppccatid  17643  oppccomfpropd  17651  brcic  17723  funcoppc  17800  invfuc  17902  hofcl  18183  yonedalem4c  18201  chnccats1  18549  gsumwsubmcl  18763  gsumsgrpccat  18766  gsumwmhm  18771  mulgnnp1  19016  mulgnnsubcl  19020  mulgnn0z  19035  mulgnndir  19037  ghmquskerlem1  19216  ghmquskerco  19217  psgnunilem4  19430  psgnran  19448  sylow1lem1  19531  lsmmod2  19609  lsmdisj2r  19618  efginvrel2  19660  efgsdmi  19665  efgsrel  19667  efgs1b  19669  efgsp1  19670  efgredleme  19676  efgredlemc  19678  efgcpbllemb  19688  frgpuplem  19705  mulgnn0di  19758  frgpnabllem1  19806  lt6abl  19828  cycsubgcyg  19834  gsumval3eu  19837  gsumval3  19840  gsumzcl2  19843  gsumzaddlem  19854  gsumconst  19867  gsumzmhm  19870  gsumzoppg  19877  telgsumfz0s  19924  dprdwd  19946  dprd2da  19977  pgpfaclem1  20016  srgbinom  20170  isirred  20357  idomdomd  20661  idomcringd  20662  lspprid2  20951  lspsnat  21102  lsppratlem1  21104  lsppratlem3  21106  lidl0cl  21177  lidlacl  21178  lidlnegcl  21179  elrspsn  21197  2idllidld  21211  2idlridld  21212  rng2idl1cntr  21262  psgnghm  21537  frlmvscavalb  21727  frlmvplusgscavalb  21728  psrbaglefi  21883  psrass23l  21923  psrass23  21925  mplcoe5lem  21995  mpfind  22071  selvval  22079  mhpvscacl  22098  psr1bascl  22142  ply1basf  22144  gsummoncoe1  22251  lply1binom  22253  lply1binomsc  22254  mpfpf1  22294  pf1mpf  22295  evl1scvarpw  22306  evl1maprhm  22322  matbas2i  22365  matecld  22369  matgsum  22380  mpomatmul  22389  dmatmul  22440  1mavmul  22491  mdetleib2  22531  m1detdiag  22540  marep01ma  22603  smadiadetlem4  22612  slesolinv  22623  pmatcollpw3fi1lem1  22729  chpscmat  22785  chpscmatgsumbin  22787  chp0mat  22789  chpidmat  22790  chfacfisf  22797  chfacfisfcpmat  22798  chfacfpmmulgsum2  22808  cldrcl  22969  ordtbas  23135  iscnp2  23182  dis1stc  23442  ptbasfi  23524  ptpjopn  23555  ptclsg  23558  ptcnp  23565  kqtop  23688  reghmph  23736  ptcmplem2  23996  ptcmplem3  23997  ptcmplem4  23998  tsmslem1  24072  utop2nei  24193  isucn2  24221  cuspcvg  24243  cnextucn  24245  imasdsf1olem  24316  blcvx  24741  xrhmeo  24891  cnrehmeo  24898  evth  24904  reparphti  24942  iscau4  25224  iscmet3lem1  25236  lmle  25246  rrxfsupp  25347  rrxdsfi  25356  pjthlem2  25383  ovollb2lem  25433  ovolunlem1a  25441  ovoliunlem1  25447  ovoliun2  25451  ovolscalem1  25458  ovolicc1  25461  ovolicc2lem4  25465  iundisj2  25494  voliunlem1  25495  volsup  25501  ioombl1lem4  25506  uniioovol  25524  uniioombllem3  25530  uniioombllem4  25531  uniioombllem6  25533  vitalilem5  25557  mbfimaopnlem  25600  mbflimsup  25611  mbfi1fseqlem3  25662  iblitg  25713  dvcnp2  25865  dvnp1  25870  cpncn  25881  dvmulbr  25884  dvcobr  25891  dvlip2  25941  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem3  25976  dvfsumrlimge0  25978  dvfsumrlim2  25980  ftc1cn  25991  elplyd  26148  ply1termlem  26149  ply1term  26150  ply0  26154  plyeq0lem  26156  plyaddlem1  26159  plymullem1  26160  plyaddlem  26161  plymullem  26162  coeeulem  26170  plyco  26187  coeeq2  26188  coefv0  26194  coemulhi  26200  coemulc  26201  plycj  26223  plycjOLD  26225  dvply1  26231  vieta1lem2  26259  elqaalem2  26268  dvtaylp  26318  dvntaylp  26319  taylthlem1  26321  taylth  26324  ulmres  26337  ulmshftlem  26338  ulmshft  26339  ulmcau  26344  ulmdvlem1  26349  mtest  26353  mtestbdd  26354  pserulm  26371  psercn2  26372  psercn2OLD  26373  psercnlem1  26375  psercn  26376  pserdvlem2  26378  abelthlem6  26386  abelth  26391  efif1olem1  26491  efif1olem3  26493  efif1olem4  26494  logcn  26596  advlogexp  26604  efopn  26607  cxpeq  26707  asinsin  26842  atantayl  26887  leibpilem2  26891  birthdaylem2  26902  birthdaylem3  26903  efrlim  26919  efrlimOLD  26920  emcllem2  26947  emcllem5  26950  emcllem7  26952  harmonicbnd4  26961  fsumharmonic  26962  lgamgulm2  26986  lgamcvglem  26990  lgamcvg2  27005  gamcvg2lem  27009  wilthlem2  27019  wilthlem3  27020  ftalem1  27023  ftalem2  27024  ftalem3  27025  ftalem5  27027  basellem2  27032  basellem3  27033  basellem5  27035  basellem8  27038  ppiprm  27101  ppinprm  27102  chtprm  27103  chtnprm  27104  chpp1  27105  vma1  27116  ppiltx  27127  musum  27141  0sgmppw  27149  1sgmprm  27150  ppiublem2  27154  chtublem  27162  fsumvma2  27165  chpchtsum  27170  logexprlim  27176  bposlem5  27239  lgscllem  27255  lgsval2lem  27258  lgsval4a  27270  lgsneg  27272  lgsdir2lem3  27278  lgsdir2lem5  27280  lgsdir  27283  lgsdilem2  27284  lgsdi  27285  lgsne0  27286  gausslemma2dlem3  27319  lgseisenlem1  27326  lgsquadlem2  27332  chebbnd1lem1  27420  chtppilimlem1  27424  rplogsumlem2  27436  rpvmasumlem  27438  dchrisumlem1  27440  dchrisumlem2  27441  dchrmusum2  27445  dchrvmasum2lem  27447  dchrvmasumiflem1  27452  dchrisum0flblem1  27459  dchrisum0flblem2  27460  dchrisum0flb  27461  dchrisum0re  27464  dchrisum0lem1b  27466  dchrisum0lem1  27467  dchrisum0lem2a  27468  dchrisum0lem2  27469  dchrisum0lem3  27470  mudivsum  27481  mulogsum  27483  mulog2sumlem2  27486  selberg2lem  27501  logdivbnd  27507  pntrsumo1  27516  pntrsumbnd2  27518  pntrlog2bndlem2  27529  pntrlog2bndlem4  27531  pntrlog2bndlem6a  27533  pntlemj  27554  pntlemf  27556  ostth2lem3  27586  madebdayim  27868  oldbdayim  27869  newbdayim  27883  cutminmax  27916  noseqp1  28271  tglngne  28606  ltgseg  28652  eedimeq  28955  axlowdimlem16  29014  ebtwntg  29039  subgruhgredgd  29341  subumgredg2  29342  umgrres1lem  29367  wlkson  29712  wksonproplem  29760  trlsonfval  29761  pthsonfval  29797  spthson  29798  crctcshwlkn0lem4  29870  crctcshwlkn0lem5  29871  eupth2lems  30297  numclwwlk1lem2foa  30413  numclwlk1lem2  30429  numclwwlk2lem1  30435  htthlem  30977  hhsscms  31338  shmodsi  31449  pjoc1i  31491  5oalem1  31714  mayete3i  31788  adj1  31993  iundisj2f  32649  fmptco1f1o  32695  fcnvgreu  32734  suppovss  32743  ssnnssfz  32850  nn0diffz0  32857  iundisj2fi  32860  indpreima  32930  ccatws1f1o  33016  cshw1s2  33025  gsumhashmul  33133  gsummulsubdishift1  33134  gsumwrd2dccat  33144  fzo0pmtrlast  33158  wrdpmtrlast  33159  pmtrto1cl  33165  psgnfzto1stlem  33166  fzto1st1  33168  cycpmfv1  33179  cycpmfv2  33180  cycpmco2rn  33191  cycpmco2lem4  33195  cycpmco2lem5  33196  cycpmco2lem6  33197  cyc3evpm  33216  cyc3genpm  33218  cycpmconjslem2  33221  cyc3conja  33223  elrgspnlem1  33308  elrgspnlem2  33309  erler  33331  idomrcanOLD  33348  nsgmgc  33477  nsgqusf1olem2  33479  unitpidl1  33489  elrspunsn  33494  ssdifidllem  33521  mxidlirredi  33536  mxidlirred  33537  opprqusplusg  33554  opprqus0g  33555  opprqusmulr  33556  idlsrgmulrss1  33576  idlsrgmulrss2  33577  rprmcl  33583  rprmdvds  33584  rprmnz  33585  rprmnunit  33586  rprmasso  33590  rprmirredb  33597  pidufd  33608  1arithufdlem2  33610  1arithufdlem3  33611  zringfrac  33619  ply1dg3rt0irred  33649  m1pmeq  33650  ig1pmindeg  33667  extvfvvcl  33684  evlextv  33691  psrmonprod  33701  esplysply  33720  esplyind  33724  esplyfvn  33726  vietalem  33728  exsslsb  33746  ply1degltdimlem  33772  lindsun  33775  fldextfld1  33797  fldextfld2  33798  rtelextdg2  33877  cos9thpiminplylem1  33932  1smat1  33954  submateqlem2  33958  lmatfval  33964  mdetlap1  33976  madjusmdetlem1  33977  madjusmdetlem2  33978  madjusmdetlem3  33979  madjusmdetlem4  33980  zarclssn  34023  zartopn  34025  zarmxt1  34030  rhmpreimacnlem  34034  rhmpreimacn  34035  pnfneige0  34101  pl1cn  34105  rrhqima  34164  esumfzf  34219  esumpcvgval  34228  esumpmono  34229  esumcvg  34236  ldgenpisyslem1  34313  ldgenpisys  34316  measbase  34347  dya2iocnei  34432  oddpwdc  34504  eulerpartlems  34510  eulerpartlemb  34518  sseqf  34542  fibp1  34551  orrvcval4  34615  orrvcoel  34616  orrvccel  34617  ballotlem2  34639  ballotlemfrceq  34679  signsplypnf  34700  signswch  34711  signstf0  34718  signstfvn  34719  signstfvneq0  34722  signstfvcl  34723  signstfveq0  34727  signsvfn  34732  fct2relem  34747  fsum2dsub  34757  reprsuc  34765  reprpmtf1o  34776  breprexplema  34780  breprexplemc  34782  hgt749d  34799  hgt750lemb  34806  tgoldbachgnn  34809  bnj1172  35149  bnj1245  35162  bnj1311  35172  bnj1450  35198  bnj1501  35215  r1elcl  35247  subfacp1lem1  35367  subfacp1lem5  35372  subfacp1lem6  35373  subfacval2  35375  erdszelem7  35385  cvxpconn  35430  cvxsconn  35431  cvmliftlem5  35477  cvmliftlem7  35479  cvmliftlem10  35482  cvmliftlem13  35484  mrsubvrs  35710  msubrn  35717  msubco  35719  msubvrs  35748  r1peuqusdeg1  35831  imageval  36116  fwddifnp1  36353  knoppcnlem8  36758  knoppcnlem10  36760  bj-unirel  37356  icoreunrn  37671  istoprelowl  37672  poimirlem3  37935  poimirlem4  37936  poimirlem6  37938  poimirlem7  37939  poimirlem8  37940  poimirlem12  37944  poimirlem15  37947  poimirlem16  37948  poimirlem17  37949  poimirlem18  37950  poimirlem19  37951  poimirlem20  37952  poimirlem21  37953  poimirlem22  37954  poimirlem23  37955  poimirlem24  37956  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  poimirlem28  37960  poimirlem29  37961  poimirlem31  37963  mblfinlem2  37970  ftc1cnnc  38004  upixp  38041  sdclem2  38054  caushft  38073  ismtyres  38120  rrnmet  38141  rrndstprj1  38142  rrndstprj2  38143  rrncmslem  38144  rrnequiv  38147  iccbnd  38152  osumcllem7N  40399  pexmidlem4N  40410  lcfrlem4  41982  lcfrlem5  41983  lcfrlem6  41984  lcfrlem16  41995  lcfrlem38  42017  mapdrvallem2  42082  mapdh8ab  42214  mapdh8ad  42216  mapdh8e  42221  3factsumint3  42454  aks4d1p1p1  42494  fldhmf1  42521  aks6d1c1p2  42540  aks6d1c1p3  42541  aks6d1c1p7  42544  aks6d1c1p6  42545  aks6d1c1p8  42546  aks6d1c1  42547  evl1gprodd  42548  idomnnzpownz  42563  aks6d1c5lem1  42567  aks6d1c5lem3  42568  aks6d1c5lem2  42569  deg1gprod  42571  sticksstones10  42586  aks6d1c6lem3  42603  aks5lem2  42618  aks5lem3a  42620  unitscyglem5  42630  fz1sump1  42741  sumcubes  42744  evlselv  43019  mhphf2  43030  prjspnfv01  43056  prjspner01  43057  prjspner1  43058  mapfzcons  43147  diophren  43244  irrapxlem1  43253  monotuz  43372  acongeq  43414  jm2.26lem3  43432  jm3.1lem2  43449  pw2f1ocnv  43468  idomodle  43622  trclfvdecomr  44158  imo72b2lem0  44595  imo72b2lem1  44599  scottelrankd  44677  dvgrat  44742  cvgdvgrat  44743  hashnzfz2  44751  fcnre  45459  refsumcn  45464  rfcnnnub  45470  disjf1o  45624  disjinfi  45625  ssmapsn  45648  ssuzfz  45782  nnsplit  45791  uzssd2  45849  uzublem  45862  fsumsermpt  46013  climsuselem1  46041  limcperiod  46062  sumnnodd  46064  lptioo2cn  46077  lptioo1cn  46078  climresmpt  46091  allbutfifvre  46107  climleltrp  46108  cnrefiisplem  46261  cncfshift  46306  cncfperiod  46311  cncfshiftioo  46324  fperdvper  46351  dvnmptdivc  46370  dvnmul  46375  dvmptfprod  46377  dvnprodlem3  46380  stoweidlem11  46443  stoweidlem15  46447  stoweidlem17  46449  stoweidlem20  46452  stoweidlem34  46466  stoweidlem35  46467  stoweidlem46  46478  stoweidlem47  46479  stoweidlem56  46488  stoweidlem59  46491  stoweidlem62  46494  stirlinglem5  46510  stirlinglem14  46519  dirkertrigeqlem2  46531  dirkertrigeqlem3  46532  fourierdlem11  46550  fourierdlem15  46554  fourierdlem16  46555  fourierdlem21  46560  fourierdlem22  46561  fourierdlem25  46564  fourierdlem48  46586  fourierdlem52  46590  fourierdlem54  46592  fourierdlem58  46596  fourierdlem62  46600  fourierdlem64  46602  fourierdlem65  46603  fourierdlem69  46607  fourierdlem70  46608  fourierdlem71  46609  fourierdlem73  46611  fourierdlem80  46618  fourierdlem81  46619  fourierdlem83  46621  fourierdlem92  46630  fourierdlem93  46631  fourierdlem97  46635  fourierdlem103  46641  fourierdlem104  46642  fourierdlem112  46650  fourierdlem113  46651  fouriercnp  46658  fouriersw  46663  elaa2lem  46665  etransclem4  46670  etransclem7  46673  etransclem10  46676  etransclem14  46680  etransclem15  46681  etransclem24  46690  etransclem25  46691  etransclem31  46697  etransclem32  46698  etransclem35  46701  etransclem44  46710  etransclem46  46712  qndenserrnopnlem  46729  qndenserrn  46731  prsal  46750  salgencntex  46775  subsaliuncl  46790  subsalsal  46791  sge0tsms  46812  sge0fodjrnlem  46848  sge0isum  46859  iundjiunlem  46891  iundjiun  46892  meadjiunlem  46897  meaiunlelem  46900  meaiuninclem  46912  meaiininc2  46920  caragensplit  46932  carageneld  46934  carageniuncllem1  46953  caratheodorylem1  46958  caratheodorylem2  46959  hoicvr  46980  hsphoidmvle2  47017  hsphoidmvle  47018  hoidmv1lelem2  47024  hoidmv1lelem3  47025  hoidmvlelem2  47028  hoiqssbllem2  47055  pimdecfgtioc  47147  pimincfltioc  47148  pimdecfgtioo  47149  pimincfltioo  47150  smflimlem3  47205  smfmullem4  47226  smfsupxr  47248  smflimsuplem2  47253  smflimsuplem5  47256  ormklocald  47306  natlocalincr  47308  elmod2  47789  isuspgrim0lem  48327  upgrimtrlslem2  48339  ssnn0ssfz  48783  zlmodzxzscm  48791  rmsupp0  48802  lincsum  48863  lincscm  48864  lindslinindimp2lem4  48895  lincresunit3  48915  elbigofrcl  48984  intubeu  49417  unilbeu  49418  cicrcl2  49476  cic1st2nd  49480  imaf1homlem  49540  oppfrcl  49561  eloppf  49566  imasubc  49584  imaid  49587  oppcuprcl5  49634  oppcup3  49642  uptrlem2  49644  uptrlem3  49645  natoppf  49662  elxpcbasex1ALT  49682  elxpcbasex2ALT  49684  swapf1a  49702  swapf2f1oa  49710  swapfida  49713  cofuswapf1  49727  cofuswapf2  49728  fucoppcco  49842  postc  50002  reldmlan2  50050  reldmran2  50051  lanrcl  50054  ranrcl  50055  setrec1  50124  aacllem  50234