Theorem eleqtrdi 2923

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  eleqtrrdi  2924  3eltr3g  2929  prid2g  4697  ndmfvrcl  6701  fnwelem  7825  tz7.48-1  8079  brwitnlem  8132  oeeulem  8227  dffi3  8895  cnfcom3lem  9166  alephgeom  9508  fpwwe2lem6  10057  canthwelem  10072  hargch  10095  r1wunlim  10159  eluzel2  12249  fseq1p1m1  12982  fznn0sub2  13015  nn0split  13023  exple1  13541  digit1  13599  bcval5  13679  bcpasc  13682  hashf1  13816  seqcoll  13823  seqcoll2  13824  ccatrn  13943  swrdccat2  14031  cats1un  14083  pfxccatin12lem3  14094  splfv2a  14118  splval2  14119  caubnd  14718  limsupgre  14838  clim2ser  15011  clim2ser2  15012  iserex  15013  isermulc2  15014  iserle  15016  iserge0  15017  climub  15018  climserle  15019  isercolllem2  15022  isercolllem3  15023  isercoll  15024  isercoll2  15025  serf0  15037  iseraltlem2  15039  iseraltlem3  15040  iseralt  15041  sumeq2ii  15050  summolem3  15071  summolem2a  15072  fsum  15077  sum0  15078  fsumcl2lem  15088  fsumadd  15096  isumclim3  15114  isumadd  15122  fsump1i  15124  fsummulc2  15139  fsumrelem  15162  iserabs  15170  cvgcmp  15171  cvgcmpub  15172  cvgcmpce  15173  binom1dif  15188  isumshft  15194  isumsplit  15195  isumrpcl  15198  isumsup2  15201  climcndslem1  15204  climcndslem2  15205  climcnds  15206  arisum2  15216  trireciplem  15217  geoser  15222  pwdif  15223  geolim  15226  geo2lim  15231  cvgrat  15239  mertenslem1  15240  mertenslem2  15241  mertens  15242  clim2prod  15244  clim2div  15245  ntrivcvgfvn0  15255  ntrivcvgtail  15256  prodeq2ii  15267  prodmolem3  15287  prodmolem2a  15288  fprod  15295  fprodntriv  15296  fprodss  15302  fprodser  15303  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodabs  15328  fprodeq0  15329  fprodn0  15333  iprodclim3  15354  iprodmul  15357  fallfacfwd  15390  0fallfac  15391  binomfallfaclem2  15394  fallfacval4  15397  bpolysum  15407  bpolydiflem  15408  fsumkthpow  15410  efcvgfsum  15439  efcj  15445  fprodefsum  15448  effsumlt  15464  ruclem7  15589  bitsfzolem  15783  bitsfzo  15784  bitsfi  15786  bitsinv1lem  15790  bitsinv1  15791  bitsinvp1  15798  sadcp1  15804  sadadd  15816  sadass  15820  bitsres  15822  smupp1  15829  smuval2  15831  smupval  15837  smueqlem  15839  smumul  15842  algrp1  15918  phiprmpw  16113  crth  16115  phimullem  16116  eulerthlem2  16119  prmdiv  16122  pcpremul  16180  pcmpt  16228  pcfac  16235  pockthlem  16241  pockthg  16242  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  prmrec  16258  1arith  16263  vdwapun  16310  vdwlem1  16317  vdwlem2  16318  vdwlem3  16319  vdwlem6  16322  vdwlem8  16324  vdwlem10  16326  vdw  16330  imasvscafn  16810  oppccatid  16989  oppccomfpropd  16997  brcic  17068  funcoppc  17145  invfuc  17244  hofcl  17509  yonedalem4c  17527  gsumwsubmcl  18001  gsumsgrpccat  18004  gsumccatOLD  18005  gsumwmhm  18010  mulgnnp1  18236  mulgnnsubcl  18240  mulgnn0z  18254  mulgnndir  18256  psgnunilem4  18625  psgnran  18643  sylow1lem1  18723  lsmmod2  18802  lsmdisj2r  18811  efginvrel2  18853  efgsdmi  18858  efgsrel  18860  efgs1b  18862  efgsp1  18863  efgredleme  18869  efgredlemc  18871  efgcpbllemb  18881  frgpuplem  18898  mulgnn0di  18946  frgpnabllem1  18993  lt6abl  19015  cycsubgcyg  19021  gsumval3eu  19024  gsumval3  19027  gsumzcl2  19030  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsumzoppg  19064  telgsumfz0s  19111  dprdwd  19133  dprd2da  19164  pgpfaclem1  19203  srgbinom  19295  isirred  19449  lspprid2  19770  lspsnat  19917  lsppratlem1  19919  lsppratlem3  19921  lidl0cl  19985  lidlacl  19986  lidlnegcl  19987  lidlmcl  19990  psrbaglefi  20152  psrass23l  20188  psrass23  20190  mplcoe5lem  20248  mpfind  20320  selvval  20331  mhpinvcl  20339  mhpvscacl  20341  psr1bascl  20368  ply1basf  20370  gsummoncoe1  20472  lply1binom  20474  lply1binomsc  20475  mpfpf1  20514  pf1mpf  20515  evl1scvarpw  20526  psgnghm  20724  frlmvscavalb  20914  frlmvplusgscavalb  20915  matbas2i  21031  matecld  21035  matgsum  21046  mpomatmul  21055  dmatmul  21106  1mavmul  21157  mdetleib2  21197  m1detdiag  21206  marep01ma  21269  smadiadetlem4  21278  slesolinv  21289  pmatcollpw3fi1lem1  21394  chpscmat  21450  chpscmatgsumbin  21452  chp0mat  21454  chpidmat  21455  chfacfisf  21462  chfacfisfcpmat  21463  chfacfpmmulgsum2  21473  cldrcl  21634  ordtbas  21800  iscnp2  21847  dis1stc  22107  ptbasfi  22189  ptpjopn  22220  ptclsg  22223  ptcnp  22230  kqtop  22353  reghmph  22401  ptcmplem2  22661  ptcmplem3  22662  ptcmplem4  22663  tsmslem1  22737  utop2nei  22859  isucn2  22888  cuspcvg  22910  cnextucn  22912  imasdsf1olem  22983  blcvx  23406  xrhmeo  23550  cnrehmeo  23557  evth  23563  reparphti  23601  iscau4  23882  iscmet3lem1  23894  lmle  23904  rrxfsupp  24005  rrxdsfi  24014  pjthlem2  24041  ovollb2lem  24089  ovolunlem1a  24097  ovoliunlem1  24103  ovoliun2  24107  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem4  24121  iundisj2  24150  voliunlem1  24151  volsup  24157  ioombl1lem4  24162  uniioovol  24180  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  vitalilem5  24213  mbfimaopnlem  24256  mbflimsup  24267  mbfi1fseqlem3  24318  iblitg  24369  dvnp1  24522  cpncn  24533  dvlip2  24592  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumrlimge0  24627  dvfsumrlim2  24629  ftc1cn  24640  elplyd  24792  ply1termlem  24793  ply1term  24794  ply0  24798  plyeq0lem  24800  plyaddlem1  24803  plymullem1  24804  plyaddlem  24805  plymullem  24806  coeeulem  24814  plyco  24831  coeeq2  24832  coefv0  24838  coemulhi  24844  coemulc  24845  plycj  24867  dvply1  24873  vieta1lem2  24900  elqaalem2  24909  dvtaylp  24958  dvntaylp  24959  taylthlem1  24961  taylth  24963  ulmres  24976  ulmshftlem  24977  ulmshft  24978  ulmcau  24983  ulmdvlem1  24988  mtest  24992  mtestbdd  24993  pserulm  25010  psercn2  25011  psercnlem1  25013  psercn  25014  pserdvlem2  25016  abelthlem6  25024  abelth  25029  efif1olem1  25126  efif1olem3  25128  efif1olem4  25129  logcn  25230  advlogexp  25238  efopn  25241  cxpeq  25338  asinsin  25470  atantayl  25515  leibpilem2  25519  birthdaylem2  25530  birthdaylem3  25531  efrlim  25547  emcllem2  25574  emcllem5  25577  emcllem7  25579  harmonicbnd4  25588  fsumharmonic  25589  lgamgulm2  25613  lgamcvglem  25617  lgamcvg2  25632  gamcvg2lem  25636  wilthlem2  25646  wilthlem3  25647  ftalem1  25650  ftalem2  25651  ftalem3  25652  ftalem5  25654  basellem2  25659  basellem3  25660  basellem5  25662  basellem8  25665  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  chpp1  25732  vma1  25743  ppiltx  25754  musum  25768  0sgmppw  25774  1sgmprm  25775  ppiublem2  25779  chtublem  25787  fsumvma2  25790  chpchtsum  25795  logexprlim  25801  bposlem5  25864  lgscllem  25880  lgsval2lem  25883  lgsval4a  25895  lgsneg  25897  lgsdir2lem3  25903  lgsdir2lem5  25905  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  gausslemma2dlem3  25944  lgseisenlem1  25951  lgsquadlem2  25957  chebbnd1lem1  26045  chtppilimlem1  26049  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem2  26066  dchrmusum2  26070  dchrvmasum2lem  26072  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0flb  26086  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  mudivsum  26106  mulogsum  26108  mulog2sumlem2  26111  selberg2lem  26126  logdivbnd  26132  pntrsumo1  26141  pntrsumbnd2  26143  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntrlog2bndlem6a  26158  pntlemj  26179  pntlemf  26181  ostth2lem3  26211  tglngne  26336  ltgseg  26382  eedimeq  26684  axlowdimlem16  26743  ebtwntg  26768  subgruhgredgd  27066  subumgredg2  27067  umgrres1lem  27092  wlkson  27438  wksonproplem  27486  trlsonfval  27487  pthsonfval  27521  spthson  27522  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  eupth2lems  28017  numclwwlk1lem2foa  28133  numclwlk1lem2  28149  numclwwlk2lem1  28155  htthlem  28694  hhsscms  29055  shmodsi  29166  pjoc1i  29208  5oalem1  29431  mayete3i  29505  adj1  29710  iundisj2f  30340  fmptco1f1o  30378  fcnvgreu  30418  suppovss  30426  ssnnssfz  30510  iundisj2fi  30520  cshw1s2  30634  pmtrto1cl  30741  psgnfzto1stlem  30742  fzto1st1  30744  cycpmfv1  30755  cycpmfv2  30756  cycpmco2rn  30767  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cyc3evpm  30792  cyc3genpm  30794  cycpmconjslem2  30797  cyc3conja  30799  rspsnel  30936  lindsun  31021  fldextfld1  31039  fldextfld2  31040  1smat1  31069  submateqlem2  31073  lmatfval  31079  mdetlap1  31091  madjusmdetlem1  31092  madjusmdetlem2  31093  madjusmdetlem3  31094  madjusmdetlem4  31095  pnfneige0  31194  pl1cn  31198  rrhqima  31255  indpreima  31284  esumfzf  31328  esumpcvgval  31337  esumpmono  31338  esumcvg  31345  ldgenpisyslem1  31422  ldgenpisys  31425  measbase  31456  dya2iocnei  31540  oddpwdc  31612  eulerpartlems  31618  eulerpartlemb  31626  sseqf  31650  fibp1  31659  orrvcval4  31722  orrvcoel  31723  orrvccel  31724  ballotlem2  31746  ballotlemfrceq  31786  signsplypnf  31820  signswch  31831  signstf0  31838  signstfvn  31839  signstfvneq0  31842  signstfvcl  31843  signstfveq0  31847  signsvfn  31852  fct2relem  31868  fsum2dsub  31878  reprsuc  31886  reprpmtf1o  31897  breprexplema  31901  breprexplemc  31903  hgt749d  31920  hgt750lemb  31927  tgoldbachgnn  31930  bnj1172  32273  bnj1245  32286  bnj1311  32296  bnj1450  32322  bnj1501  32339  subfacp1lem1  32426  subfacp1lem5  32431  subfacp1lem6  32432  subfacval2  32434  erdszelem7  32444  cvxsconn  32490  cvmliftlem5  32536  cvmliftlem7  32538  cvmliftlem10  32541  cvmliftlem13  32543  mrsubvrs  32769  msubrn  32776  msubco  32778  msubvrs  32807  imageval  33391  fwddifnp1  33626  knoppcnlem8  33839  knoppcnlem10  33841  bj-unirel  34347  icoreunrn  34643  istoprelowl  34644  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem12  34919  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  mblfinlem2  34945  ftc1cnnc  34981  upixp  35019  sdclem2  35032  caushft  35051  ismtyres  35101  rrnmet  35122  rrndstprj1  35123  rrndstprj2  35124  rrncmslem  35125  rrnequiv  35128  iccbnd  35133  osumcllem7N  37113  pexmidlem4N  37124  lcfrlem4  38696  lcfrlem5  38697  lcfrlem6  38698  lcfrlem16  38709  lcfrlem38  38731  mapdrvallem2  38796  mapdh8ab  38928  mapdh8ad  38930  mapdh8e  38935  mapfzcons  39362  diophren  39459  irrapxlem1  39468  monotuz  39587  acongeq  39629  jm2.26lem3  39647  jm3.1lem2  39664  pw2f1ocnv  39683  idomodle  39845  trclfvdecomr  40122  imo72b2lem1  40570  scottelrankd  40632  dvgrat  40693  cvgdvgrat  40694  hashnzfz2  40702  fcnre  41331  refsumcn  41336  rfcnnnub  41342  disjf1o  41501  disjinfi  41503  ssmapsn  41528  ssuzfz  41666  nnsplit  41675  uzssd2  41740  uzublem  41753  fsumsermpt  41909  climsuselem1  41937  limcperiod  41958  sumnnodd  41960  lptioo2cn  41975  lptioo1cn  41976  climresmpt  41989  allbutfifvre  42005  climleltrp  42006  cnrefiisplem  42159  cncfshift  42206  cncfperiod  42211  cncfshiftioo  42224  fperdvper  42252  dvnmptdivc  42272  dvnmul  42277  dvmptfprod  42279  dvnprodlem3  42282  stoweidlem11  42345  stoweidlem15  42349  stoweidlem17  42351  stoweidlem20  42354  stoweidlem34  42368  stoweidlem35  42369  stoweidlem46  42380  stoweidlem47  42381  stoweidlem56  42390  stoweidlem59  42393  stoweidlem62  42396  stirlinglem5  42412  stirlinglem14  42421  dirkertrigeqlem2  42433  dirkertrigeqlem3  42434  fourierdlem11  42452  fourierdlem15  42456  fourierdlem16  42457  fourierdlem21  42462  fourierdlem22  42463  fourierdlem25  42466  fourierdlem48  42488  fourierdlem52  42492  fourierdlem54  42494  fourierdlem58  42498  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem69  42509  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem80  42520  fourierdlem81  42521  fourierdlem83  42523  fourierdlem92  42532  fourierdlem93  42533  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierdlem113  42553  fouriercnp  42560  fouriersw  42565  elaa2lem  42567  etransclem4  42572  etransclem7  42575  etransclem10  42578  etransclem14  42582  etransclem15  42583  etransclem24  42592  etransclem25  42593  etransclem31  42599  etransclem32  42600  etransclem35  42603  etransclem44  42612  etransclem46  42614  qndenserrnopnlem  42631  qndenserrn  42633  prsal  42652  salgencntex  42675  subsaliuncl  42690  subsalsal  42691  sge0tsms  42711  sge0fodjrnlem  42747  sge0isum  42758  iundjiunlem  42790  iundjiun  42791  meadjiunlem  42796  meaiunlelem  42799  meaiuninclem  42811  meaiininc2  42819  caragensplit  42831  carageneld  42833  carageniuncllem1  42852  caratheodorylem1  42857  caratheodorylem2  42858  hoicvr  42879  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem2  42927  hoiqssbllem2  42954  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  smflimlem3  43098  smfmullem4  43118  smfsupxr  43139  smflimsuplem2  43144  smflimsuplem5  43147  elmod2  43579  ssnn0ssfz  44446  zlmodzxzscm  44454  rmsupp0  44465  lincsum  44533  lincscm  44534  lindslinindimp2lem4  44565  lincresunit3  44585  elbigofrcl  44659  setrec1  44843  aacllem  44951