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

Theorem eleqtrdi 2921
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 2913 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
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 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2813  df-clel 2891
This theorem is referenced by:  eleqtrrdi  2922  3eltr3g  2927  prid2g  4673  ndmfvrcl  6677  fnwelem  7803  tz7.48-1  8057  brwitnlem  8110  oeeulem  8205  dffi3  8873  cnfcom3lem  9144  alephgeom  9486  fpwwe2lem6  10035  canthwelem  10050  hargch  10073  r1wunlim  10137  eluzel2  12227  fseq1p1m1  12965  fznn0sub2  12998  nn0split  13006  seqp1d  13370  exple1  13525  digit1  13583  bcval5  13663  bcpasc  13666  hashf1  13800  seqcoll  13807  seqcoll2  13808  ccatrn  13923  swrdccat2  14011  cats1un  14063  pfxccatin12lem3  14074  splfv2a  14098  splval2  14099  caubnd  14698  limsupgre  14818  clim2ser  14991  clim2ser2  14992  iserex  14993  isermulc2  14994  iserle  14996  iserge0  14997  climub  14998  climserle  14999  isercolllem2  15002  isercolllem3  15003  isercoll  15004  isercoll2  15005  serf0  15017  iseraltlem2  15019  iseraltlem3  15020  iseralt  15021  sumeq2ii  15030  summolem3  15051  summolem2a  15052  fsum  15057  sum0  15058  fsumcl2lem  15068  fsumadd  15076  isumclim3  15094  isumadd  15102  fsump1i  15104  fsummulc2  15119  fsumrelem  15142  iserabs  15150  cvgcmp  15151  cvgcmpub  15152  cvgcmpce  15153  binom1dif  15168  isumshft  15174  isumsplit  15175  isumrpcl  15178  isumsup2  15181  climcndslem1  15184  climcndslem2  15185  climcnds  15186  arisum2  15196  trireciplem  15197  geoser  15202  pwdif  15203  geolim  15206  geo2lim  15211  cvgrat  15219  mertenslem1  15220  mertenslem2  15221  mertens  15222  clim2prod  15224  clim2div  15225  ntrivcvgfvn0  15235  ntrivcvgtail  15236  prodeq2ii  15247  prodmolem3  15267  prodmolem2a  15268  fprod  15275  fprodntriv  15276  fprodss  15282  fprodser  15283  fprodcl2lem  15284  fprodmul  15294  fproddiv  15295  fprodabs  15308  fprodeq0  15309  fprodn0  15313  iprodclim3  15334  iprodmul  15337  fallfacfwd  15370  0fallfac  15371  binomfallfaclem2  15374  fallfacval4  15377  bpolysum  15387  bpolydiflem  15388  fsumkthpow  15390  efcvgfsum  15419  efcj  15425  fprodefsum  15428  effsumlt  15444  ruclem7  15569  bitsfzolem  15761  bitsfzo  15762  bitsfi  15764  bitsinv1lem  15768  bitsinv1  15769  bitsinvp1  15776  sadcp1  15782  sadadd  15794  sadass  15798  bitsres  15800  smupp1  15807  smuval2  15809  smupval  15815  smueqlem  15817  smumul  15820  algrp1  15896  phiprmpw  16091  crth  16093  phimullem  16094  eulerthlem2  16097  prmdiv  16100  pcpremul  16158  pcmpt  16206  pcfac  16213  pockthlem  16219  pockthg  16220  prmreclem2  16231  prmreclem3  16232  prmreclem4  16233  prmreclem5  16234  prmreclem6  16235  prmrec  16236  1arith  16241  vdwapun  16288  vdwlem1  16295  vdwlem2  16296  vdwlem3  16297  vdwlem6  16300  vdwlem8  16302  vdwlem10  16304  vdw  16308  imasvscafn  16789  oppccatid  16968  oppccomfpropd  16976  brcic  17047  funcoppc  17124  invfuc  17223  hofcl  17488  yonedalem4c  17506  gsumwsubmcl  17980  gsumsgrpccat  17983  gsumccatOLD  17984  gsumwmhm  17989  mulgnnp1  18215  mulgnnsubcl  18219  mulgnn0z  18233  mulgnndir  18235  psgnunilem4  18604  psgnran  18622  sylow1lem1  18702  lsmmod2  18781  lsmdisj2r  18790  efginvrel2  18832  efgsdmi  18837  efgsrel  18839  efgs1b  18841  efgsp1  18842  efgredleme  18848  efgredlemc  18850  efgcpbllemb  18860  frgpuplem  18877  mulgnn0di  18925  frgpnabllem1  18972  lt6abl  18994  cycsubgcyg  19000  gsumval3eu  19003  gsumval3  19006  gsumzcl2  19009  gsumzaddlem  19020  gsumconst  19033  gsumzmhm  19036  gsumzoppg  19043  telgsumfz0s  19090  dprdwd  19112  dprd2da  19143  pgpfaclem1  19182  srgbinom  19274  isirred  19428  lspprid2  19746  lspsnat  19893  lsppratlem1  19895  lsppratlem3  19897  lidl0cl  19961  lidlacl  19962  lidlnegcl  19963  lidlmcl  19966  psrbaglefi  20128  psrass23l  20164  psrass23  20166  mplcoe5lem  20224  mpfind  20296  selvval  20307  mhpinvcl  20315  mhpvscacl  20317  psr1bascl  20344  ply1basf  20346  gsummoncoe1  20448  lply1binom  20450  lply1binomsc  20451  mpfpf1  20490  pf1mpf  20491  evl1scvarpw  20502  psgnghm  20700  frlmvscavalb  20890  frlmvplusgscavalb  20891  matbas2i  21007  matecld  21011  matgsum  21022  mpomatmul  21031  dmatmul  21082  1mavmul  21133  mdetleib2  21173  m1detdiag  21182  marep01ma  21245  smadiadetlem4  21254  slesolinv  21265  pmatcollpw3fi1lem1  21370  chpscmat  21426  chpscmatgsumbin  21428  chp0mat  21430  chpidmat  21431  chfacfisf  21438  chfacfisfcpmat  21439  chfacfpmmulgsum2  21449  cldrcl  21610  ordtbas  21776  iscnp2  21823  dis1stc  22083  ptbasfi  22165  ptpjopn  22196  ptclsg  22199  ptcnp  22206  kqtop  22329  reghmph  22377  ptcmplem2  22637  ptcmplem3  22638  ptcmplem4  22639  tsmslem1  22713  utop2nei  22835  isucn2  22864  cuspcvg  22886  cnextucn  22888  imasdsf1olem  22959  blcvx  23382  xrhmeo  23530  cnrehmeo  23537  evth  23543  reparphti  23581  iscau4  23862  iscmet3lem1  23874  lmle  23884  rrxfsupp  23985  rrxdsfi  23994  pjthlem2  24021  ovollb2lem  24071  ovolunlem1a  24079  ovoliunlem1  24085  ovoliun2  24089  ovolscalem1  24096  ovolicc1  24099  ovolicc2lem4  24103  iundisj2  24132  voliunlem1  24133  volsup  24139  ioombl1lem4  24144  uniioovol  24162  uniioombllem3  24168  uniioombllem4  24169  uniioombllem6  24171  vitalilem5  24195  mbfimaopnlem  24238  mbflimsup  24249  mbfi1fseqlem3  24300  iblitg  24351  dvnp1  24507  cpncn  24518  dvlip2  24577  dvfsumlem2  24609  dvfsumlem3  24610  dvfsumrlimge0  24612  dvfsumrlim2  24614  ftc1cn  24625  elplyd  24778  ply1termlem  24779  ply1term  24780  ply0  24784  plyeq0lem  24786  plyaddlem1  24789  plymullem1  24790  plyaddlem  24791  plymullem  24792  coeeulem  24800  plyco  24817  coeeq2  24818  coefv0  24824  coemulhi  24830  coemulc  24831  plycj  24853  dvply1  24859  vieta1lem2  24886  elqaalem2  24895  dvtaylp  24944  dvntaylp  24945  taylthlem1  24947  taylth  24949  ulmres  24962  ulmshftlem  24963  ulmshft  24964  ulmcau  24969  ulmdvlem1  24974  mtest  24978  mtestbdd  24979  pserulm  24996  psercn2  24997  psercnlem1  24999  psercn  25000  pserdvlem2  25002  abelthlem6  25010  abelth  25015  efif1olem1  25113  efif1olem3  25115  efif1olem4  25116  logcn  25217  advlogexp  25225  efopn  25228  cxpeq  25325  asinsin  25457  atantayl  25502  leibpilem2  25506  birthdaylem2  25517  birthdaylem3  25518  efrlim  25534  emcllem2  25561  emcllem5  25564  emcllem7  25566  harmonicbnd4  25575  fsumharmonic  25576  lgamgulm2  25600  lgamcvglem  25604  lgamcvg2  25619  gamcvg2lem  25623  wilthlem2  25633  wilthlem3  25634  ftalem1  25637  ftalem2  25638  ftalem3  25639  ftalem5  25641  basellem2  25646  basellem3  25647  basellem5  25649  basellem8  25652  ppiprm  25715  ppinprm  25716  chtprm  25717  chtnprm  25718  chpp1  25719  vma1  25730  ppiltx  25741  musum  25755  0sgmppw  25761  1sgmprm  25762  ppiublem2  25766  chtublem  25774  fsumvma2  25777  chpchtsum  25782  logexprlim  25788  bposlem5  25851  lgscllem  25867  lgsval2lem  25870  lgsval4a  25882  lgsneg  25884  lgsdir2lem3  25890  lgsdir2lem5  25892  lgsdir  25895  lgsdilem2  25896  lgsdi  25897  lgsne0  25898  gausslemma2dlem3  25931  lgseisenlem1  25938  lgsquadlem2  25944  chebbnd1lem1  26032  chtppilimlem1  26036  rplogsumlem2  26048  rpvmasumlem  26050  dchrisumlem1  26052  dchrisumlem2  26053  dchrmusum2  26057  dchrvmasum2lem  26059  dchrvmasumiflem1  26064  dchrisum0flblem1  26071  dchrisum0flblem2  26072  dchrisum0flb  26073  dchrisum0re  26076  dchrisum0lem1b  26078  dchrisum0lem1  26079  dchrisum0lem2a  26080  dchrisum0lem2  26081  dchrisum0lem3  26082  mudivsum  26093  mulogsum  26095  mulog2sumlem2  26098  selberg2lem  26113  logdivbnd  26119  pntrsumo1  26128  pntrsumbnd2  26130  pntrlog2bndlem2  26141  pntrlog2bndlem4  26143  pntrlog2bndlem6a  26145  pntlemj  26166  pntlemf  26168  ostth2lem3  26198  tglngne  26323  ltgseg  26369  eedimeq  26671  axlowdimlem16  26730  ebtwntg  26755  subgruhgredgd  27053  subumgredg2  27054  umgrres1lem  27079  wlkson  27425  wksonproplem  27473  trlsonfval  27474  pthsonfval  27508  spthson  27509  crctcshwlkn0lem4  27578  crctcshwlkn0lem5  27579  eupth2lems  28002  numclwwlk1lem2foa  28118  numclwlk1lem2  28134  numclwwlk2lem1  28140  htthlem  28679  hhsscms  29040  shmodsi  29151  pjoc1i  29193  5oalem1  29416  mayete3i  29490  adj1  29695  iundisj2f  30327  fmptco1f1o  30365  fcnvgreu  30405  suppovss  30413  ssnnssfz  30497  iundisj2fi  30507  cshw1s2  30621  pmtrto1cl  30749  psgnfzto1stlem  30750  fzto1st1  30752  cycpmfv1  30763  cycpmfv2  30764  cycpmco2rn  30775  cycpmco2lem4  30779  cycpmco2lem5  30780  cycpmco2lem6  30781  cyc3evpm  30800  cyc3genpm  30802  cycpmconjslem2  30805  cyc3conja  30807  rspsnel  30944  lindsun  31032  fldextfld1  31050  fldextfld2  31051  1smat1  31080  submateqlem2  31084  lmatfval  31090  mdetlap1  31102  madjusmdetlem1  31103  madjusmdetlem2  31104  madjusmdetlem3  31105  madjusmdetlem4  31106  pnfneige0  31202  pl1cn  31206  rrhqima  31263  indpreima  31292  esumfzf  31336  esumpcvgval  31345  esumpmono  31346  esumcvg  31353  ldgenpisyslem1  31430  ldgenpisys  31433  measbase  31464  dya2iocnei  31548  oddpwdc  31620  eulerpartlems  31626  eulerpartlemb  31634  sseqf  31658  fibp1  31667  orrvcval4  31730  orrvcoel  31731  orrvccel  31732  ballotlem2  31754  ballotlemfrceq  31794  signsplypnf  31828  signswch  31839  signstf0  31846  signstfvn  31847  signstfvneq0  31850  signstfvcl  31851  signstfveq0  31855  signsvfn  31860  fct2relem  31876  fsum2dsub  31886  reprsuc  31894  reprpmtf1o  31905  breprexplema  31909  breprexplemc  31911  hgt749d  31928  hgt750lemb  31935  tgoldbachgnn  31938  bnj1172  32281  bnj1245  32294  bnj1311  32304  bnj1450  32330  bnj1501  32347  subfacp1lem1  32434  subfacp1lem5  32439  subfacp1lem6  32440  subfacval2  32442  erdszelem7  32452  cvxsconn  32498  cvmliftlem5  32544  cvmliftlem7  32546  cvmliftlem10  32549  cvmliftlem13  32551  mrsubvrs  32777  msubrn  32784  msubco  32786  msubvrs  32815  imageval  33399  fwddifnp1  33634  knoppcnlem8  33847  knoppcnlem10  33849  bj-unirel  34361  icoreunrn  34657  istoprelowl  34658  poimirlem3  34936  poimirlem4  34937  poimirlem6  34939  poimirlem7  34940  poimirlem8  34941  poimirlem12  34945  poimirlem15  34948  poimirlem16  34949  poimirlem17  34950  poimirlem18  34951  poimirlem19  34952  poimirlem20  34953  poimirlem21  34954  poimirlem22  34955  poimirlem23  34956  poimirlem24  34957  poimirlem25  34958  poimirlem26  34959  poimirlem27  34960  poimirlem28  34961  poimirlem29  34962  poimirlem31  34964  mblfinlem2  34971  ftc1cnnc  35005  upixp  35043  sdclem2  35056  caushft  35075  ismtyres  35122  rrnmet  35143  rrndstprj1  35144  rrndstprj2  35145  rrncmslem  35146  rrnequiv  35149  iccbnd  35154  osumcllem7N  37134  pexmidlem4N  37145  lcfrlem4  38717  lcfrlem5  38718  lcfrlem6  38719  lcfrlem16  38730  lcfrlem38  38752  mapdrvallem2  38817  mapdh8ab  38949  mapdh8ad  38951  mapdh8e  38956  3factsumint3  39175  mapfzcons  39450  diophren  39547  irrapxlem1  39556  monotuz  39675  acongeq  39717  jm2.26lem3  39735  jm3.1lem2  39752  pw2f1ocnv  39771  idomodle  39933  trclfvdecomr  40208  imo72b2lem1  40656  scottelrankd  40738  dvgrat  40799  cvgdvgrat  40800  hashnzfz2  40808  fcnre  41437  refsumcn  41442  rfcnnnub  41448  disjf1o  41606  disjinfi  41608  ssmapsn  41633  ssuzfz  41771  nnsplit  41780  uzssd2  41845  uzublem  41858  fsumsermpt  42012  climsuselem1  42040  limcperiod  42061  sumnnodd  42063  lptioo2cn  42078  lptioo1cn  42079  climresmpt  42092  allbutfifvre  42108  climleltrp  42109  cnrefiisplem  42262  cncfshift  42307  cncfperiod  42312  cncfshiftioo  42325  fperdvper  42352  dvnmptdivc  42371  dvnmul  42376  dvmptfprod  42378  dvnprodlem3  42381  stoweidlem11  42444  stoweidlem15  42448  stoweidlem17  42450  stoweidlem20  42453  stoweidlem34  42467  stoweidlem35  42468  stoweidlem46  42479  stoweidlem47  42480  stoweidlem56  42489  stoweidlem59  42492  stoweidlem62  42495  stirlinglem5  42511  stirlinglem14  42520  dirkertrigeqlem2  42532  dirkertrigeqlem3  42533  fourierdlem11  42551  fourierdlem15  42555  fourierdlem16  42556  fourierdlem21  42561  fourierdlem22  42562  fourierdlem25  42565  fourierdlem48  42587  fourierdlem52  42591  fourierdlem54  42593  fourierdlem58  42597  fourierdlem62  42601  fourierdlem64  42603  fourierdlem65  42604  fourierdlem69  42608  fourierdlem70  42609  fourierdlem71  42610  fourierdlem73  42612  fourierdlem80  42619  fourierdlem81  42620  fourierdlem83  42622  fourierdlem92  42631  fourierdlem93  42632  fourierdlem97  42636  fourierdlem103  42642  fourierdlem104  42643  fourierdlem112  42651  fourierdlem113  42652  fouriercnp  42659  fouriersw  42664  elaa2lem  42666  etransclem4  42671  etransclem7  42674  etransclem10  42677  etransclem14  42681  etransclem15  42682  etransclem24  42691  etransclem25  42692  etransclem31  42698  etransclem32  42699  etransclem35  42702  etransclem44  42711  etransclem46  42713  qndenserrnopnlem  42730  qndenserrn  42732  prsal  42751  salgencntex  42774  subsaliuncl  42789  subsalsal  42790  sge0tsms  42810  sge0fodjrnlem  42846  sge0isum  42857  iundjiunlem  42889  iundjiun  42890  meadjiunlem  42895  meaiunlelem  42898  meaiuninclem  42910  meaiininc2  42918  caragensplit  42930  carageneld  42932  carageniuncllem1  42951  caratheodorylem1  42956  caratheodorylem2  42957  hoicvr  42978  hsphoidmvle2  43015  hsphoidmvle  43016  hoidmv1lelem2  43022  hoidmv1lelem3  43023  hoidmvlelem2  43026  hoiqssbllem2  43053  pimdecfgtioc  43141  pimincfltioc  43142  pimdecfgtioo  43143  pimincfltioo  43144  smflimlem3  43197  smfmullem4  43217  smfsupxr  43238  smflimsuplem2  43243  smflimsuplem5  43246  elmod2  43678  ssnn0ssfz  44542  zlmodzxzscm  44550  rmsupp0  44561  lincsum  44629  lincscm  44630  lindslinindimp2lem4  44661  lincresunit3  44681  elbigofrcl  44755  setrec1  44981  aacllem  45089
  Copyright terms: Public domain W3C validator