Theorem eleqtrdi 2843

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-clel 2808

This theorem is referenced by:  eleqtrrdi  2844  3eltr3g  2849  prid2g  4741  ndmfvrcl  6922  fnwelem  8138  tz7.48-1  8465  brwitnlem  8527  oeeulem  8621  dffi3  9453  cnfcom3lem  9725  ttrclse  9749  alephgeom  10104  fpwwe2lem5  10657  canthwelem  10672  hargch  10695  r1wunlim  10759  eluzel2  12865  fseq1p1m1  13620  fznn0sub2  13657  nn0split  13665  seqp1d  14041  exple1  14199  digit1  14259  bcval5  14340  bcpasc  14343  hashf1  14479  seqcoll  14486  seqcoll2  14487  ccatrn  14610  swrdccat2  14690  cats1un  14742  pfxccatin12lem3  14753  splfv2a  14777  splval2  14778  caubnd  15380  limsupgre  15500  clim2ser  15674  clim2ser2  15675  iserex  15676  isermulc2  15677  iserle  15679  iserge0  15680  climub  15681  climserle  15682  isercolllem2  15685  isercolllem3  15686  isercoll  15687  isercoll2  15688  serf0  15700  iseraltlem2  15702  iseraltlem3  15703  iseralt  15704  sumeq2ii  15712  summolem3  15733  summolem2a  15734  fsum  15739  sum0  15740  fsumcl2lem  15750  fsumadd  15759  isumclim3  15778  isumadd  15786  fsump1i  15788  fsummulc2  15803  fsumrelem  15826  iserabs  15834  cvgcmp  15835  cvgcmpub  15836  cvgcmpce  15837  binom1dif  15852  isumshft  15858  isumsplit  15859  isumrpcl  15862  isumsup2  15865  climcndslem1  15868  climcndslem2  15869  climcnds  15870  arisum2  15880  trireciplem  15881  geoser  15886  pwdif  15887  geolim  15889  geo2lim  15894  cvgrat  15902  mertenslem1  15903  mertenslem2  15904  mertens  15905  clim2prod  15907  clim2div  15908  ntrivcvgfvn0  15918  ntrivcvgtail  15919  prodeq2ii  15930  prodmolem3  15952  prodmolem2a  15953  fprod  15960  fprodntriv  15961  fprodss  15967  fprodser  15968  fprodcl2lem  15969  fprodmul  15979  fproddiv  15980  fprodabs  15993  fprodeq0  15994  fprodn0  15998  iprodclim3  16019  iprodmul  16022  fallfacfwd  16055  0fallfac  16056  binomfallfaclem2  16059  fallfacval4  16062  bpolysum  16072  bpolydiflem  16073  fsumkthpow  16075  efcvgfsum  16105  efcj  16111  fprodefsum  16114  effsumlt  16130  ruclem7  16255  bitsfzolem  16454  bitsfzo  16455  bitsfi  16457  bitsinv1lem  16461  bitsinv1  16462  bitsinvp1  16469  sadcp1  16475  sadadd  16487  sadass  16491  bitsres  16493  smupp1  16500  smuval2  16502  smupval  16508  smueqlem  16510  smumul  16513  algrp1  16594  phiprmpw  16796  crth  16798  phimullem  16799  eulerthlem2  16802  prmdiv  16805  pcpremul  16864  pcmpt  16913  pcfac  16920  pockthlem  16926  pockthg  16927  prmreclem2  16938  prmreclem3  16939  prmreclem4  16940  prmreclem5  16941  prmreclem6  16942  prmrec  16943  1arith  16948  vdwapun  16995  vdwlem1  17002  vdwlem2  17003  vdwlem3  17004  vdwlem6  17007  vdwlem8  17009  vdwlem10  17011  vdw  17015  imasvscafn  17554  oppccatid  17734  oppccomfpropd  17742  brcic  17814  funcoppc  17892  invfuc  17994  hofcl  18275  yonedalem4c  18293  gsumwsubmcl  18820  gsumsgrpccat  18823  gsumwmhm  18828  mulgnnp1  19070  mulgnnsubcl  19074  mulgnn0z  19089  mulgnndir  19091  ghmquskerlem1  19271  ghmquskerco  19272  psgnunilem4  19484  psgnran  19502  sylow1lem1  19585  lsmmod2  19663  lsmdisj2r  19672  efginvrel2  19714  efgsdmi  19719  efgsrel  19721  efgs1b  19723  efgsp1  19724  efgredleme  19730  efgredlemc  19732  efgcpbllemb  19742  frgpuplem  19759  mulgnn0di  19812  frgpnabllem1  19860  lt6abl  19882  cycsubgcyg  19888  gsumval3eu  19891  gsumval3  19894  gsumzcl2  19897  gsumzaddlem  19908  gsumconst  19921  gsumzmhm  19924  gsumzoppg  19931  telgsumfz0s  19978  dprdwd  20000  dprd2da  20031  pgpfaclem1  20070  srgbinom  20197  isirred  20388  idomdomd  20695  idomcringd  20696  lspprid2  20965  lspsnat  21116  lsppratlem1  21118  lsppratlem3  21120  lidl0cl  21193  lidlacl  21194  lidlnegcl  21195  elrspsn  21213  2idllidld  21227  2idlridld  21228  rng2idl1cntr  21278  psgnghm  21553  frlmvscavalb  21745  frlmvplusgscavalb  21746  psrbaglefi  21901  psrass23l  21942  psrass23  21944  mplcoe5lem  22012  mpfind  22080  selvval  22088  mhpvscacl  22107  psr1bascl  22151  ply1basf  22153  gsummoncoe1  22261  lply1binom  22263  lply1binomsc  22264  mpfpf1  22304  pf1mpf  22305  evl1scvarpw  22316  evl1maprhm  22332  matbas2i  22377  matecld  22381  matgsum  22392  mpomatmul  22401  dmatmul  22452  1mavmul  22503  mdetleib2  22543  m1detdiag  22552  marep01ma  22615  smadiadetlem4  22624  slesolinv  22635  pmatcollpw3fi1lem1  22741  chpscmat  22797  chpscmatgsumbin  22799  chp0mat  22801  chpidmat  22802  chfacfisf  22809  chfacfisfcpmat  22810  chfacfpmmulgsum2  22820  cldrcl  22981  ordtbas  23147  iscnp2  23194  dis1stc  23454  ptbasfi  23536  ptpjopn  23567  ptclsg  23570  ptcnp  23577  kqtop  23700  reghmph  23748  ptcmplem2  24008  ptcmplem3  24009  ptcmplem4  24010  tsmslem1  24084  utop2nei  24206  isucn2  24234  cuspcvg  24256  cnextucn  24258  imasdsf1olem  24329  blcvx  24756  xrhmeo  24914  cnrehmeo  24921  cnrehmeoOLD  24922  evth  24928  reparphti  24966  reparphtiOLD  24967  iscau4  25250  iscmet3lem1  25262  lmle  25272  rrxfsupp  25373  rrxdsfi  25382  pjthlem2  25409  ovollb2lem  25460  ovolunlem1a  25468  ovoliunlem1  25474  ovoliun2  25478  ovolscalem1  25485  ovolicc1  25488  ovolicc2lem4  25492  iundisj2  25521  voliunlem1  25522  volsup  25528  ioombl1lem4  25533  uniioovol  25551  uniioombllem3  25557  uniioombllem4  25558  uniioombllem6  25560  vitalilem5  25584  mbfimaopnlem  25627  mbflimsup  25638  mbfi1fseqlem3  25689  iblitg  25740  dvcnp2  25892  dvnp1  25898  cpncn  25909  dvmulbr  25912  dvcobr  25920  dvlip2  25971  dvfsumlem2  26004  dvfsumlem2OLD  26005  dvfsumlem3  26006  dvfsumrlimge0  26008  dvfsumrlim2  26010  ftc1cn  26021  elplyd  26178  ply1termlem  26179  ply1term  26180  ply0  26184  plyeq0lem  26186  plyaddlem1  26189  plymullem1  26190  plyaddlem  26191  plymullem  26192  coeeulem  26200  plyco  26217  coeeq2  26218  coefv0  26224  coemulhi  26230  coemulc  26231  plycj  26254  plycjOLD  26256  dvply1  26262  vieta1lem2  26290  elqaalem2  26299  dvtaylp  26349  dvntaylp  26350  taylthlem1  26352  taylth  26355  ulmres  26368  ulmshftlem  26369  ulmshft  26370  ulmcau  26375  ulmdvlem1  26380  mtest  26384  mtestbdd  26385  pserulm  26402  psercn2  26403  psercn2OLD  26404  psercnlem1  26406  psercn  26407  pserdvlem2  26409  abelthlem6  26417  abelth  26422  efif1olem1  26521  efif1olem3  26523  efif1olem4  26524  logcn  26626  advlogexp  26634  efopn  26637  cxpeq  26737  asinsin  26872  atantayl  26917  leibpilem2  26921  birthdaylem2  26932  birthdaylem3  26933  efrlim  26949  efrlimOLD  26950  emcllem2  26977  emcllem5  26980  emcllem7  26982  harmonicbnd4  26991  fsumharmonic  26992  lgamgulm2  27016  lgamcvglem  27020  lgamcvg2  27035  gamcvg2lem  27039  wilthlem2  27049  wilthlem3  27050  ftalem1  27053  ftalem2  27054  ftalem3  27055  ftalem5  27057  basellem2  27062  basellem3  27063  basellem5  27065  basellem8  27068  ppiprm  27131  ppinprm  27132  chtprm  27133  chtnprm  27134  chpp1  27135  vma1  27146  ppiltx  27157  musum  27171  0sgmppw  27179  1sgmprm  27180  ppiublem2  27184  chtublem  27192  fsumvma2  27195  chpchtsum  27200  logexprlim  27206  bposlem5  27269  lgscllem  27285  lgsval2lem  27288  lgsval4a  27300  lgsneg  27302  lgsdir2lem3  27308  lgsdir2lem5  27310  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  gausslemma2dlem3  27349  lgseisenlem1  27356  lgsquadlem2  27362  chebbnd1lem1  27450  chtppilimlem1  27454  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasum2lem  27477  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0flb  27491  dchrisum0re  27494  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  mudivsum  27511  mulogsum  27513  mulog2sumlem2  27516  selberg2lem  27531  logdivbnd  27537  pntrsumo1  27546  pntrsumbnd2  27548  pntrlog2bndlem2  27559  pntrlog2bndlem4  27561  pntrlog2bndlem6a  27563  pntlemj  27584  pntlemf  27586  ostth2lem3  27616  madebdayim  27863  oldbdayim  27864  noseqp1  28234  tglngne  28495  ltgseg  28541  eedimeq  28844  axlowdimlem16  28903  ebtwntg  28928  subgruhgredgd  29230  subumgredg2  29231  umgrres1lem  29256  wlkson  29603  wksonproplem  29651  wksonproplemOLD  29652  trlsonfval  29653  pthsonfval  29689  spthson  29690  crctcshwlkn0lem4  29762  crctcshwlkn0lem5  29763  eupth2lems  30186  numclwwlk1lem2foa  30302  numclwlk1lem2  30318  numclwwlk2lem1  30324  htthlem  30865  hhsscms  31226  shmodsi  31337  pjoc1i  31379  5oalem1  31602  mayete3i  31676  adj1  31881  iundisj2f  32539  fmptco1f1o  32579  fcnvgreu  32619  suppovss  32626  ssnnssfz  32733  iundisj2fi  32743  indpreima  32795  ccatws1f1o  32881  cshw1s2  32890  chnccats1  32949  gsumhashmul  33008  gsumwrd2dccat  33014  fzo0pmtrlast  33056  wrdpmtrlast  33057  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1st1  33066  cycpmfv1  33077  cycpmfv2  33078  cycpmco2rn  33089  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cyc3evpm  33114  cyc3genpm  33116  cycpmconjslem2  33119  cyc3conja  33121  elrgspnlem1  33190  elrgspnlem2  33191  erler  33213  idomrcanOLD  33229  nsgmgc  33380  nsgqusf1olem2  33382  unitpidl1  33392  elrspunsn  33397  ssdifidllem  33424  mxidlirredi  33439  mxidlirred  33440  opprqusplusg  33457  opprqus0g  33458  opprqusmulr  33459  idlsrgmulrss1  33479  idlsrgmulrss2  33480  rprmcl  33486  rprmdvds  33487  rprmnz  33488  rprmnunit  33489  rprmasso  33493  rprmirredb  33500  pidufd  33511  1arithufdlem2  33513  1arithufdlem3  33514  zringfrac  33522  ply1dg3rt0irred  33547  m1pmeq  33548  ig1pmindeg  33562  exsslsb  33587  ply1degltdimlem  33613  lindsun  33616  fldextfld1  33640  fldextfld2  33641  rtelextdg2  33712  1smat1  33778  submateqlem2  33782  lmatfval  33788  mdetlap1  33800  madjusmdetlem1  33801  madjusmdetlem2  33802  madjusmdetlem3  33803  madjusmdetlem4  33804  zarclssn  33847  zartopn  33849  zarmxt1  33854  rhmpreimacnlem  33858  rhmpreimacn  33859  pnfneige0  33925  pl1cn  33929  rrhqima  33990  esumfzf  34045  esumpcvgval  34054  esumpmono  34055  esumcvg  34062  ldgenpisyslem1  34139  ldgenpisys  34142  measbase  34173  dya2iocnei  34259  oddpwdc  34331  eulerpartlems  34337  eulerpartlemb  34345  sseqf  34369  fibp1  34378  orrvcval4  34442  orrvcoel  34443  orrvccel  34444  ballotlem2  34466  ballotlemfrceq  34506  signsplypnf  34540  signswch  34551  signstf0  34558  signstfvn  34559  signstfvneq0  34562  signstfvcl  34563  signstfveq0  34567  signsvfn  34572  fct2relem  34587  fsum2dsub  34597  reprsuc  34605  reprpmtf1o  34616  breprexplema  34620  breprexplemc  34622  hgt749d  34639  hgt750lemb  34646  tgoldbachgnn  34649  bnj1172  34990  bnj1245  35003  bnj1311  35013  bnj1450  35039  bnj1501  35056  subfacp1lem1  35159  subfacp1lem5  35164  subfacp1lem6  35165  subfacval2  35167  erdszelem7  35177  cvxpconn  35222  cvxsconn  35223  cvmliftlem5  35269  cvmliftlem7  35271  cvmliftlem10  35274  cvmliftlem13  35276  mrsubvrs  35502  msubrn  35509  msubco  35511  msubvrs  35540  r1peuqusdeg1  35623  imageval  35906  fwddifnp1  36141  knoppcnlem8  36476  knoppcnlem10  36478  bj-unirel  37027  icoreunrn  37335  istoprelowl  37336  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  poimirlem28  37630  poimirlem29  37631  poimirlem31  37633  mblfinlem2  37640  ftc1cnnc  37674  upixp  37711  sdclem2  37724  caushft  37743  ismtyres  37790  rrnmet  37811  rrndstprj1  37812  rrndstprj2  37813  rrncmslem  37814  rrnequiv  37817  iccbnd  37822  osumcllem7N  39939  pexmidlem4N  39950  lcfrlem4  41522  lcfrlem5  41523  lcfrlem6  41524  lcfrlem16  41535  lcfrlem38  41557  mapdrvallem2  41622  mapdh8ab  41754  mapdh8ad  41756  mapdh8e  41761  3factsumint3  41999  aks4d1p1p1  42039  fldhmf1  42066  aks6d1c1p2  42085  aks6d1c1p3  42086  aks6d1c1p7  42089  aks6d1c1p6  42090  aks6d1c1p8  42091  aks6d1c1  42092  evl1gprodd  42093  idomnnzpownz  42108  aks6d1c5lem1  42112  aks6d1c5lem3  42113  aks6d1c5lem2  42114  deg1gprod  42116  sticksstones10  42131  aks6d1c6lem3  42148  aks5lem2  42163  aks5lem3a  42165  unitscyglem5  42175  metakunt20  42200  fz1sump1  42323  sumcubes  42326  evlselv  42576  mhphf2  42587  prjspnfv01  42613  prjspner01  42614  prjspner1  42615  mapfzcons  42705  diophren  42802  irrapxlem1  42811  monotuz  42931  acongeq  42973  jm2.26lem3  42991  jm3.1lem2  43008  pw2f1ocnv  43027  idomodle  43181  trclfvdecomr  43718  imo72b2lem0  44155  imo72b2lem1  44159  scottelrankd  44238  dvgrat  44303  cvgdvgrat  44304  hashnzfz2  44312  fcnre  45002  refsumcn  45007  rfcnnnub  45013  disjf1o  45168  disjinfi  45169  ssmapsn  45193  ssuzfz  45332  nnsplit  45341  uzssd2  45400  uzublem  45413  fsumsermpt  45566  climsuselem1  45594  limcperiod  45615  sumnnodd  45617  lptioo2cn  45632  lptioo1cn  45633  climresmpt  45646  allbutfifvre  45662  climleltrp  45663  cnrefiisplem  45816  cncfshift  45861  cncfperiod  45866  cncfshiftioo  45879  fperdvper  45906  dvnmptdivc  45925  dvnmul  45930  dvmptfprod  45932  dvnprodlem3  45935  stoweidlem11  45998  stoweidlem15  46002  stoweidlem17  46004  stoweidlem20  46007  stoweidlem34  46021  stoweidlem35  46022  stoweidlem46  46033  stoweidlem47  46034  stoweidlem56  46043  stoweidlem59  46046  stoweidlem62  46049  stirlinglem5  46065  stirlinglem14  46074  dirkertrigeqlem2  46086  dirkertrigeqlem3  46087  fourierdlem11  46105  fourierdlem15  46109  fourierdlem16  46110  fourierdlem21  46115  fourierdlem22  46116  fourierdlem25  46119  fourierdlem48  46141  fourierdlem52  46145  fourierdlem54  46147  fourierdlem58  46151  fourierdlem62  46155  fourierdlem64  46157  fourierdlem65  46158  fourierdlem69  46162  fourierdlem70  46163  fourierdlem71  46164  fourierdlem73  46166  fourierdlem80  46173  fourierdlem81  46174  fourierdlem83  46176  fourierdlem92  46185  fourierdlem93  46186  fourierdlem97  46190  fourierdlem103  46196  fourierdlem104  46197  fourierdlem112  46205  fourierdlem113  46206  fouriercnp  46213  fouriersw  46218  elaa2lem  46220  etransclem4  46225  etransclem7  46228  etransclem10  46231  etransclem14  46235  etransclem15  46236  etransclem24  46245  etransclem25  46246  etransclem31  46252  etransclem32  46253  etransclem35  46256  etransclem44  46265  etransclem46  46267  qndenserrnopnlem  46284  qndenserrn  46286  prsal  46305  salgencntex  46330  subsaliuncl  46345  subsalsal  46346  sge0tsms  46367  sge0fodjrnlem  46403  sge0isum  46414  iundjiunlem  46446  iundjiun  46447  meadjiunlem  46452  meaiunlelem  46455  meaiuninclem  46467  meaiininc2  46475  caragensplit  46487  carageneld  46489  carageniuncllem1  46508  caratheodorylem1  46513  caratheodorylem2  46514  hoicvr  46535  hsphoidmvle2  46572  hsphoidmvle  46573  hoidmv1lelem2  46579  hoidmv1lelem3  46580  hoidmvlelem2  46583  hoiqssbllem2  46610  pimdecfgtioc  46702  pimincfltioc  46703  pimdecfgtioo  46704  pimincfltioo  46705  smflimlem3  46760  smfmullem4  46781  smfsupxr  46803  smflimsuplem2  46808  smflimsuplem5  46811  ormklocald  46861  natlocalincr  46863  elmod2  47330  isuspgrim0lem  47844  ssnn0ssfz  48238  zlmodzxzscm  48246  rmsupp0  48257  lincsum  48319  lincscm  48320  lindslinindimp2lem4  48351  lincresunit3  48371  elbigofrcl  48444  intubeu  48865  unilbeu  48866  cicrcl2  48917  cic1st2nd  48921  elxpcbasex1ALT  49000  elxpcbasex2ALT  49002  swapf1a  49020  swapf2f1oa  49028  swapfida  49031  cofuswapf1  49039  cofuswapf2  49040  postc  49261  setrec1  49305  aacllem  49415