Theorem eleqtrdi 2874

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2839

This theorem is used by:  eleqtrrdi  2875  3eltr3g  2880  prid2g  4722  ndmfvrcl  6929  fnwelem  8156  tz7.48-1  8467  brwitnlem  8529  oeeulem  8624  dffi3  9436  cnfcom3lem  9717  ttrclse  9741  rankwflemb  9813  scottelrankd  9961  setrec1  9985  alephgeom  10174  fpwwe2lem5  10733  canthwelem  10748  hargch  10771  r1wunlim  10835  eluzel2  12983  fseq1p1m1  13745  fznn0sub2  13782  nn0split  13790  seqp1d  14174  exple1  14333  digit1  14394  bcval5  14475  bcpasc  14478  hashf1  14615  seqcoll  14622  seqcoll2  14623  ccatrn  14748  s1mapd  14769  swrdccat2  14833  cats1un  14884  pfxccatin12lem3  14895  splfv2a  14919  splval2  14920  caubnd  15541  limsupgre  15663  clim2ser  15837  clim2ser2  15838  iserex  15839  isermulc2  15840  iserle  15842  iserge0  15843  climub  15844  climserle  15845  isercolllem2  15848  isercolllem3  15849  isercoll  15850  isercoll2  15851  serf0  15863  iseraltlem2  15865  iseraltlem3  15866  iseralt  15867  sumeq2ii  15875  summolem3  15895  summolem2a  15896  fsum  15901  sum0  15902  fsumcl2lem  15912  fsumadd  15921  isumclim3  15940  isumadd  15948  fsump1i  15950  fsummulc2  15965  fsumrelem  15989  iserabs  15997  cvgcmp  15998  cvgcmpub  15999  cvgcmpce  16000  binom1dif  16017  isumshft  16023  isumsplit  16024  isumrpcl  16027  isumsup2  16030  climcndslem1  16033  climcndslem2  16034  climcnds  16035  arisum2  16045  trireciplem  16046  geoser  16051  pwdif  16052  geolim  16054  geo2lim  16059  cvgrat  16067  mertenslem1  16068  mertenslem2  16069  mertens  16070  clim2prod  16072  clim2div  16073  ntrivcvgfvn0  16083  ntrivcvgtail  16084  prodeq2ii  16095  prodmolem3  16115  prodmolem2a  16116  fprod  16123  fprodntriv  16124  fprodss  16130  fprodser  16131  fprodcl2lem  16132  fprodmul  16142  fproddiv  16143  fprodabs  16156  fprodeq0  16157  fprodn0  16161  iprodclim3  16182  iprodmul  16185  fallfacfwd  16217  0fallfac  16218  binomfallfaclem2  16221  fallfacval4  16224  bpolysum  16234  bpolydiflem  16235  fsumkthpow  16237  efcvgfsum  16267  efcj  16273  fprodefsum  16276  effsumlt  16294  ruclem7  16419  bitsfzolem  16619  bitsfzo  16620  bitsfi  16622  bitsinv1lem  16626  bitsinv1  16627  bitsinvp1  16634  sadcp1  16640  sadadd  16652  sadass  16656  bitsres  16658  smupp1  16665  smuval2  16667  smupval  16673  smueqlem  16675  smumul  16678  algrp1  16764  phiprmpw  16968  crth  16970  phimullem  16971  eulerthlem2  16974  prmdiv  16977  pcpremul  17036  pcmpt  17085  pcfac  17092  pockthlem  17098  pockthg  17099  prmreclem2  17110  prmreclem3  17111  prmreclem4  17112  prmreclem5  17113  prmreclem6  17114  prmrec  17115  1arith  17120  vdwapun  17167  vdwlem1  17174  vdwlem2  17175  vdwlem3  17176  vdwlem6  17179  vdwlem8  17181  vdwlem10  17183  vdw  17187  imasvscafn  17724  oppccatid  17908  oppccomfpropd  17916  brcic  17988  funcoppc  18065  invfuc  18167  hofcl  18448  yonedalem4c  18466  chnccats1  18814  gsumwsubmcl  19048  gsumsgrpccat  19051  gsumwmhm  19056  mulgnnp1  19307  mulgnnsubcl  19311  mulgnn0z  19326  mulgnndir  19328  ghmquskerlem1  19512  ghmquskerco  19513  psgnunilem4  19726  psgnran  19744  sylow1lem1  19827  lsmmod2  19905  lsmdisj2r  19914  efginvrel2  19956  efgsdmi  19961  efgsrel  19963  efgs1b  19965  efgsp1  19966  efgredleme  19972  efgredlemc  19974  efgcpbllemb  19984  frgpuplem  20001  mulgnn0di  20054  frgpnabllem1  20102  lt6abl  20124  cycsubgcyg  20130  gsumval3eu  20133  gsumval3  20136  gsumzcl2  20139  gsumzaddlem  20150  gsumconst  20163  gsumzmhm  20166  gsumzoppg  20173  telgsumfz0s  20220  dprdwd  20242  dprd2da  20273  pgpfaclem1  20312  srgbinom  20472  isirred  20664  idomdomd  20992  idomcringd  20993  lspprid2  21288  lspsnat  21438  lsppratlem1  21440  lsppratlem3  21442  lidl0cl  21514  lidlacl  21515  lidlnegcl  21516  elrspsn  21540  2idllidld  21562  2idlridld  21563  rng2idl1cntr  21616  ssdifidllem  21655  psgnghm  21901  frlmvscavalb  22091  frlmvplusgscavalb  22092  psrbaglefi  22249  psrass23l  22289  psrass23  22291  mplcoe5lem  22363  mpfind  22439  selvval  22444  mhpvscacl  22490  psr1bascl  22533  ply1basf  22535  gsummoncoe1  22641  lply1binom  22643  lply1binomsc  22644  mpfpf1  22684  pf1mpf  22685  evl1scvarpw  22696  evl1maprhm  22712  matbas2i  22752  matecld  22756  matgsum  22767  mpomatmul  22776  dmatmul  22827  1mavmul  22878  mdetleib2  22918  m1detdiag  22927  marep01ma  22990  smadiadetlem4  22999  slesolinv  23013  pmatcollpw3fi1lem1  23119  chpscmat  23175  chpscmatgsumbin  23177  chp0mat  23179  chpidmat  23180  chfacfisf  23187  chfacfisfcpmat  23188  chfacfpmmulgsum2  23198  cldrcl  23359  ordtbas  23525  iscnp2  23572  dis1stc  23833  ptbasfi  23915  ptpjopn  23946  ptclsg  23949  ptcnp  23956  kqtop  24079  reghmph  24127  ptcmplem2  24387  ptcmplem3  24388  ptcmplem4  24389  tsmslem1  24463  utop2nei  24584  isucn2  24612  cuspcvg  24634  cnextucn  24636  imasdsf1olem  24707  blcvx  25132  xrhmeo  25282  cnrehmeo  25289  evth  25295  reparphti  25333  iscau4  25615  iscmet3lem1  25627  lmle  25637  rrxfsupp  25738  rrxdsfi  25747  pjthlem2  25774  ovollb2lem  25824  ovolunlem1a  25832  ovoliunlem1  25838  ovoliun2  25842  ovolscalem1  25849  ovolicc1  25852  ovolicc2lem4  25856  iundisj2  25885  voliunlem1  25886  volsup  25892  ioombl1lem4  25897  uniioovol  25915  uniioombllem3  25921  uniioombllem4  25922  uniioombllem6  25924  vitalilem5  25948  mbfimaopnlem  25991  mbflimsup  26002  mbfi1fseqlem3  26053  iblitg  26104  dvcnp2  26255  dvnp1  26260  cpncn  26271  dvmulbr  26274  dvcobr  26281  dvlip2  26330  dvfsumlem2  26362  dvfsumlem3  26363  dvfsumrlimge0  26365  dvfsumrlim2  26367  ftc1cn  26378  elplyd  26535  ply1termlem  26536  ply1term  26537  ply0  26541  plyeq0lem  26544  plyaddlem1  26547  plymullem1  26548  plyaddlem  26549  plymullem  26550  coeeulem  26558  plyco  26575  coeeq2  26576  coefv0  26582  coemulhi  26588  coemulc  26589  plycj  26611  dvply1  26620  vieta1lem2  26649  elqaalem2  26658  dvtaylp  26712  dvntaylp  26713  taylthlem1  26715  taylth  26717  ulmres  26730  ulmshftlem  26731  ulmshft  26732  ulmcau  26737  ulmdvlem1  26742  mtest  26746  mtestbdd  26747  pserulm  26764  psercn2  26765  psercnlem1  26767  psercn  26768  pserdvlem2  26770  abelthlem6  26778  abelth  26783  efif1olem1  26885  efif1olem3  26887  efif1olem4  26888  logcn  26990  advlogexp  26998  efopn  27001  cxpeq  27100  asinsin  27235  atantayl  27280  leibpilem2  27284  birthdaylem2  27295  birthdaylem3  27296  efrlim  27312  emcllem2  27339  emcllem5  27342  emcllem7  27344  harmonicbnd4  27353  fsumharmonic  27354  lgamgulm2  27378  lgamcvglem  27382  lgamcvg2  27397  gamcvg2lem  27401  wilthlem2  27411  wilthlem3  27412  ftalem1  27415  ftalem2  27416  ftalem3  27417  ftalem5  27419  basellem2  27424  basellem3  27425  basellem5  27427  basellem8  27430  ppiprm  27493  ppinprm  27494  chtprm  27495  chtnprm  27496  chpp1  27497  vma1  27508  ppiltx  27519  musum  27533  0sgmppw  27540  1sgmprm  27541  ppiublem2  27545  chtublem  27553  fsumvma2  27556  chpchtsum  27561  logexprlim  27567  bposlem5  27630  lgscllem  27646  lgsval2lem  27649  lgsval4a  27661  lgsneg  27663  lgsdir2lem3  27669  lgsdir2lem5  27671  lgsdir  27674  lgsdilem2  27675  lgsdi  27676  lgsne0  27677  gausslemma2dlem3  27710  lgseisenlem1  27717  lgsquadlem2  27723  chebbnd1lem1  27811  chtppilimlem1  27815  rplogsumlem2  27827  rpvmasumlem  27829  dchrisumlem1  27831  dchrisumlem2  27832  dchrmusum2  27836  dchrvmasum2lem  27838  dchrvmasumiflem1  27843  dchrisum0flblem1  27850  dchrisum0flblem2  27851  dchrisum0flb  27852  dchrisum0re  27855  dchrisum0lem1b  27857  dchrisum0lem1  27858  dchrisum0lem2a  27859  dchrisum0lem2  27860  dchrisum0lem3  27861  mudivsum  27872  mulogsum  27874  mulog2sumlem2  27877  selberg2lem  27892  logdivbnd  27898  pntrsumo1  27907  pntrsumbnd2  27909  pntrlog2bndlem2  27920  pntrlog2bndlem4  27922  pntrlog2bndlem6a  27924  pntlemj  27945  pntlemf  27947  ostth2lem3  27977  madebdayim  28289  oldbdayim  28290  newbdayim  28304  cutminmax  28337  noseqp1  28692  tglngne  29028  ltgseg  29074  eedimeq  29491  axlowdimlem16  29550  ebtwntg  29575  subgruhgredgd  29880  subumgredg2  29881  umgrres1lem  29906  wlkson  30250  wksonproplem  30302  trlsonfval  30303  pthsonfval  30341  spthson  30342  crctcshwlkn0lem4  30417  crctcshwlkn0lem5  30418  eupth2lems  30854  numclwwlk1lem2foa  30970  numclwlk1lem2  30986  numclwwlk2lem1  30992  htthlem  31534  hhsscms  31895  shmodsi  32006  pjoc1i  32048  5oalem1  32271  mayete3i  32345  adj1  32550  iundisj2f  33241  fmptco1f1o  33284  fcnvgreu  33323  suppovss  33331  ssnnssfz  33435  nn0diffz0  33442  iundisj2fi  33445  indpreima  33488  ccatws1f1o  33570  cshw1s2  33577  gsumhashmul  33684  gsummulsubdishift1  33685  gsumwrd2dccat  33695  fzo0pmtrlast  33709  wrdpmtrlast  33710  pmtrto1cl  33716  psgnfzto1stlem  33717  fzto1st1  33719  cycpmfv1  33730  cycpmfv2  33731  cycpmco2rn  33742  cycpmco2lem4  33746  cycpmco2lem5  33747  cycpmco2lem6  33748  cyc3evpm  33767  cyc3genpm  33769  cycpmconjslem2  33772  cyc3conja  33774  elrgspnlem1  33859  elrgspnlem2  33860  erler  33882  nsgmgc  34019  nsgqusf1olem2  34021  unitpidl1  34030  elrspunsn  34035  mxidlirredi  34052  mxidlirred  34053  opprqusplusg  34069  opprqus0g  34070  opprqusmulr  34071  idlsrgmulrss1  34099  idlsrgmulrss2  34100  rprmcl  34106  rprmdvds  34107  rprmnz  34108  rprmnunit  34109  rprmasso  34113  rprmirredb  34120  pidufd  34131  1arithufdlem2  34133  1arithufdlem3  34134  zringfrac  34142  ply1dg3rt0irred  34172  m1pmeq  34173  ig1pmindeg  34190  selvply1rhmlem2  34209  selvply1rhmlem4  34211  selvply1rhm0  34214  extvfvvcl  34223  evlextv  34230  psrmonprod  34240  esplysply  34259  esplyind  34263  esplyfvn  34265  vietalem  34267  exsslsb  34285  ply1degltdimlem  34310  lindsun  34313  fldextfld1  34335  fldextfld2  34336  rtelextdg2  34415  cos9thpiminplylem1  34470  1smat1  34492  submateqlem2  34496  lmatfval  34502  mdetlap1  34514  madjusmdetlem1  34515  madjusmdetlem2  34516  madjusmdetlem3  34517  madjusmdetlem4  34518  zarclssn  34561  zartopn  34563  zarmxt1  34568  rhmpreimacnlem  34572  rhmpreimacn  34573  pnfneige0  34639  pl1cn  34643  rrhqima  34702  esumfzf  34757  esumpcvgval  34766  esumpmono  34767  esumcvg  34774  ldgenpisyslem1  34852  ldgenpisys  34855  measbase  34886  dya2iocnei  34970  oddpwdc  35042  eulerpartlems  35048  eulerpartlemb  35056  sseqf  35080  fibp1  35089  orrvcval4  35153  orrvcoel  35154  orrvccel  35155  ballotlem2  35177  ballotlemfrceq  35217  signsplypnf  35235  signswch  35246  signstf0  35253  signstfvn  35254  signstfvneq0  35257  signstfvcl  35258  signstfveq0  35262  signsvfn  35267  fct2relem  35282  fsum2dsub  35292  reprsuc  35300  reprpmtf1o  35311  breprexplema  35315  breprexplemc  35317  hgt749d  35334  hgt750lemb  35341  tgoldbachgnn  35344  bnj1172  35687  bnj1245  35700  bnj1311  35710  bnj1450  35736  bnj1501  35753  subfacp1lem1  36068  subfacp1lem5  36073  subfacp1lem6  36074  subfacval2  36076  erdszelem7  36086  cvxpconn  36131  cvxsconn  36132  cvmliftlem5  36178  cvmliftlem7  36180  cvmliftlem10  36183  cvmliftlem13  36185  mrsubvrs  36411  msubrn  36418  msubco  36420  msubvrs  36449  r1peuqusdeg1  36532  imageval  36825  fwddifnp1  37063  knoppcnlem8  37499  knoppcnlem10  37501  bj-unirel  38111  icoreunrn  38428  istoprelowl  38429  poimirlem3  38687  poimirlem4  38688  poimirlem6  38690  poimirlem7  38691  poimirlem8  38692  poimirlem12  38696  poimirlem15  38699  poimirlem16  38700  poimirlem17  38701  poimirlem18  38702  poimirlem19  38703  poimirlem20  38704  poimirlem21  38705  poimirlem22  38706  poimirlem23  38707  poimirlem24  38708  poimirlem25  38709  poimirlem26  38710  poimirlem27  38711  poimirlem28  38712  poimirlem29  38713  poimirlem31  38715  mblfinlem2  38722  ftc1cnnc  38756  upixp  38809  sdclem2  38822  caushft  38841  ismtyres  38888  rrnmet  38909  rrndstprj1  38910  rrndstprj2  38911  rrncmslem  38912  rrnequiv  38915  iccbnd  38920  osumcllem7N  41165  pexmidlem4N  41176  lcfrlem4  42748  lcfrlem5  42749  lcfrlem6  42750  lcfrlem16  42761  lcfrlem38  42783  mapdrvallem2  42848  mapdh8ab  42980  mapdh8ad  42982  mapdh8e  42987  3factsumint3  43219  aks4d1p1p1  43259  fldhmf1  43286  aks6d1c1p2  43305  aks6d1c1p3  43306  aks6d1c1p7  43309  aks6d1c1p6  43310  aks6d1c1p8  43311  aks6d1c1  43312  evl1gprodd  43313  idomnnzpownz  43328  aks6d1c5lem1  43332  aks6d1c5lem3  43333  aks6d1c5lem2  43334  deg1gprod  43336  sticksstones10  43351  aks6d1c6lem3  43368  aks5lem2  43383  aks5lem3a  43385  unitscyglem5  43395  fz1sump1  43513  sumcubes  43516  evlselv  43763  mhphf2  43772  frlmnzcoordex  43798  frlmnzcoordsca  43804  prjspnnorm  43807  mapfzcons  43873  diophren  43966  irrapxlem1  43975  monotuz  44094  acongeq  44136  jm2.26lem3  44154  jm3.1lem2  44171  pw2f1ocnv  44190  idomodle  44339  trclfvdecomr  44874  imo72b2lem0  45311  imo72b2lem1  45315  dvgrat  45442  cvgdvgrat  45443  hashnzfz2  45451  fcnre  46187  refsumcn  46192  rfcnnnub  46198  disjf1o  46351  disjinfi  46352  ssmapsn  46374  ssuzfz  46506  nnsplit  46515  uzssd2  46572  uzublem  46585  fsumsermpt  46736  climsuselem1  46764  limcperiod  46785  sumnnodd  46787  lptioo2cn  46800  lptioo1cn  46801  climresmpt  46814  allbutfifvre  46830  climleltrp  46831  cnrefiisplem  46984  cncfshift  47029  cncfperiod  47034  cncfshiftioo  47047  fperdvper  47074  dvnmptdivc  47093  dvnmul  47098  dvmptfprod  47100  dvnprodlem3  47103  stoweidlem11  47166  stoweidlem15  47170  stoweidlem17  47172  stoweidlem20  47175  stoweidlem34  47189  stoweidlem35  47190  stoweidlem46  47201  stoweidlem47  47202  stoweidlem56  47211  stoweidlem59  47214  stoweidlem62  47217  stirlinglem5  47233  stirlinglem14  47242  dirkertrigeqlem2  47254  dirkertrigeqlem3  47255  fourierdlem11  47273  fourierdlem15  47277  fourierdlem16  47278  fourierdlem21  47283  fourierdlem22  47284  fourierdlem25  47287  fourierdlem48  47309  fourierdlem49  47310  fourierdlem52  47313  fourierdlem54  47315  fourierdlem58  47319  fourierdlem62  47323  fourierdlem64  47325  fourierdlem65  47326  fourierdlem69  47330  fourierdlem70  47331  fourierdlem71  47332  fourierdlem73  47334  fourierdlem80  47341  fourierdlem81  47342  fourierdlem83  47344  fourierdlem92  47353  fourierdlem93  47354  fourierdlem97  47358  fourierdlem103  47364  fourierdlem104  47365  fourierdlem112  47373  fourierdlem113  47374  fouriercnp  47381  fouriersw  47386  elaa2lem  47388  etransclem4  47393  etransclem7  47396  etransclem10  47399  etransclem14  47403  etransclem15  47404  etransclem24  47413  etransclem25  47414  etransclem31  47420  etransclem32  47421  etransclem35  47424  etransclem44  47433  etransclem46  47435  qndenserrnopnlem  47452  qndenserrn  47454  prsal  47473  salgencntex  47498  subsaliuncl  47513  subsalsal  47514  sge0tsms  47535  sge0fodjrnlem  47571  sge0isum  47582  iundjiunlem  47614  iundjiun  47615  meadjiunlem  47620  meaiunlelem  47623  meaiuninclem  47635  meaiininc2  47643  caragensplit  47655  carageneld  47657  carageniuncllem1  47676  caratheodorylem1  47681  caratheodorylem2  47682  hoicvr  47703  hsphoidmvle2  47740  hsphoidmvle  47741  hoidmv1lelem2  47747  hoidmv1lelem3  47748  hoidmvlelem2  47751  hoiqssbllem2  47778  pimdecfgtioc  47870  pimincfltioc  47871  pimdecfgtioo  47872  pimincfltioo  47873  smflimlem3  47928  smfmullem4  47949  smfsupxr  47971  smflimsuplem2  47976  smflimsuplem5  47979  ormklocald  48031  chnerlem1  48037  elmod2  48576  isuspgrim0lem  49136  upgrimtrlslem2  49148  ssnn0ssfz  49606  zlmodzxzscm  49614  rmsupp0  49625  lincsum  49686  lincscm  49687  lindslinindimp2lem4  49718  lincresunit3  49738  elbigofrcl  49807  elovmpoeq  50125  intubeu  50243  unilbeu  50244  cicrcl2  50302  cic1st2nd  50306  imaf1homlem  50368  oppfrcl  50389  eloppf  50394  imasubc  50412  imaid  50415  oppcuprcl5  50462  oppcup3  50470  uptrlem2  50472  uptrlem3  50473  natoppf  50496  elxpcbasex1ALT  50516  elxpcbasex2ALT  50518  swapf1a  50536  swapf2f1oa  50544  swapfida  50547  cofuswapf1  50561  cofuswapf2  50562  fucoppcco  50689  postc  50852  reldmlan2  50945  reldmran2  50946  lanrcl  50949  ranrcl  50950  aacllem  51159  crosspaltd  51186  crossp3d  51187  veronesematbasd  51200  veroquaddetzerod  51206