Theorem eleqtrdi 2871

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  eleqtrrdi  2872  3eltr3g  2877  prid2g  4722  ndmfvrcl  6918  fnwelem  8143  tz7.48-1  8453  brwitnlem  8515  oeeulem  8610  dffi3  9423  cnfcom3lem  9704  ttrclse  9728  rankwflemb  9800  scottelrankd  9948  setrec1  9972  alephgeom  10161  fpwwe2lem5  10720  canthwelem  10735  hargch  10758  r1wunlim  10822  eluzel2  12970  fseq1p1m1  13732  fznn0sub2  13769  nn0split  13777  seqp1d  14161  exple1  14320  digit1  14381  bcval5  14462  bcpasc  14465  hashf1  14602  seqcoll  14609  seqcoll2  14610  ccatrn  14735  swrdccat2  14819  cats1un  14870  pfxccatin12lem3  14881  splfv2a  14905  splval2  14906  caubnd  15526  limsupgre  15648  clim2ser  15822  clim2ser2  15823  iserex  15824  isermulc2  15825  iserle  15827  iserge0  15828  climub  15829  climserle  15830  isercolllem2  15833  isercolllem3  15834  isercoll  15835  isercoll2  15836  serf0  15848  iseraltlem2  15850  iseraltlem3  15851  iseralt  15852  sumeq2ii  15860  summolem3  15880  summolem2a  15881  fsum  15886  sum0  15887  fsumcl2lem  15897  fsumadd  15906  isumclim3  15925  isumadd  15933  fsump1i  15935  fsummulc2  15950  fsumrelem  15974  iserabs  15982  cvgcmp  15983  cvgcmpub  15984  cvgcmpce  15985  binom1dif  16002  isumshft  16008  isumsplit  16009  isumrpcl  16012  isumsup2  16015  climcndslem1  16018  climcndslem2  16019  climcnds  16020  arisum2  16030  trireciplem  16031  geoser  16036  pwdif  16037  geolim  16039  geo2lim  16044  cvgrat  16052  mertenslem1  16053  mertenslem2  16054  mertens  16055  clim2prod  16057  clim2div  16058  ntrivcvgfvn0  16068  ntrivcvgtail  16069  prodeq2ii  16080  prodmolem3  16100  prodmolem2a  16101  fprod  16108  fprodntriv  16109  fprodss  16115  fprodser  16116  fprodcl2lem  16117  fprodmul  16127  fproddiv  16128  fprodabs  16141  fprodeq0  16142  fprodn0  16146  iprodclim3  16167  iprodmul  16170  fallfacfwd  16202  0fallfac  16203  binomfallfaclem2  16206  fallfacval4  16209  bpolysum  16219  bpolydiflem  16220  fsumkthpow  16222  efcvgfsum  16252  efcj  16258  fprodefsum  16261  effsumlt  16279  ruclem7  16404  bitsfzolem  16604  bitsfzo  16605  bitsfi  16607  bitsinv1lem  16611  bitsinv1  16612  bitsinvp1  16619  sadcp1  16625  sadadd  16637  sadass  16641  bitsres  16643  smupp1  16650  smuval2  16652  smupval  16658  smueqlem  16660  smumul  16663  algrp1  16749  phiprmpw  16953  crth  16955  phimullem  16956  eulerthlem2  16959  prmdiv  16962  pcpremul  17021  pcmpt  17070  pcfac  17077  pockthlem  17083  pockthg  17084  prmreclem2  17095  prmreclem3  17096  prmreclem4  17097  prmreclem5  17098  prmreclem6  17099  prmrec  17100  1arith  17105  vdwapun  17152  vdwlem1  17159  vdwlem2  17160  vdwlem3  17161  vdwlem6  17164  vdwlem8  17166  vdwlem10  17168  vdw  17172  imasvscafn  17709  oppccatid  17893  oppccomfpropd  17901  brcic  17973  funcoppc  18050  invfuc  18152  hofcl  18433  yonedalem4c  18451  chnccats1  18799  gsumwsubmcl  19033  gsumsgrpccat  19036  gsumwmhm  19041  mulgnnp1  19292  mulgnnsubcl  19296  mulgnn0z  19311  mulgnndir  19313  ghmquskerlem1  19497  ghmquskerco  19498  psgnunilem4  19711  psgnran  19729  sylow1lem1  19812  lsmmod2  19890  lsmdisj2r  19899  efginvrel2  19941  efgsdmi  19946  efgsrel  19948  efgs1b  19950  efgsp1  19951  efgredleme  19957  efgredlemc  19959  efgcpbllemb  19969  frgpuplem  19986  mulgnn0di  20039  frgpnabllem1  20087  lt6abl  20109  cycsubgcyg  20115  gsumval3eu  20118  gsumval3  20121  gsumzcl2  20124  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  telgsumfz0s  20205  dprdwd  20227  dprd2da  20258  pgpfaclem1  20297  srgbinom  20457  isirred  20649  idomdomd  20977  idomcringd  20978  lspprid2  21273  lspsnat  21423  lsppratlem1  21425  lsppratlem3  21427  lidl0cl  21499  lidlacl  21500  lidlnegcl  21501  elrspsn  21525  2idllidld  21547  2idlridld  21548  rng2idl1cntr  21601  ssdifidllem  21640  psgnghm  21886  frlmvscavalb  22076  frlmvplusgscavalb  22077  psrbaglefi  22234  psrass23l  22274  psrass23  22276  mplcoe5lem  22348  mpfind  22424  selvval  22429  mhpvscacl  22475  psr1bascl  22518  ply1basf  22520  gsummoncoe1  22626  lply1binom  22628  lply1binomsc  22629  mpfpf1  22669  pf1mpf  22670  evl1scvarpw  22681  evl1maprhm  22697  matbas2i  22737  matecld  22741  matgsum  22752  mpomatmul  22761  dmatmul  22812  1mavmul  22863  mdetleib2  22903  m1detdiag  22912  marep01ma  22975  smadiadetlem4  22984  slesolinv  22998  pmatcollpw3fi1lem1  23104  chpscmat  23160  chpscmatgsumbin  23162  chp0mat  23164  chpidmat  23165  chfacfisf  23172  chfacfisfcpmat  23173  chfacfpmmulgsum2  23183  cldrcl  23344  ordtbas  23510  iscnp2  23557  dis1stc  23818  ptbasfi  23900  ptpjopn  23931  ptclsg  23934  ptcnp  23941  kqtop  24064  reghmph  24112  ptcmplem2  24372  ptcmplem3  24373  ptcmplem4  24374  tsmslem1  24448  utop2nei  24569  isucn2  24597  cuspcvg  24619  cnextucn  24621  imasdsf1olem  24692  blcvx  25117  xrhmeo  25267  cnrehmeo  25274  evth  25280  reparphti  25318  iscau4  25600  iscmet3lem1  25612  lmle  25622  rrxfsupp  25723  rrxdsfi  25732  pjthlem2  25759  ovollb2lem  25809  ovolunlem1a  25817  ovoliunlem1  25823  ovoliun2  25827  ovolscalem1  25834  ovolicc1  25837  ovolicc2lem4  25841  iundisj2  25870  voliunlem1  25871  volsup  25877  ioombl1lem4  25882  uniioovol  25900  uniioombllem3  25906  uniioombllem4  25907  uniioombllem6  25909  vitalilem5  25933  mbfimaopnlem  25976  mbflimsup  25987  mbfi1fseqlem3  26038  iblitg  26089  dvcnp2  26240  dvnp1  26245  cpncn  26256  dvmulbr  26259  dvcobr  26266  dvlip2  26315  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumrlimge0  26350  dvfsumrlim2  26352  ftc1cn  26363  elplyd  26520  ply1termlem  26521  ply1term  26522  ply0  26526  plyeq0lem  26529  plyaddlem1  26532  plymullem1  26533  plyaddlem  26534  plymullem  26535  coeeulem  26543  plyco  26560  coeeq2  26561  coefv0  26567  coemulhi  26573  coemulc  26574  plycj  26596  dvply1  26605  vieta1lem2  26634  elqaalem2  26643  dvtaylp  26697  dvntaylp  26698  taylthlem1  26700  taylth  26702  ulmres  26715  ulmshftlem  26716  ulmshft  26717  ulmcau  26722  ulmdvlem1  26727  mtest  26731  mtestbdd  26732  pserulm  26749  psercn2  26750  psercnlem1  26752  psercn  26753  pserdvlem2  26755  abelthlem6  26763  abelth  26768  efif1olem1  26870  efif1olem3  26872  efif1olem4  26873  logcn  26975  advlogexp  26983  efopn  26986  cxpeq  27085  asinsin  27220  atantayl  27265  leibpilem2  27269  birthdaylem2  27280  birthdaylem3  27281  efrlim  27297  emcllem2  27324  emcllem5  27327  emcllem7  27329  harmonicbnd4  27338  fsumharmonic  27339  lgamgulm2  27363  lgamcvglem  27367  lgamcvg2  27382  gamcvg2lem  27386  wilthlem2  27396  wilthlem3  27397  ftalem1  27400  ftalem2  27401  ftalem3  27402  ftalem5  27404  basellem2  27409  basellem3  27410  basellem5  27412  basellem8  27415  ppiprm  27478  ppinprm  27479  chtprm  27480  chtnprm  27481  chpp1  27482  vma1  27493  ppiltx  27504  musum  27518  0sgmppw  27525  1sgmprm  27526  ppiublem2  27530  chtublem  27538  fsumvma2  27541  chpchtsum  27546  logexprlim  27552  bposlem5  27615  lgscllem  27631  lgsval2lem  27634  lgsval4a  27646  lgsneg  27648  lgsdir2lem3  27654  lgsdir2lem5  27656  lgsdir  27659  lgsdilem2  27660  lgsdi  27661  lgsne0  27662  gausslemma2dlem3  27695  lgseisenlem1  27702  lgsquadlem2  27708  chebbnd1lem1  27796  chtppilimlem1  27800  rplogsumlem2  27812  rpvmasumlem  27814  dchrisumlem1  27816  dchrisumlem2  27817  dchrmusum2  27821  dchrvmasum2lem  27823  dchrvmasumiflem1  27828  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0flb  27837  dchrisum0re  27840  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem2  27845  dchrisum0lem3  27846  mudivsum  27857  mulogsum  27859  mulog2sumlem2  27862  selberg2lem  27877  logdivbnd  27883  pntrsumo1  27892  pntrsumbnd2  27894  pntrlog2bndlem2  27905  pntrlog2bndlem4  27907  pntrlog2bndlem6a  27909  pntlemj  27930  pntlemf  27932  ostth2lem3  27962  madebdayim  28274  oldbdayim  28275  newbdayim  28289  cutminmax  28322  noseqp1  28677  tglngne  29013  ltgseg  29059  eedimeq  29476  axlowdimlem16  29535  ebtwntg  29560  subgruhgredgd  29865  subumgredg2  29866  umgrres1lem  29891  wlkson  30235  wksonproplem  30287  trlsonfval  30288  pthsonfval  30326  spthson  30327  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  eupth2lems  30839  numclwwlk1lem2foa  30955  numclwlk1lem2  30971  numclwwlk2lem1  30977  htthlem  31519  hhsscms  31880  shmodsi  31991  pjoc1i  32033  5oalem1  32256  mayete3i  32330  adj1  32535  iundisj2f  33184  fmptco1f1o  33227  fcnvgreu  33266  suppovss  33274  ssnnssfz  33379  nn0diffz0  33386  iundisj2fi  33389  indpreima  33432  ccatws1f1o  33514  cshw1s2  33521  gsumhashmul  33628  gsummulsubdishift1  33629  gsumwrd2dccat  33639  fzo0pmtrlast  33653  wrdpmtrlast  33654  pmtrto1cl  33660  psgnfzto1stlem  33661  fzto1st1  33663  cycpmfv1  33674  cycpmfv2  33675  cycpmco2rn  33686  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cyc3evpm  33711  cyc3genpm  33713  cycpmconjslem2  33716  cyc3conja  33718  elrgspnlem1  33803  elrgspnlem2  33804  erler  33826  nsgmgc  33963  nsgqusf1olem2  33965  unitpidl1  33974  elrspunsn  33979  mxidlirredi  33996  mxidlirred  33997  opprqusplusg  34013  opprqus0g  34014  opprqusmulr  34015  idlsrgmulrss1  34043  idlsrgmulrss2  34044  rprmcl  34050  rprmdvds  34051  rprmnz  34052  rprmnunit  34053  rprmasso  34057  rprmirredb  34064  pidufd  34075  1arithufdlem2  34077  1arithufdlem3  34078  zringfrac  34086  ply1dg3rt0irred  34116  m1pmeq  34117  ig1pmindeg  34134  selvply1rhmlem2  34153  selvply1rhmlem4  34155  selvply1rhm0  34158  extvfvvcl  34167  evlextv  34174  psrmonprod  34184  esplysply  34203  esplyind  34207  esplyfvn  34209  vietalem  34211  exsslsb  34229  ply1degltdimlem  34254  lindsun  34257  fldextfld1  34279  fldextfld2  34280  rtelextdg2  34359  cos9thpiminplylem1  34414  1smat1  34436  submateqlem2  34440  lmatfval  34446  mdetlap1  34458  madjusmdetlem1  34459  madjusmdetlem2  34460  madjusmdetlem3  34461  madjusmdetlem4  34462  zarclssn  34505  zartopn  34507  zarmxt1  34512  rhmpreimacnlem  34516  rhmpreimacn  34517  pnfneige0  34583  pl1cn  34587  rrhqima  34646  esumfzf  34701  esumpcvgval  34710  esumpmono  34711  esumcvg  34718  ldgenpisyslem1  34796  ldgenpisys  34799  measbase  34830  dya2iocnei  34914  oddpwdc  34986  eulerpartlems  34992  eulerpartlemb  35000  sseqf  35024  fibp1  35033  orrvcval4  35097  orrvcoel  35098  orrvccel  35099  ballotlem2  35121  ballotlemfrceq  35161  signsplypnf  35179  signswch  35190  signstf0  35197  signstfvn  35198  signstfvneq0  35201  signstfvcl  35202  signstfveq0  35206  signsvfn  35211  fct2relem  35226  fsum2dsub  35236  reprsuc  35244  reprpmtf1o  35255  breprexplema  35259  breprexplemc  35261  hgt749d  35278  hgt750lemb  35285  tgoldbachgnn  35288  bnj1172  35631  bnj1245  35644  bnj1311  35654  bnj1450  35680  bnj1501  35697  subfacp1lem1  35944  subfacp1lem5  35949  subfacp1lem6  35950  subfacval2  35952  erdszelem7  35962  cvxpconn  36007  cvxsconn  36008  cvmliftlem5  36054  cvmliftlem7  36056  cvmliftlem10  36059  cvmliftlem13  36061  mrsubvrs  36287  msubrn  36294  msubco  36296  msubvrs  36325  r1peuqusdeg1  36408  imageval  36692  fwddifnp1  36930  knoppcnlem8  37366  knoppcnlem10  37368  bj-unirel  37966  icoreunrn  38282  istoprelowl  38283  poimirlem3  38541  poimirlem4  38542  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem12  38550  poimirlem15  38553  poimirlem16  38554  poimirlem17  38555  poimirlem18  38556  poimirlem19  38557  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem23  38561  poimirlem24  38562  poimirlem25  38563  poimirlem26  38564  poimirlem27  38565  poimirlem28  38566  poimirlem29  38567  poimirlem31  38569  mblfinlem2  38576  ftc1cnnc  38610  upixp  38663  sdclem2  38676  caushft  38695  ismtyres  38742  rrnmet  38763  rrndstprj1  38764  rrndstprj2  38765  rrncmslem  38766  rrnequiv  38769  iccbnd  38774  osumcllem7N  41019  pexmidlem4N  41030  lcfrlem4  42602  lcfrlem5  42603  lcfrlem6  42604  lcfrlem16  42615  lcfrlem38  42637  mapdrvallem2  42702  mapdh8ab  42834  mapdh8ad  42836  mapdh8e  42841  3factsumint3  43073  aks4d1p1p1  43113  fldhmf1  43140  aks6d1c1p2  43159  aks6d1c1p3  43160  aks6d1c1p7  43163  aks6d1c1p6  43164  aks6d1c1p8  43165  aks6d1c1  43166  evl1gprodd  43167  idomnnzpownz  43182  aks6d1c5lem1  43186  aks6d1c5lem3  43187  aks6d1c5lem2  43188  deg1gprod  43190  sticksstones10  43205  aks6d1c6lem3  43222  aks5lem2  43237  aks5lem3a  43239  unitscyglem5  43249  fz1sump1  43367  sumcubes  43370  evlselv  43617  mhphf2  43626  frlmnzcoordex  43652  frlmnzcoordsca  43658  prjspnnorm  43661  mapfzcons  43726  diophren  43819  irrapxlem1  43828  monotuz  43947  acongeq  43989  jm2.26lem3  44007  jm3.1lem2  44024  pw2f1ocnv  44043  idomodle  44192  trclfvdecomr  44727  imo72b2lem0  45164  imo72b2lem1  45168  dvgrat  45295  cvgdvgrat  45296  hashnzfz2  45304  fcnre  46041  refsumcn  46046  rfcnnnub  46052  disjf1o  46205  disjinfi  46206  ssmapsn  46228  ssuzfz  46360  nnsplit  46369  uzssd2  46426  uzublem  46439  fsumsermpt  46590  climsuselem1  46618  limcperiod  46639  sumnnodd  46641  lptioo2cn  46654  lptioo1cn  46655  climresmpt  46668  allbutfifvre  46684  climleltrp  46685  cnrefiisplem  46838  cncfshift  46883  cncfperiod  46888  cncfshiftioo  46901  fperdvper  46928  dvnmptdivc  46947  dvnmul  46952  dvmptfprod  46954  dvnprodlem3  46957  stoweidlem11  47020  stoweidlem15  47024  stoweidlem17  47026  stoweidlem20  47029  stoweidlem34  47043  stoweidlem35  47044  stoweidlem46  47055  stoweidlem47  47056  stoweidlem56  47065  stoweidlem59  47068  stoweidlem62  47071  stirlinglem5  47087  stirlinglem14  47096  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  fourierdlem11  47127  fourierdlem15  47131  fourierdlem16  47132  fourierdlem21  47137  fourierdlem22  47138  fourierdlem25  47141  fourierdlem48  47163  fourierdlem49  47164  fourierdlem52  47167  fourierdlem54  47169  fourierdlem58  47173  fourierdlem62  47177  fourierdlem64  47179  fourierdlem65  47180  fourierdlem69  47184  fourierdlem70  47185  fourierdlem71  47186  fourierdlem73  47188  fourierdlem80  47195  fourierdlem81  47196  fourierdlem83  47198  fourierdlem92  47207  fourierdlem93  47208  fourierdlem97  47212  fourierdlem103  47218  fourierdlem104  47219  fourierdlem112  47227  fourierdlem113  47228  fouriercnp  47235  fouriersw  47240  elaa2lem  47242  etransclem4  47247  etransclem7  47250  etransclem10  47253  etransclem14  47257  etransclem15  47258  etransclem24  47267  etransclem25  47268  etransclem31  47274  etransclem32  47275  etransclem35  47278  etransclem44  47287  etransclem46  47289  qndenserrnopnlem  47306  qndenserrn  47308  prsal  47327  salgencntex  47352  subsaliuncl  47367  subsalsal  47368  sge0tsms  47389  sge0fodjrnlem  47425  sge0isum  47436  iundjiunlem  47468  iundjiun  47469  meadjiunlem  47474  meaiunlelem  47477  meaiuninclem  47489  meaiininc2  47497  caragensplit  47509  carageneld  47511  carageniuncllem1  47530  caratheodorylem1  47535  caratheodorylem2  47536  hoicvr  47557  hsphoidmvle2  47594  hsphoidmvle  47595  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmvlelem2  47605  hoiqssbllem2  47632  pimdecfgtioc  47724  pimincfltioc  47725  pimdecfgtioo  47726  pimincfltioo  47727  smflimlem3  47782  smfmullem4  47803  smfsupxr  47825  smflimsuplem2  47830  smflimsuplem5  47833  ormklocald  47885  chnerlem1  47891  elmod2  48430  isuspgrim0lem  48990  upgrimtrlslem2  49002  ssnn0ssfz  49460  zlmodzxzscm  49468  rmsupp0  49479  lincsum  49540  lincscm  49541  lindslinindimp2lem4  49572  lincresunit3  49592  elbigofrcl  49661  intubeu  50091  unilbeu  50092  cicrcl2  50150  cic1st2nd  50154  imaf1homlem  50214  oppfrcl  50235  eloppf  50240  imasubc  50258  imaid  50261  oppcuprcl5  50308  oppcup3  50316  uptrlem2  50318  uptrlem3  50319  natoppf  50336  elxpcbasex1ALT  50356  elxpcbasex2ALT  50358  swapf1a  50376  swapf2f1oa  50384  swapfida  50387  cofuswapf1  50401  cofuswapf2  50402  fucoppcco  50516  postc  50676  reldmlan2  50724  reldmran2  50725  lanrcl  50728  ranrcl  50729  aacllem  50938  crosspaltd  50965  crossp3d  50966  veronesematbasd  50979  veroquaddetzerod  50985