MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleqtrdi Structured version   Visualization version   GIF version

Theorem eleqtrdi 2848
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
StepHypRef Expression
1 eleqtrdi.1 . 2 (𝜑𝐴𝐵)
2 eleqtrdi.2 . . 3 𝐵 = 𝐶
32a1i 11 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrd 2840 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815
This theorem is referenced by:  eleqtrrdi  2849  3eltr3g  2854  prid2g  4727  ndmfvrcl  6883  fnwelem  8068  tz7.48-1  8394  brwitnlem  8458  oeeulem  8553  dffi3  9374  cnfcom3lem  9646  ttrclse  9670  alephgeom  10025  fpwwe2lem5  10578  canthwelem  10593  hargch  10616  r1wunlim  10680  eluzel2  12775  fseq1p1m1  13522  fznn0sub2  13555  nn0split  13563  seqp1d  13930  exple1  14088  digit1  14147  bcval5  14225  bcpasc  14228  hashf1  14363  seqcoll  14370  seqcoll2  14371  ccatrn  14484  swrdccat2  14564  cats1un  14616  pfxccatin12lem3  14627  splfv2a  14651  splval2  14652  caubnd  15250  limsupgre  15370  clim2ser  15546  clim2ser2  15547  iserex  15548  isermulc2  15549  iserle  15551  iserge0  15552  climub  15553  climserle  15554  isercolllem2  15557  isercolllem3  15558  isercoll  15559  isercoll2  15560  serf0  15572  iseraltlem2  15574  iseraltlem3  15575  iseralt  15576  sumeq2ii  15585  summolem3  15606  summolem2a  15607  fsum  15612  sum0  15613  fsumcl2lem  15623  fsumadd  15632  isumclim3  15651  isumadd  15659  fsump1i  15661  fsummulc2  15676  fsumrelem  15699  iserabs  15707  cvgcmp  15708  cvgcmpub  15709  cvgcmpce  15710  binom1dif  15725  isumshft  15731  isumsplit  15732  isumrpcl  15735  isumsup2  15738  climcndslem1  15741  climcndslem2  15742  climcnds  15743  arisum2  15753  trireciplem  15754  geoser  15759  pwdif  15760  geolim  15762  geo2lim  15767  cvgrat  15775  mertenslem1  15776  mertenslem2  15777  mertens  15778  clim2prod  15780  clim2div  15781  ntrivcvgfvn0  15791  ntrivcvgtail  15792  prodeq2ii  15803  prodmolem3  15823  prodmolem2a  15824  fprod  15831  fprodntriv  15832  fprodss  15838  fprodser  15839  fprodcl2lem  15840  fprodmul  15850  fproddiv  15851  fprodabs  15864  fprodeq0  15865  fprodn0  15869  iprodclim3  15890  iprodmul  15893  fallfacfwd  15926  0fallfac  15927  binomfallfaclem2  15930  fallfacval4  15933  bpolysum  15943  bpolydiflem  15944  fsumkthpow  15946  efcvgfsum  15975  efcj  15981  fprodefsum  15984  effsumlt  16000  ruclem7  16125  bitsfzolem  16321  bitsfzo  16322  bitsfi  16324  bitsinv1lem  16328  bitsinv1  16329  bitsinvp1  16336  sadcp1  16342  sadadd  16354  sadass  16358  bitsres  16360  smupp1  16367  smuval2  16369  smupval  16375  smueqlem  16377  smumul  16380  algrp1  16457  phiprmpw  16655  crth  16657  phimullem  16658  eulerthlem2  16661  prmdiv  16664  pcpremul  16722  pcmpt  16771  pcfac  16778  pockthlem  16784  pockthg  16785  prmreclem2  16796  prmreclem3  16797  prmreclem4  16798  prmreclem5  16799  prmreclem6  16800  prmrec  16801  1arith  16806  vdwapun  16853  vdwlem1  16860  vdwlem2  16861  vdwlem3  16862  vdwlem6  16865  vdwlem8  16867  vdwlem10  16869  vdw  16873  imasvscafn  17426  oppccatid  17608  oppccomfpropd  17616  brcic  17688  funcoppc  17768  invfuc  17870  hofcl  18155  yonedalem4c  18173  gsumwsubmcl  18654  gsumsgrpccat  18657  gsumwmhm  18662  mulgnnp1  18891  mulgnnsubcl  18895  mulgnn0z  18910  mulgnndir  18912  psgnunilem4  19286  psgnran  19304  sylow1lem1  19387  lsmmod2  19465  lsmdisj2r  19474  efginvrel2  19516  efgsdmi  19521  efgsrel  19523  efgs1b  19525  efgsp1  19526  efgredleme  19532  efgredlemc  19534  efgcpbllemb  19544  frgpuplem  19561  mulgnn0di  19611  frgpnabllem1  19658  lt6abl  19679  cycsubgcyg  19685  gsumval3eu  19688  gsumval3  19691  gsumzcl2  19694  gsumzaddlem  19705  gsumconst  19718  gsumzmhm  19721  gsumzoppg  19728  telgsumfz0s  19775  dprdwd  19797  dprd2da  19828  pgpfaclem1  19867  srgbinom  19969  isirred  20137  lspprid2  20475  lspsnat  20622  lsppratlem1  20624  lsppratlem3  20626  lidl0cl  20698  lidlacl  20699  lidlnegcl  20700  lidlmcl  20703  psgnghm  21000  frlmvscavalb  21192  frlmvplusgscavalb  21193  psrbaglefi  21350  psrbaglefiOLD  21351  psrass23l  21393  psrass23  21395  mplcoe5lem  21456  mpfind  21533  selvval  21544  mhpvscacl  21560  psr1bascl  21587  ply1basf  21589  gsummoncoe1  21691  lply1binom  21693  lply1binomsc  21694  mpfpf1  21733  pf1mpf  21734  evl1scvarpw  21745  matbas2i  21787  matecld  21791  matgsum  21802  mpomatmul  21811  dmatmul  21862  1mavmul  21913  mdetleib2  21953  m1detdiag  21962  marep01ma  22025  smadiadetlem4  22034  slesolinv  22045  pmatcollpw3fi1lem1  22151  chpscmat  22207  chpscmatgsumbin  22209  chp0mat  22211  chpidmat  22212  chfacfisf  22219  chfacfisfcpmat  22220  chfacfpmmulgsum2  22230  cldrcl  22393  ordtbas  22559  iscnp2  22606  dis1stc  22866  ptbasfi  22948  ptpjopn  22979  ptclsg  22982  ptcnp  22989  kqtop  23112  reghmph  23160  ptcmplem2  23420  ptcmplem3  23421  ptcmplem4  23422  tsmslem1  23496  utop2nei  23618  isucn2  23647  cuspcvg  23669  cnextucn  23671  imasdsf1olem  23742  blcvx  24177  xrhmeo  24325  cnrehmeo  24332  evth  24338  reparphti  24376  iscau4  24659  iscmet3lem1  24671  lmle  24681  rrxfsupp  24782  rrxdsfi  24791  pjthlem2  24818  ovollb2lem  24868  ovolunlem1a  24876  ovoliunlem1  24882  ovoliun2  24886  ovolscalem1  24893  ovolicc1  24896  ovolicc2lem4  24900  iundisj2  24929  voliunlem1  24930  volsup  24936  ioombl1lem4  24941  uniioovol  24959  uniioombllem3  24965  uniioombllem4  24966  uniioombllem6  24968  vitalilem5  24992  mbfimaopnlem  25035  mbflimsup  25046  mbfi1fseqlem3  25098  iblitg  25149  dvnp1  25305  cpncn  25316  dvlip2  25375  dvfsumlem2  25407  dvfsumlem3  25408  dvfsumrlimge0  25410  dvfsumrlim2  25412  ftc1cn  25423  elplyd  25579  ply1termlem  25580  ply1term  25581  ply0  25585  plyeq0lem  25587  plyaddlem1  25590  plymullem1  25591  plyaddlem  25592  plymullem  25593  coeeulem  25601  plyco  25618  coeeq2  25619  coefv0  25625  coemulhi  25631  coemulc  25632  plycj  25654  dvply1  25660  vieta1lem2  25687  elqaalem2  25696  dvtaylp  25745  dvntaylp  25746  taylthlem1  25748  taylth  25750  ulmres  25763  ulmshftlem  25764  ulmshft  25765  ulmcau  25770  ulmdvlem1  25775  mtest  25779  mtestbdd  25780  pserulm  25797  psercn2  25798  psercnlem1  25800  psercn  25801  pserdvlem2  25803  abelthlem6  25811  abelth  25816  efif1olem1  25914  efif1olem3  25916  efif1olem4  25917  logcn  26018  advlogexp  26026  efopn  26029  cxpeq  26126  asinsin  26258  atantayl  26303  leibpilem2  26307  birthdaylem2  26318  birthdaylem3  26319  efrlim  26335  emcllem2  26362  emcllem5  26365  emcllem7  26367  harmonicbnd4  26376  fsumharmonic  26377  lgamgulm2  26401  lgamcvglem  26405  lgamcvg2  26420  gamcvg2lem  26424  wilthlem2  26434  wilthlem3  26435  ftalem1  26438  ftalem2  26439  ftalem3  26440  ftalem5  26442  basellem2  26447  basellem3  26448  basellem5  26450  basellem8  26453  ppiprm  26516  ppinprm  26517  chtprm  26518  chtnprm  26519  chpp1  26520  vma1  26531  ppiltx  26542  musum  26556  0sgmppw  26562  1sgmprm  26563  ppiublem2  26567  chtublem  26575  fsumvma2  26578  chpchtsum  26583  logexprlim  26589  bposlem5  26652  lgscllem  26668  lgsval2lem  26671  lgsval4a  26683  lgsneg  26685  lgsdir2lem3  26691  lgsdir2lem5  26693  lgsdir  26696  lgsdilem2  26697  lgsdi  26698  lgsne0  26699  gausslemma2dlem3  26732  lgseisenlem1  26739  lgsquadlem2  26745  chebbnd1lem1  26833  chtppilimlem1  26837  rplogsumlem2  26849  rpvmasumlem  26851  dchrisumlem1  26853  dchrisumlem2  26854  dchrmusum2  26858  dchrvmasum2lem  26860  dchrvmasumiflem1  26865  dchrisum0flblem1  26872  dchrisum0flblem2  26873  dchrisum0flb  26874  dchrisum0re  26877  dchrisum0lem1b  26879  dchrisum0lem1  26880  dchrisum0lem2a  26881  dchrisum0lem2  26882  dchrisum0lem3  26883  mudivsum  26894  mulogsum  26896  mulog2sumlem2  26899  selberg2lem  26914  logdivbnd  26920  pntrsumo1  26929  pntrsumbnd2  26931  pntrlog2bndlem2  26942  pntrlog2bndlem4  26944  pntrlog2bndlem6a  26946  pntlemj  26967  pntlemf  26969  ostth2lem3  26999  madebdayim  27239  oldbdayim  27240  tglngne  27534  ltgseg  27580  eedimeq  27889  axlowdimlem16  27948  ebtwntg  27973  subgruhgredgd  28274  subumgredg2  28275  umgrres1lem  28300  wlkson  28646  wksonproplem  28694  wksonproplemOLD  28695  trlsonfval  28696  pthsonfval  28730  spthson  28731  crctcshwlkn0lem4  28800  crctcshwlkn0lem5  28801  eupth2lems  29224  numclwwlk1lem2foa  29340  numclwlk1lem2  29356  numclwwlk2lem1  29362  htthlem  29901  hhsscms  30262  shmodsi  30373  pjoc1i  30415  5oalem1  30638  mayete3i  30712  adj1  30917  iundisj2f  31550  fmptco1f1o  31589  fcnvgreu  31631  suppovss  31640  ssnnssfz  31732  iundisj2fi  31742  cshw1s2  31856  gsumhashmul  31940  pmtrto1cl  31990  psgnfzto1stlem  31991  fzto1st1  31993  cycpmfv1  32004  cycpmfv2  32005  cycpmco2rn  32016  cycpmco2lem4  32020  cycpmco2lem5  32021  cycpmco2lem6  32022  cyc3evpm  32041  cyc3genpm  32043  cycpmconjslem2  32046  cyc3conja  32048  rspsnel  32200  nsgmgc  32230  nsgqusf1olem2  32232  ghmquskerlem1  32235  ghmquskerco  32236  idlsrgmulrss1  32293  idlsrgmulrss2  32294  lindsun  32360  fldextfld1  32378  fldextfld2  32379  1smat1  32425  submateqlem2  32429  lmatfval  32435  mdetlap1  32447  madjusmdetlem1  32448  madjusmdetlem2  32449  madjusmdetlem3  32450  madjusmdetlem4  32451  zarclssn  32494  zartopn  32496  zarmxt1  32501  rhmpreimacnlem  32505  rhmpreimacn  32506  pnfneige0  32572  pl1cn  32576  rrhqima  32635  indpreima  32664  esumfzf  32708  esumpcvgval  32717  esumpmono  32718  esumcvg  32725  ldgenpisyslem1  32802  ldgenpisys  32805  measbase  32836  dya2iocnei  32922  oddpwdc  32994  eulerpartlems  33000  eulerpartlemb  33008  sseqf  33032  fibp1  33041  orrvcval4  33104  orrvcoel  33105  orrvccel  33106  ballotlem2  33128  ballotlemfrceq  33168  signsplypnf  33202  signswch  33213  signstf0  33220  signstfvn  33221  signstfvneq0  33224  signstfvcl  33225  signstfveq0  33229  signsvfn  33234  fct2relem  33250  fsum2dsub  33260  reprsuc  33268  reprpmtf1o  33279  breprexplema  33283  breprexplemc  33285  hgt749d  33302  hgt750lemb  33309  tgoldbachgnn  33312  bnj1172  33653  bnj1245  33666  bnj1311  33676  bnj1450  33702  bnj1501  33719  subfacp1lem1  33813  subfacp1lem5  33818  subfacp1lem6  33819  subfacval2  33821  erdszelem7  33831  cvxsconn  33877  cvmliftlem5  33923  cvmliftlem7  33925  cvmliftlem10  33928  cvmliftlem13  33930  mrsubvrs  34156  msubrn  34163  msubco  34165  msubvrs  34194  imageval  34544  fwddifnp1  34779  knoppcnlem8  34992  knoppcnlem10  34994  bj-unirel  35551  icoreunrn  35859  istoprelowl  35860  poimirlem3  36110  poimirlem4  36111  poimirlem6  36113  poimirlem7  36114  poimirlem8  36115  poimirlem12  36119  poimirlem15  36122  poimirlem16  36123  poimirlem17  36124  poimirlem18  36125  poimirlem19  36126  poimirlem20  36127  poimirlem21  36128  poimirlem22  36129  poimirlem23  36130  poimirlem24  36131  poimirlem25  36132  poimirlem26  36133  poimirlem27  36134  poimirlem28  36135  poimirlem29  36136  poimirlem31  36138  mblfinlem2  36145  ftc1cnnc  36179  upixp  36217  sdclem2  36230  caushft  36249  ismtyres  36296  rrnmet  36317  rrndstprj1  36318  rrndstprj2  36319  rrncmslem  36320  rrnequiv  36323  iccbnd  36328  osumcllem7N  38454  pexmidlem4N  38465  lcfrlem4  40037  lcfrlem5  40038  lcfrlem6  40039  lcfrlem16  40050  lcfrlem38  40072  mapdrvallem2  40137  mapdh8ab  40269  mapdh8ad  40271  mapdh8e  40276  3factsumint3  40509  aks4d1p1p1  40549  fldhmf1  40576  sticksstones10  40592  metakunt20  40625  mhphf2  40801  prjspnfv01  40991  prjspner01  40992  prjspner1  40993  mapfzcons  41068  diophren  41165  irrapxlem1  41174  monotuz  41294  acongeq  41336  jm2.26lem3  41354  jm3.1lem2  41371  pw2f1ocnv  41390  idomodle  41552  trclfvdecomr  42074  imo72b2lem1  42516  scottelrankd  42601  dvgrat  42666  cvgdvgrat  42667  hashnzfz2  42675  fcnre  43304  refsumcn  43309  rfcnnnub  43315  disjf1o  43484  disjinfi  43486  ssmapsn  43511  ssuzfz  43657  nnsplit  43666  uzssd2  43726  uzublem  43739  fsumsermpt  43894  climsuselem1  43922  limcperiod  43943  sumnnodd  43945  lptioo2cn  43960  lptioo1cn  43961  climresmpt  43974  allbutfifvre  43990  climleltrp  43991  cnrefiisplem  44144  cncfshift  44189  cncfperiod  44194  cncfshiftioo  44207  fperdvper  44234  dvnmptdivc  44253  dvnmul  44258  dvmptfprod  44260  dvnprodlem3  44263  stoweidlem11  44326  stoweidlem15  44330  stoweidlem17  44332  stoweidlem20  44335  stoweidlem34  44349  stoweidlem35  44350  stoweidlem46  44361  stoweidlem47  44362  stoweidlem56  44371  stoweidlem59  44374  stoweidlem62  44377  stirlinglem5  44393  stirlinglem14  44402  dirkertrigeqlem2  44414  dirkertrigeqlem3  44415  fourierdlem11  44433  fourierdlem15  44437  fourierdlem16  44438  fourierdlem21  44443  fourierdlem22  44444  fourierdlem25  44447  fourierdlem48  44469  fourierdlem52  44473  fourierdlem54  44475  fourierdlem58  44479  fourierdlem62  44483  fourierdlem64  44485  fourierdlem65  44486  fourierdlem69  44490  fourierdlem70  44491  fourierdlem71  44492  fourierdlem73  44494  fourierdlem80  44501  fourierdlem81  44502  fourierdlem83  44504  fourierdlem92  44513  fourierdlem93  44514  fourierdlem97  44518  fourierdlem103  44524  fourierdlem104  44525  fourierdlem112  44533  fourierdlem113  44534  fouriercnp  44541  fouriersw  44546  elaa2lem  44548  etransclem4  44553  etransclem7  44556  etransclem10  44559  etransclem14  44563  etransclem15  44564  etransclem24  44573  etransclem25  44574  etransclem31  44580  etransclem32  44581  etransclem35  44584  etransclem44  44593  etransclem46  44595  qndenserrnopnlem  44612  qndenserrn  44614  prsal  44633  salgencntex  44658  subsaliuncl  44673  subsalsal  44674  sge0tsms  44695  sge0fodjrnlem  44731  sge0isum  44742  iundjiunlem  44774  iundjiun  44775  meadjiunlem  44780  meaiunlelem  44783  meaiuninclem  44795  meaiininc2  44803  caragensplit  44815  carageneld  44817  carageniuncllem1  44836  caratheodorylem1  44841  caratheodorylem2  44842  hoicvr  44863  hsphoidmvle2  44900  hsphoidmvle  44901  hoidmv1lelem2  44907  hoidmv1lelem3  44908  hoidmvlelem2  44911  hoiqssbllem2  44938  pimdecfgtioc  45030  pimincfltioc  45031  pimdecfgtioo  45032  pimincfltioo  45033  smflimlem3  45088  smfmullem4  45109  smfsupxr  45131  smflimsuplem2  45136  smflimsuplem5  45139  natlocalincr  45189  elmod2  45636  ssnn0ssfz  46499  zlmodzxzscm  46507  rmsupp0  46518  lincsum  46584  lincscm  46585  lindslinindimp2lem4  46616  lincresunit3  46636  elbigofrcl  46710  intubeu  47083  unilbeu  47084  postc  47176  setrec1  47210  aacllem  47322
  Copyright terms: Public domain W3C validator