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

Theorem eleq2i 2679
Description: Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
eleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eleq2i (𝐶𝐴𝐶𝐵)

Proof of Theorem eleq2i
StepHypRef Expression
1 eleq1i.1 . 2 𝐴 = 𝐵
2 eleq2 2676 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  eleq12i  2680  eleqtri  2685  eleq2s  2705  hbxfreq  2716  raleqbii  2972  rexeqbii  3035  rabeq2i  3169  elab2g  3321  elrabf  3328  elrab3t  3329  elrab2  3332  cbvsbc  3430  elin2  3762  elsymdif  3810  dfnul2  3875  noel  3877  eltpg  4173  tpid3gOLD  4248  elunirab  4378  elintrab  4417  disjxiun  4573  disjxiunOLD  4574  exss  4852  elopOLD  4857  otiunsndisj  4896  brabsb  4901  brabga  4904  pofun  4965  elxp  5045  brab2a  5081  opeliunxp  5083  bropaex12  5105  brab2ga  5107  elcnv  5209  elrnmptg  5283  opelres  5309  rninxp  5478  elsuci  5694  elsucg  5695  elsuc2g  5696  elfv  6086  0fv  6122  opabiota  6156  dffv2  6166  fvopab3g  6172  fvmptex  6188  fvopab5  6202  fvn0ssdmfun  6243  fveqressseq  6248  f0cli  6263  fmptco  6288  fvrnressn  6311  funfvima  6374  elunirnALT  6392  fliftel  6437  eloprabga  6623  elrnmpt2  6649  ovid  6653  offval  6779  suceloni  6882  1st2val  7062  2nd2val  7063  bropopvvv  7119  bropfvvvv  7121  fsplit  7146  xporderlem  7152  brtpos2  7222  wfrdmcl  7287  wfrfun  7289  wfrlem12  7290  wfrlem17  7295  wfr2  7298  issmo  7309  smores3  7314  tfrlem7  7343  tfrlem9  7345  tfrlem9a  7346  tfr2b  7356  tfr2  7358  rdgsuc  7384  frsucmptn  7398  tz7.48-2  7401  el1o  7443  dif1o  7444  ondif2  7446  oawordeulem  7498  elecg  7649  brecop  7704  erovlem  7707  eceqoveq  7717  mapsncnv  7767  mptelixpg  7808  brsdom  7841  isfi  7842  enssdom  7843  brdom2  7848  map1  7898  xpcomco  7912  brsdom2  7946  en3lplem2  8372  cnfcom2lem  8458  epfrs  8467  r1limg  8494  r1ord  8503  r1ord3  8505  tz9.12lem3  8512  rankvaln  8522  r1elss  8529  rankpwi  8546  ssrankr1  8558  r1val3  8561  r1pw  8568  rankr1b  8587  isnum2  8631  cardprclem  8665  infxpenlem  8696  alephcard  8753  alephnbtwn  8754  alephnbtwn2  8755  alephord2  8759  alephsdom  8769  dfac3  8804  dfac5lem2  8807  dfac5lem3  8808  dfac5lem5  8810  pwsdompw  8886  cfub  8931  cardcf  8934  cflecard  8935  cfle  8936  cflim2  8945  cofsmo  8951  cfidm  8957  isfin3  8978  isfin5  8981  isfin6  8982  sdom2en01  8984  fin23lem26  9007  fin23lem30  9024  isf32lem5  9039  itunitc1  9102  ituniiun  9104  axdc3lem3  9134  axcclem  9139  axdclem  9201  iunfo  9217  iundom2g  9218  cardidg  9226  konigthlem  9246  alephadd  9255  alephreg  9260  pwcfsdom  9261  cfpwsdom  9262  elgch  9300  fpwwe2lem12  9319  canth4  9325  wunex2  9416  r1tskina  9460  elni  9554  nlt1pi  9584  adderpq  9634  mulerpq  9635  recmulnq  9642  addsrpr  9752  mulsrpr  9753  opelcn  9806  opelreal  9807  elreal  9808  elreal2  9809  0ncn  9810  addcnsr  9812  mulcnsr  9813  xrlenlt  9954  elnn0  11141  elnnne0  11153  un0addcl  11173  un0mulcl  11174  uztrn2  11537  elnnuz  11556  elnn0uz  11557  elq  11622  elxr  11785  elfzm1b  12242  uzrdgfni  12574  fzennn  12584  fsuppmapnn0fiubOLD  12608  ser0  12670  hash2pwpr  13065  iswrd  13108  s3iunsndisj  13501  sumz  14246  sumss  14248  fsumcvg3  14253  abscvgcvg  14338  isumshft  14356  prodf1  14408  zprod  14452  prod1  14459  prodss  14462  prodsn  14477  prodsnf  14479  bpolydiflem  14570  bpoly2  14573  bpoly3  14574  bpoly4  14575  ruclem6  14749  divides  14769  dvdsflip  14823  pwp1fsum  14898  sadc0  14960  eulerthlem2  15271  prm23lt5  15303  4sqlem2  15437  4sqlem12  15444  vdwpc  15468  xpscf  15995  cidpropd  16139  oppcsect  16207  funcpropd  16329  natpropd  16405  initoeu2lem0  16432  arwhoma  16464  eldmcoa  16484  pospo  16742  psss  16983  ismgmn0  17013  gsumpropd2lem  17042  dfgrp2e  17217  ghmeqker  17456  cntri  17532  oppgsubg  17562  fvcosymgeq  17618  symgfixels  17623  pmtrfrn  17647  efgsfo  17921  efgrelexlemb  17932  lt6abl  18065  dmdprd  18166  dprdval  18171  dprdw  18178  srgbinomlem4  18312  isnirred  18469  isrhm  18490  issrng  18619  lspexchn2  18898  lspindp2l  18901  lspindp2  18902  lbsextlem2  18926  evlslem4  19275  ply1bascl2  19341  cply1mul  19431  lply1binom  19443  dsmmelbas  19844  frlmbas3  19876  lindsind2  19919  islindf4  19938  matsubgcell  20001  matinvgcell  20002  matvscacell  20003  matepmcl  20029  matepm2cl  20030  scmatscm  20080  smatvscl  20091  marrepcl  20131  marepvcl  20136  mulmarep1el  20139  mulmarep1gsum1  20140  mulmarep1gsum2  20141  submabas  20145  m1detdiag  20164  mdetdiag  20166  m2detleib  20198  gsummatr01lem3  20224  gsummatr01  20226  smadiadetlem4  20236  slesolinv  20247  slesolinvbi  20248  slesolex  20249  cramerimplem2  20251  pmatcoe1fsupp  20267  mat2pmatbas  20292  mat2pmatmul  20297  mat2pmatlin  20301  decpmatmul  20338  monmatcollpw  20345  pm2mpf1  20365  pm2mpghm  20382  istps  20493  mretopd  20648  neiptopuni  20686  lpdifsn  20699  restcls  20737  perfopn  20741  pnfnei  20776  mnfnei  20777  lmss  20854  hauscmplem  20961  is2ndc  21001  2ndcdisj  21011  hausnlly  21048  txuni2  21120  ptpjpre1  21126  elpt  21127  dfac14  21173  xkococn  21215  fbasrn  21440  fin1aufil  21488  elfm2  21504  elfm3  21506  fbflim  21532  flffbas  21551  cnpflf2  21556  fclsbas  21577  tsmssubm  21698  iscusp2  21858  imasdsf1olem  21929  metustel  22106  metuel2  22121  isnghm  22269  opnreen  22374  iccpnfcnv  22482  cvsi  22667  minveclem3b  22924  ovoliunlem1  22994  ioombl1lem4  23053  subopnmbl  23095  vitalilem2  23101  vitalilem3  23102  mbfimaopnlem  23145  mbfimaopn2  23147  itg2l  23219  dvply1  23760  vieta1lem1  23786  vieta1lem2  23787  elaa  23792  taylthlem2  23849  abelthlem6  23911  abelthlem9  23915  sinq34lt0t  23982  ellogrn  24027  dvrelog  24100  ellogdm  24102  logtayl2  24125  cxpcn3lem  24205  cxpcn3  24206  1cubr  24286  atandm  24320  atanf  24324  reasinsin  24340  atans2  24375  dmarea  24401  xrlimcnp  24412  amgmlem  24433  ppiublem1  24644  lgsdir2lem2  24768  gausslemma2dlem1a  24807  lgsquadlem1  24822  lgsquadlem2  24823  2sqlem1  24859  rpvmasum2  24918  eleenn  25494  usgraop  25645  nbgra0edg  25727  nbgraf1olem1  25736  nbgraf1olem3  25738  nbgraf1olem5  25740  uvtx01vtx  25786  wlknwwlknsur  26006  clwwlknprop  26066  hashecclwwlkn1  26127  usghashecclwwlk  26128  2wlkonot3v  26168  2spthonot3v  26169  isrgra  26219  isrusgra  26220  frgranbnb  26313  frgrancvvdeqlem2  26324  frgrancvvdeqlem3  26325  frgrancvvdeqlem4  26326  frgrancvvdeqlemC  26332  frgrawopreglem3  26339  frgrawopreglem4  26340  frgrawopreg  26342  2spotiundisj  26355  topnfbey  26483  isvclem  26598  isnvlem  26633  vsfval  26658  h2hlm  27027  hhcmpl  27247  hhcms  27250  elch0  27301  omlsilem  27451  h1de2ctlem  27604  elspansni  27607  nonbooli  27700  spansncvi  27701  adjeq  27984  cnlnssadj  28129  cnvbraval  28159  brabgaf  28606  fmptdF  28642  fmptcof2  28645  acunirnmpt  28647  acunirnmpt2  28648  ofpreima  28654  fcnvgreu  28661  1stpreima  28673  2ndpreima  28674  elxrge02  28777  psgnfzto1stlem  28987  submatres  29006  lmat22lem  29017  crefdf  29049  cmppcmp  29059  prsdm  29094  prsrn  29095  xrge0iifcnv  29113  xrge0iifiso  29115  xrge0iifhom  29117  pnfneige0  29131  qqhre  29198  rrhre  29199  esumnul  29243  esumcvgsum  29283  ldgenpisyslem1  29359  measvuni  29410  cntnevol  29424  dya2iocnrect  29476  sibf0  29529  oddpwdc  29549  eulerpartlemd  29561  eulerpartgbij  29567  eulerpartlemgh  29573  isrrvv  29638  coinfliprv  29677  ballotlem7  29730  signswch  29770  bnj23  29844  bnj158  29857  bnj168  29858  bnj1138  29919  bnj1143  29921  bnj1454  29972  bnj110  29988  bnj882  30056  bnj893  30058  bnj916  30063  bnj970  30077  bnj983  30081  bnj984  30082  bnj1137  30123  bnj1174  30131  bnj1388  30161  bnj1398  30162  subfacp1lem5  30226  mrsub0  30473  mrsubccat  30475  mrsubcn  30476  elmrsubrn  30477  msubco  30488  msubvrs  30517  elmthm  30533  mthmblem  30537  elrn3  30712  dfon2lem7  30744  eltrpred  30776  frrlem5e  30838  frrlem11  30842  nofulllem5  30911  brsset  30972  eltrans  30974  elfix  30986  ellimits  30993  elfuns  30998  elsingles  31001  fvtransport  31115  brcolinear2  31141  fvray  31224  linedegen  31226  fvline  31227  ellines  31235  fwddifn0  31247  elhf  31257  hfninf  31269  fnessref  31328  bj-csbsnlem  31886  bj-sels  31939  bj-eltag  31954  bj-sngltag  31960  bj-projun  31971  bj-0nelmpt  32046  bj-elid  32058  bj-elccinfty  32074  f1omptsnlem  32155  icoreelrnab  32174  relowlpssretop  32184  finxpnom  32210  uncov  32356  tan2h  32367  ptrecube  32375  poimirlem25  32400  poimirlem29  32404  poimirlem30  32405  poimirlem31  32406  poimirlem32  32407  cnambfre  32424  ftc1cnnc  32450  sdclem2  32504  sdclem1  32505  fdc  32507  caushft  32523  issmgrpOLD  32628  ismndo  32637  isrngo  32662  isdivrngo  32715  csbcom2fi  32900  dath  33836  diclspsn  35297  dvh4dimlem  35546  dvh2dim  35548  dvh3dim3N  35552  lcfrvalsnN  35644  mapdh6eN  35843  mapdh7dN  35853  mapdh8b  35883  hdmap1l6e  35918  pellex  36213  rmspecnonsq  36286  islmodfg  36453  aaitgo  36547  areaquad  36617  elcnvcnvintab  36703  elnonrel  36706  elcnvcnvlem  36720  cnvcnvintabd  36721  brfvrcld2  36799  dvgrat  37329  cvgdvgrat  37330  radcnvrat  37331  nznngen  37333  uzmptshftfval  37363  binomcxplemcvg  37371  binomcxplemnotnn0  37373  tpid3gVD  37895  en3lplem2VD  37897  rabid3  38081  rexanuz3  38099  eliuniin  38103  eliuniin2  38131  disjinfi  38171  fsneq  38189  iuneqfzuzlem  38288  allbutfi  38354  elicores  38404  climsuselem1  38471  climsuse  38472  islptre  38483  fnlimfvre  38538  stoweidlem14  38704  stoweidlem39  38729  stoweidlem48  38738  stoweidlem51  38741  stoweidlem59  38749  stoweidlem62  38752  wallispilem3  38757  fourierdlem42  38839  fourierdlem62  38858  fourierdlem80  38876  fourierdlem103  38899  fourierdlem104  38900  etransclem26  38950  rrxsnicc  38993  ioorrnopn  38998  ioorrnopnxr  39000  sge00  39066  sge0fodjrnlem  39106  sge0isum  39117  sge0seq  39136  ismea  39141  meadjiunlem  39155  carageneld  39189  volicorescl  39240  hoidmv1lelem1  39278  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem3  39284  ovnhoilem2  39289  hoiqssbllem2  39310  opnvonmbllem2  39320  ovolval4lem1  39336  iinhoiicc  39362  vonioolem1  39368  smflimlem1  39454  smflimlem2  39455  smflim  39460  nsssmfmbf  39462  smfresal  39470  smfrec  39471  smfdiv  39479  smfpimbor1lem2  39481  ndmaovcl  39730  ndmaovcom  39732  ndmaovass  39733  ndmaovdistr  39734  fmtno4prmfac  39820  iseven  39877  isodd  39878  dfodd5  39908  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  pfxccatpfx1  40088  otiunsndisjX  40125  elfz0lmr  40187  elxnn0  40194  isuhgr  40277  isushgr  40278  isupgr  40305  isumgr  40315  umgredg  40366  umgrpredgav  40367  umgredgne  40370  umgredgnlp  40372  isuspgr  40377  isusgr  40378  ausgrusgri  40393  usgredgappr  40418  edgassv2  40420  uspgredg2vlem  40445  uspgredg2v  40446  ushgredgedga  40451  ushgredgedgaloop  40453  griedg0ssusgr  40484  uhgrissubgr  40494  subumgredg2  40504  umgrres1lem  40524  upgrres1  40527  nbgrcl  40554  nbuhgr  40560  nbuhgr2vtx1edgblem  40568  nbupgrres  40587  edgnbusgreu  40590  nbusgredgeu0  40591  nbusgrf1o0  40592  hashnbusgrnn0  40599  nbupgruvtxres  40629  cusgrfilem2  40667  vtxdg0v  40683  vtxduhgr0nedg  40702  uhgrvd00  40745  rgrx0ndm  40788  1wlk1walk  40838  1wlkp1lem6  40882  iswwlks  41034  wspthnonp  41050  wwlksn0  41054  wlknwwlksnsur  41082  wwlksnwwlksnon  41116  umgr2wlk  41151  elwwlks2ons3  41154  2wspiundisj  41161  elwwlks2s3  41164  rusgrnumwlkg  41175  isclwwlks  41183  wwlksext2clwwlk  41226  hashecclwwlksn1  41256  umgrhashecclwwlk  41257  1pthon2v-av  41315  uhgr3cyclex  41344  isconngr  41351  isconngr1  41352  eucrctshift  41406  isfrgr  41425  frgrnbnb  41458  frgrncvvdeqlem2  41465  frgrncvvdeqlem3  41466  frgrncvvdeqlem4  41467  frgrncvvdeqlemC  41473  frgrwopreglem3  41478  frgrwopreglem4  41479  frgrwopreg  41481  fusgreghash2wspv  41494  av-numclwwlkovf2  41510  av-numclwwlk2lem1  41527  av-numclwlk2lem2f1o  41530  opeliun2xp  41899  ply1sclrmsm  41960  lcoop  41989  lincfsuppcl  41991  linccl  41992  lincvalsng  41994  lincvalpr  41996  lincvalsc0  41999  linc0scn0  42001  lincdifsn  42002  linc1  42003  lincsum  42007  lincscm  42008  lspsslco  42015  snlindsntor  42049  lincresunit3lem2  42058  ldepsnlinclem1  42083  ldepsnlinclem2  42084
  Copyright terms: Public domain W3C validator