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

Theorem eleq2i 2722
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 2719 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  eleq12i  2723  eleqtri  2728  eleq2s  2748  hbxfreq  2759  raleqbii  3019  rexeqbii  3083  rabeq2i  3228  elab2g  3385  elrabf  3392  elrab3t  3395  elrab2  3399  cbvsbc  3497  elin2  3834  elsymdif  3882  dfnul2  3950  noel  3952  eltpg  4259  elunirab  4480  elintrab  4520  disjxiun  4681  disjxiunOLD  4682  exss  4961  otiunsndisj  5009  brabsb  5015  brabga  5018  pofun  5080  elxp  5165  opeliunxp  5204  bropaex12  5226  brab2a  5228  elcnv  5331  elrnmptg  5407  opelresg  5434  opelresOLD  5438  rninxp  5608  elsuci  5829  elsucg  5830  elsuc2g  5831  elfv  6227  0fv  6265  opabiota  6300  dffv2  6310  fvopab3g  6316  fvmptex  6333  fvopab5  6349  fvn0ssdmfun  6390  fveqressseq  6395  f0cli  6410  fmptco  6436  fvrnressn  6468  funfvima  6532  elunirnALT  6550  fliftel  6599  eloprabga  6789  elrnmpt2  6815  ovid  6819  offval  6946  suceloni  7055  1st2val  7238  2nd2val  7239  bropopvvv  7300  bropfvvvv  7302  fsplit  7327  xporderlem  7333  brtpos2  7403  wfrdmcl  7468  wfrfun  7470  wfrlem12  7471  wfrlem17  7476  wfr2  7479  issmo  7490  smores3  7495  tfrlem7  7524  tfrlem9  7526  tfrlem9a  7527  tfr2b  7537  tfr2  7539  rdgsuc  7565  frsucmptn  7579  tz7.48-2  7582  el1o  7624  dif1o  7625  ondif2  7627  oawordeulem  7679  elecg  7828  brecop  7883  erovlem  7886  eceqoveq  7895  mapsncnv  7946  mptelixpg  7987  brsdom  8020  isfi  8021  enssdom  8022  brdom2  8027  map1  8077  xpcomco  8091  brsdom2  8125  en3lplem2  8550  cnfcom2lem  8636  epfrs  8645  r1limg  8672  r1ord  8681  r1ord3  8683  tz9.12lem3  8690  rankvaln  8700  r1elss  8707  rankpwi  8724  ssrankr1  8736  r1val3  8739  r1pw  8746  rankr1b  8765  isnum2  8809  cardprclem  8843  infxpenlem  8874  alephcard  8931  alephnbtwn  8932  alephnbtwn2  8933  alephord2  8937  alephsdom  8947  dfac3  8982  dfac5lem2  8985  dfac5lem3  8986  dfac5lem5  8988  pwsdompw  9064  cfub  9109  cardcf  9112  cflecard  9113  cfle  9114  cflim2  9123  cofsmo  9129  cfidm  9135  isfin3  9156  isfin5  9159  isfin6  9160  sdom2en01  9162  fin23lem26  9185  fin23lem30  9202  isf32lem5  9217  itunitc1  9280  ituniiun  9282  axdc3lem3  9312  axcclem  9317  axdclem  9379  iunfo  9399  iundom2g  9400  cardidg  9408  konigthlem  9428  alephadd  9437  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  elgch  9482  fpwwe2lem12  9501  canth4  9507  wunex2  9598  r1tskina  9642  elni  9736  nlt1pi  9766  adderpq  9816  mulerpq  9817  recmulnq  9824  addsrpr  9934  mulsrpr  9935  opelcn  9988  opelreal  9989  elreal  9990  elreal2  9991  0ncn  9992  addcnsr  9994  mulcnsr  9995  xrlenlt  10141  elnn0  11332  elnnne0  11344  un0addcl  11364  un0mulcl  11365  elxnn0  11403  uztrn2  11743  elnnuz  11762  elnn0uz  11763  elq  11828  elxr  11988  elfzm1b  12456  elfz0lmr  12623  uzrdgfni  12797  fzennn  12807  fsuppmapnn0fiubOLD  12831  ser0  12893  hash2pwpr  13296  iswrd  13339  s3iunsndisj  13753  sumz  14497  sumss  14499  fsumcvg3  14504  abscvgcvg  14595  isumshft  14615  prodf1  14667  zprod  14711  prod1  14718  prodss  14721  prodsn  14736  prodsnf  14738  bpolydiflem  14829  bpoly2  14832  bpoly3  14833  bpoly4  14834  ruclem6  15008  divides  15029  dvdsflip  15086  pwp1fsum  15161  sadc0  15223  eulerthlem2  15534  prm23lt5  15566  4sqlem2  15700  4sqlem12  15707  vdwpc  15731  xpscf  16273  cidpropd  16417  oppcsect  16485  funcpropd  16607  natpropd  16683  initoeu2lem0  16710  arwhoma  16742  eldmcoa  16762  pospo  17020  psss  17261  ismgmn0  17291  gsumpropd2lem  17320  dfgrp2e  17495  ghmeqker  17734  cntri  17809  oppgsubg  17839  fvcosymgeq  17895  symgfixels  17900  pmtrfrn  17924  efgsfo  18198  efgrelexlemb  18209  lt6abl  18342  dmdprd  18443  dprdval  18448  dprdw  18455  srgbinomlem4  18589  isnirred  18746  isrhm  18769  issrng  18898  lspexchn2  19179  lspindp2l  19182  lspindp2  19183  lbsextlem2  19207  evlslem4  19556  ply1bascl2  19622  cply1mul  19712  lply1binom  19724  cnfldfunALT  19807  dsmmelbas  20131  frlmbas3  20163  lindsind2  20206  islindf4  20225  matsubgcell  20288  matinvgcell  20289  matvscacell  20290  matepmcl  20316  matepm2cl  20317  scmatscm  20367  smatvscl  20378  marrepcl  20418  marepvcl  20423  mulmarep1el  20426  mulmarep1gsum1  20427  mulmarep1gsum2  20428  submabas  20432  m1detdiag  20451  mdetdiag  20453  m2detleib  20485  gsummatr01lem3  20511  gsummatr01  20513  smadiadetlem4  20523  slesolinv  20534  slesolinvbi  20535  slesolex  20536  cramerimplem2  20538  pmatcoe1fsupp  20554  mat2pmatbas  20579  mat2pmatmul  20584  mat2pmatlin  20588  decpmatmul  20625  monmatcollpw  20632  pm2mpf1  20652  pm2mpghm  20669  istps  20786  mretopd  20944  neiptopuni  20982  lpdifsn  20995  restcls  21033  perfopn  21037  pnfnei  21072  mnfnei  21073  lmss  21150  hauscmplem  21257  is2ndc  21297  2ndcdisj  21307  hausnlly  21344  txuni2  21416  ptpjpre1  21422  elpt  21423  dfac14  21469  xkococn  21511  fbasrn  21735  fin1aufil  21783  elfm2  21799  elfm3  21801  fbflim  21827  flffbas  21846  cnpflf2  21851  fclsbas  21872  tsmssubm  21993  iscusp2  22153  imasdsf1olem  22225  metustel  22402  metuel2  22417  isnghm  22574  opnreen  22681  iccpnfcnv  22790  cvsi  22976  minveclem3b  23245  ovoliunlem1  23316  ioombl1lem4  23375  subopnmbl  23418  vitalilem2  23423  vitalilem3  23424  mbfimaopnlem  23467  mbfimaopn2  23469  itg2l  23541  dvply1  24084  vieta1lem1  24110  vieta1lem2  24111  elaa  24116  taylthlem2  24173  abelthlem6  24235  abelthlem9  24239  sinq34lt0t  24306  ellogrn  24351  dvrelog  24428  ellogdm  24430  logtayl2  24453  cxpcn3lem  24533  cxpcn3  24534  1cubr  24614  atandm  24648  atanf  24652  reasinsin  24668  atans2  24703  dmarea  24729  xrlimcnp  24740  amgmlem  24761  ppiublem1  24972  lgsdir2lem2  25096  gausslemma2dlem1a  25135  lgsquadlem1  25150  lgsquadlem2  25151  2sqlem1  25187  rpvmasum2  25246  eleenn  25821  edgiedgb  25992  isuhgr  26000  isushgr  26001  isupgr  26024  isumgr  26035  umgredg  26078  umgrpredgv  26080  umgredgne  26085  umgredgnlp  26087  isuspgr  26092  isusgr  26093  ausgrusgri  26108  usgredgppr  26133  edgssv2  26135  uspgredg2vlem  26160  uspgredg2v  26161  ushgredgedg  26166  ushgredgedgloop  26168  griedg0ssusgr  26202  uhgrissubgr  26212  subumgredg2  26222  uhgrspansubgrlem  26227  umgrres1lem  26247  upgrres1  26250  nbgrcl  26272  nbgrclOLD  26273  nbuhgr  26284  nbuhgr2vtx1edgblem  26292  nbupgrres  26310  edgnbusgreu  26313  nbusgredgeu0  26314  nbusgrf1o0  26315  hashnbusgrnn0  26322  nbupgruvtxres  26358  cffldtocusgr  26399  cusgrfilem2  26408  vtxdg0v  26425  vtxduhgr0nedg  26444  uhgrvd00  26486  vtxdginducedm1  26495  finsumvtxdg2ssteplem4  26500  rgrx0ndm  26545  wlk1walk  26591  wlkp1lem6  26631  iswwlks  26784  wwlknllvtx  26795  wwlksonvtx  26805  wspthnonp  26813  wwlksn0  26817  wlkiswwlksupgr2  26831  wlknwwlksnsur  26844  wwlksnwwlksnon  26878  wwlksnwwlksnonOLD  26880  2pthon3v  26908  umgr2wlk  26914  elwwlks2s3  26916  wwlks2onv  26918  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  rusgrnumwlkg  26944  isclwwlk  26952  clwlkclwwlk  26968  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  clwwlknon1  27072  clwwlknon1nloop  27074  clwwlknon2x  27078  1pthon2v  27131  uhgr3cyclex  27160  isconngr  27167  isconngr1  27168  eucrctshift  27221  isfrgr  27238  frgrnbnb  27273  frgrncvvdeqlem1  27279  frgrncvvdeqlem2  27280  frgrncvvdeqlem3  27281  frgrncvvdeqlem9  27287  fusgreghash2wspv  27315  clwwlkccatlem  27331  extwwlkfab  27342  numclwlk1lem2foa  27344  numclwlk1lem2fo  27348  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  numclwwlk5lem  27374  topnfbey  27455  isvclem  27560  isnvlem  27593  vsfval  27616  h2hlm  27965  hhcmpl  28185  hhcms  28188  elch0  28239  omlsilem  28389  h1de2ctlem  28542  elspansni  28545  nonbooli  28638  spansncvi  28639  adjeq  28922  cnlnssadj  29067  cnvbraval  29097  brabgaf  29546  elimampt  29566  fmptdF  29584  fmptcof2  29585  acunirnmpt  29587  acunirnmpt2  29588  ofpreima  29593  fcnvgreu  29600  1stpreima  29612  2ndpreima  29613  fz2ssnn0  29675  elxrge02  29768  psgnfzto1stlem  29978  submatres  30000  lmat22lem  30011  crefdf  30043  cmppcmp  30053  prsdm  30088  prsrn  30089  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  pnfneige0  30125  qqhre  30192  rrhre  30193  esumnul  30238  esumcvgsum  30278  ldgenpisyslem1  30354  measvuni  30405  cntnevol  30419  dya2iocnrect  30471  sibf0  30524  oddpwdc  30544  eulerpartlemd  30556  eulerpartgbij  30562  eulerpartlemgh  30568  isrrvv  30633  coinfliprv  30672  ballotlem7  30725  signswch  30766  hashreprin  30826  chtvalz  30835  circlemethhgt  30849  hgt750lemb  30862  tgoldbachgt  30869  bnj23  30912  bnj158  30923  bnj168  30924  bnj1138  30985  bnj1143  30987  bnj1454  31038  bnj110  31054  bnj882  31122  bnj893  31124  bnj916  31129  bnj970  31143  bnj983  31147  bnj984  31148  bnj1137  31189  bnj1174  31197  bnj1388  31227  bnj1398  31228  subfacp1lem5  31292  mrsub0  31539  mrsubccat  31541  mrsubcn  31542  elmrsubrn  31543  msubco  31554  msubvrs  31583  elmthm  31599  mthmblem  31603  elrn3  31778  dfon2lem7  31818  eltrpred  31850  frrlem5e  31913  frrlem11  31917  madeval2  32061  brsset  32121  eltrans  32123  elfix  32135  ellimits  32142  elfuns  32147  elsingles  32150  fvtransport  32264  brcolinear2  32290  fvray  32373  linedegen  32375  fvline  32376  ellines  32384  fwddifn0  32396  elhf  32406  hfninf  32418  fnessref  32477  bj-csbsnlem  33023  bj-sels  33075  bj-eltag  33090  bj-sngltag  33096  bj-projun  33107  bj-0nelmpt  33194  bj-elid  33215  bj-elccinfty  33231  f1omptsnlem  33313  icoreelrnab  33332  relowlpssretop  33342  finxpnom  33368  uncov  33520  tan2h  33531  ptrecube  33539  poimirlem25  33564  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  cnambfre  33588  ftc1cnnc  33614  sdclem2  33668  sdclem1  33669  fdc  33671  caushft  33687  issmgrpOLD  33792  ismndo  33801  isrngo  33826  isdivrngo  33879  csbcom2fi  34064  elecALTV  34171  eldmcoss  34348  coss0  34369  elrels2  34376  dath  35340  diclspsn  36800  dvh4dimlem  37049  dvh2dim  37051  dvh3dim3N  37055  lcfrvalsnN  37147  mapdh6eN  37346  mapdh7dN  37356  mapdh8b  37386  hdmap1l6e  37421  pellex  37716  rmspecnonsq  37789  islmodfg  37956  aaitgo  38049  areaquad  38119  elcnvcnvintab  38205  elnonrel  38208  elcnvcnvlem  38222  cnvcnvintabd  38223  brfvrcld2  38301  dvgrat  38828  cvgdvgrat  38829  radcnvrat  38830  nznngen  38832  uzmptshftfval  38862  binomcxplemcvg  38870  binomcxplemnotnn0  38872  tpid3gVD  39391  en3lplem2VD  39393  rexanuz3  39589  eliuniin  39593  eliuniin2  39617  disjinfi  39694  fsneq  39712  iuneqfzuzlem  39863  allbutfi  39929  eluzelz2  39940  uz0  39952  uzublem  39970  uzid3  39975  elicores  40078  uzinico  40105  climsuselem1  40157  climsuse  40158  islptre  40169  fnlimfvre  40224  limsupresico  40250  limsupvaluz  40258  limsupubuzlem  40262  limsupequzmptlem  40278  liminfresico  40321  cnrefiisplem  40373  stoweidlem14  40549  stoweidlem39  40574  stoweidlem48  40583  stoweidlem51  40586  stoweidlem59  40594  stoweidlem62  40597  wallispilem3  40602  fourierdlem42  40684  fourierdlem62  40703  fourierdlem80  40721  fourierdlem103  40744  fourierdlem104  40745  etransclem26  40795  rrxsnicc  40838  ioorrnopn  40843  ioorrnopnxr  40845  sge00  40911  sge0fodjrnlem  40951  sge0isum  40962  sge0seq  40981  ismea  40986  meadjiunlem  41000  carageneld  41037  volicorescl  41088  hoidmv1lelem1  41126  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem3  41132  ovnhoilem2  41137  hoiqssbllem2  41158  opnvonmbllem2  41168  ovolval4lem1  41184  iinhoiicc  41209  vonioolem1  41215  smflimlem1  41300  smflimlem2  41301  smflim  41306  nsssmfmbf  41308  smfresal  41316  smfrec  41317  smfdiv  41325  smfpimbor1lem2  41327  smflim2  41333  smflimmpt  41337  smfsupmpt  41342  smfinflem  41344  smfinfmpt  41346  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem3  41349  smflimsuplem5  41351  smflimsuplem6  41352  smflimsup  41355  smflimsupmpt  41356  smfliminfmpt  41359  ndmaovcl  41604  ndmaovcom  41606  ndmaovass  41607  ndmaovdistr  41608  otiunsndisjX  41621  fvmptrabdm  41632  pfxccatpfx1  41752  fmtno4prmfac  41809  dfodd5  41897  sbgoldbo  42000  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  sprsymrelfolem2  42068  sprsymrelf  42070  sprsymrelf1  42071  uspgrsprf  42079  uspgrsprf1  42080  uspgrsprfo  42081  opeliun2xp  42436  ply1sclrmsm  42496  lcoop  42525  lincfsuppcl  42527  linccl  42528  lincvalsng  42530  lincvalpr  42532  lincvalsc0  42535  linc0scn0  42537  lincdifsn  42538  linc1  42539  lincsum  42543  lincscm  42544  lspsslco  42551  snlindsntor  42585  lincresunit3lem2  42594  ldepsnlinclem1  42619  ldepsnlinclem2  42620  elpglem3  42784
  Copyright terms: Public domain W3C validator