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

Theorem eleq2i 2535
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 2530 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  eleq12i  2536  eleqtri  2543  eleq2s  2565  hbxfreq  2579  abeq2iOLD  2585  abeq1iOLD  2587  nfceqiOLD  2616  raleqbii  2902  rexeqbii  2972  rabeq2i  3106  elab2g  3248  elrabf  3255  elrab3t  3256  elrab2  3259  cbvsbc  3356  elin2  3688  dfnul2  3786  noel  3788  eltpg  4071  tpid3g  4145  elunirab  4261  elintrab  4298  disjxiun  4449  exss  4715  elop  4718  otiunsndisj  4758  brabsb  4763  brabga  4766  pofun  4821  elsuci  4949  elsucg  4950  elsuc2g  4951  elxp  5021  brab2a  5054  opeliunxp  5056  bropaex12  5078  brab2ga  5080  elcnv  5184  elrnmptg  5257  opelres  5284  rninxp  5451  elfv  5869  0fv  5904  opabiota  5936  dffv2  5946  fvopab3g  5952  fvmptex  5966  fvopab5  5979  fvn0ssdmfun  6022  fveqressseq  6027  f0cli  6042  fmptco  6064  fvrnressn  6086  funfvima  6147  elunirnALT  6164  fliftel  6207  eloprabga  6389  elrnmpt2  6415  ovid  6419  offval  6547  suceloni  6648  1st2val  6826  2nd2val  6827  bropopvvv  6880  fsplit  6905  xporderlem  6911  brtpos2  6980  issmo  7038  smores3  7043  tfrlem7  7071  tfrlem9  7073  tfrlem9a  7074  tfr2b  7084  tfr2  7086  rdgsuc  7109  frsucmptn  7123  tz7.48-2  7126  el1o  7168  dif1o  7169  ondif2  7171  oawordeulem  7222  elecg  7369  brecop  7423  erovlem  7426  eceqoveq  7435  mapsncnv  7485  mptelixpg  7526  brsdom  7558  isfi  7559  enssdom  7560  brdom2  7565  map1  7614  xpcomco  7627  brsdom2  7661  en3lplem2  8053  cnfcom2lem  8166  cnfcom2lemOLD  8174  epfrs  8183  r1limg  8210  r1ord  8219  r1ord3  8221  tz9.12lem3  8228  rankvaln  8238  r1elss  8245  rankpwi  8262  ssrankr1  8274  r1val3  8277  r1pw  8284  rankr1b  8303  isnum2  8347  cardprclem  8381  infxpenlem  8412  alephcard  8472  alephnbtwn  8473  alephnbtwn2  8474  alephord2  8478  alephsdom  8488  dfac3  8523  dfac5lem2  8526  dfac5lem3  8527  dfac5lem5  8529  pwsdompw  8605  cfub  8650  cardcf  8653  cflecard  8654  cfle  8655  cflim2  8664  cofsmo  8670  cfidm  8676  isfin3  8697  isfin5  8700  isfin6  8701  sdom2en01  8703  fin23lem26  8726  fin23lem30  8743  isf32lem5  8758  itunitc1  8821  ituniiun  8823  axdc3lem2  8852  axdc3lem3  8853  axcclem  8858  axdclem  8920  iunfo  8935  iundom2g  8936  cardidg  8944  konigthlem  8964  alephadd  8973  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  elgch  9021  fpwwe2lem12  9040  canth4  9046  wunex2  9137  r1tskina  9181  elni  9275  nlt1pi  9305  adderpq  9355  mulerpq  9356  recmulnq  9363  addsrpr  9473  mulsrpr  9474  opelcn  9527  opelreal  9528  elreal  9529  elreal2  9530  0ncn  9531  addcnsr  9533  mulcnsr  9534  xrlenlt  9673  elnn0  10822  elnnne0  10834  un0addcl  10854  un0mulcl  10855  uztrn2  11127  elnnuz  11146  elnn0uz  11147  elq  11213  elxr  11354  elfzm1b  11785  uzrdgfni  12069  fzennn  12078  fsuppmapnn0fiub  12097  ser0  12159  hash2pwpr  12519  iswrd  12550  wrdeqswrdlsw  12674  sumz  13544  sumss  13546  fsumcvg3  13551  abscvgcvg  13633  isumshft  13651  prodf1  13700  zprod  13744  prod1  13751  prodss  13754  prodsn  13767  ruclem6  13968  divides  13988  sadc0  14104  eulerthlem2  14312  4sqlem2  14467  4sqlem12  14474  vdwpc  14498  xpscf  14963  cidpropd  15105  oppcsect  15168  funcpropd  15269  natpropd  15345  arwhoma  15372  eldmcoa  15392  pospo  15603  psss  15844  ismgmn0  15874  gsumpropd2lem  15900  ismndOLD  15926  ghmeqker  16293  cntri  16368  oppgsubg  16398  fvcosymgeq  16454  symgfixels  16459  pmtrfrn  16483  efgsfo  16757  efgrelexlemb  16768  lt6abl  16897  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  dprdw  17043  dprdwOLD  17050  srgbinomlem4  17194  isnirred  17349  isrhm  17370  issrng  17499  lspexchn2  17777  lspindp2l  17780  lspindp2  17781  lbsextlem2  17805  evlslem4OLD  18173  evlslem4  18174  ply1bascl2  18243  cply1mul  18335  lply1binom  18348  dsmmelbas  18770  frlmbas3  18807  lindsind2  18854  islindf4  18873  matsubgcell  18936  matinvgcell  18937  matvscacell  18938  matepmcl  18964  matepm2cl  18965  scmatscm  19015  smatvscl  19026  marrepcl  19066  marepvcl  19071  mulmarep1el  19074  mulmarep1gsum1  19075  mulmarep1gsum2  19076  submabas  19080  m1detdiag  19099  mdetdiag  19101  m2detleib  19133  gsummatr01lem3  19159  gsummatr01  19161  smadiadetlem4  19171  slesolinv  19182  slesolinvbi  19183  slesolex  19184  cramerimplem2  19186  pmatcoe1fsupp  19202  mat2pmatbas  19227  mat2pmatmul  19232  mat2pmatlin  19236  decpmatmul  19273  monmatcollpw  19280  pm2mpf1  19300  pm2mpghm  19317  eltopspOLD  19419  istpsOLD  19421  istps  19437  mretopd  19593  neiptopuni  19631  lpdifsn  19644  restcls  19682  perfopn  19686  pnfnei  19721  mnfnei  19722  lmss  19799  hauscmplem  19906  is2ndc  19947  2ndcdisj  19957  hausnlly  19994  txuni2  20066  ptpjpre1  20072  elpt  20073  dfac14  20119  xkococn  20161  fbasrn  20385  fin1aufil  20433  elfm2  20449  elfm3  20451  fbflim  20477  flffbas  20496  cnpflf2  20501  fclsbas  20522  tsmssubm  20644  iscusp2  20805  imasdsf1olem  20876  metustelOLD  21054  metustel  21055  metuel2  21082  isnghm  21230  opnreen  21336  iccpnfcnv  21444  minveclem3b  21843  ovoliunlem1  21913  ioombl1lem4  21971  subopnmbl  22013  vitalilem2  22018  vitalilem3  22019  mbfimaopnlem  22062  mbfimaopn2  22064  itg2l  22136  dvply1  22680  vieta1lem1  22706  vieta1lem2  22707  elaa  22712  taylthlem2  22769  abelthlem6  22831  abelthlem9  22835  sinq34lt0t  22902  ellogrn  22947  dvrelog  23018  ellogdm  23020  logtayl2  23043  cxpcn3lem  23121  cxpcn3  23122  1cubr  23173  atandm  23207  atanf  23211  reasinsin  23227  atans2  23262  dmarea  23287  xrlimcnp  23298  amgmlem  23319  dvdsflip  23458  ppiublem1  23477  lgsdir2lem2  23599  lgsquadlem1  23629  lgsquadlem2  23630  2sqlem1  23638  rpvmasum2  23697  eleenn  24199  usgraop  24350  nbgra0edg  24432  nbgraf1olem1  24441  nbgraf1olem3  24443  nbgraf1olem5  24445  uvtx01vtx  24492  wlknwwlknsur  24712  clwwlknprop  24772  hashecclwwlkn1  24834  usghashecclwwlk  24835  2wlkonot3v  24875  2spthonot3v  24876  isrgra  24926  isrusgra  24927  frgranbnb  25020  frgrancvvdeqlem2  25031  frgrancvvdeqlem3  25032  frgrancvvdeqlem4  25033  frgrancvvdeqlemC  25039  frgrawopreglem3  25046  frgrawopreglem4  25047  frgrawopreg  25049  2spotiundisj  25062  issmgrpOLD  25336  ismndo  25345  isrngo  25380  isdivrngo  25433  isvclem  25470  isnvlem  25503  vsfval  25528  h2hlm  25897  hhcmpl  26117  hhcms  26120  elch0  26172  omlsilem  26320  h1de2ctlem  26473  elspansni  26476  nonbooli  26569  spansncvi  26570  mayete3iOLD  26647  adjeq  26854  cnlnssadj  26999  cnvbraval  27029  fmptdF  27495  fmptcof2  27502  ofpreima  27507  fcnvgreu  27514  1stpreima  27524  2ndpreima  27525  elxrge02  27628  crefdf  27851  cmppcmp  27861  prsdm  27896  prsrn  27897  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  pnfneige0  27933  qqhre  27998  rrhre  27999  esumnul  28059  measvuni  28185  cntnevol  28199  dya2iocnrect  28252  sibf0  28276  oddpwdc  28293  eulerpartlemd  28305  eulerpartgbij  28311  eulerpartlemgh  28317  isrrvv  28382  coinfliprv  28421  ballotlem7  28474  signswch  28518  subfacp1lem5  28628  mrsub0  28876  mrsubccat  28878  mrsubcn  28879  elmrsubrn  28880  msubco  28891  msubvrs  28920  elmthm  28936  mthmblem  28940  ghomgrpilem2  29026  elrn3  29192  dfon2lem7  29221  eltrpred  29309  wfrlem9  29351  wfrlem11  29353  wfrlem12  29354  wfr2  29360  frrlem5e  29395  frrlem11  29399  nofulllem5  29466  elsymdif  29473  brsset  29539  eltrans  29541  elfix  29553  ellimits  29560  elfuns  29565  elsingles  29568  fvtransport  29682  brcolinear2  29708  fvray  29791  linedegen  29793  fvline  29794  ellines  29802  bpolydiflem  29816  bpoly2  29819  bpoly3  29820  bpoly4  29821  elhf  29831  hfninf  29843  tan2h  30047  cnambfre  30063  ftc1cnnc  30089  fnessref  30175  sdclem2  30235  sdclem1  30236  fdc  30238  caushft  30254  csbcom2fi  30534  pellex  30771  rmspecnonsq  30843  islmodfg  31015  aaitgo  31111  areaquad  31184  dvgrat  31193  cvgdvgrat  31194  radcnvrat  31195  nznngen  31221  uzmptshftfval  31251  binomcxplemcvg  31259  binomcxplemnotnn0  31261  prodsnf  31587  climsuselem1  31613  climsuse  31614  islptre  31625  stoweidlem14  31796  stoweidlem39  31821  stoweidlem48  31830  stoweidlem51  31833  stoweidlem59  31841  stoweidlem62  31844  wallispilem3  31849  fourierdlem42  31931  fourierdlem62  31951  fourierdlem80  31969  fourierdlem103  31992  fourierdlem104  31993  etransclem26  32043  ndmaovcl  32288  ndmaovcom  32290  ndmaovass  32291  ndmaovdistr  32292  otiunsndisjX  32301  isuhgr  32366  isushgr  32367  usgedgppr  32398  usgpredgv  32399  usgpredgvALT  32400  edgssv2ALT  32401  edgssv2  32402  initoeu2lem0  32619  opeliun2xp  32922  ply1sclrmsm  32983  lcoop  33012  lincfsuppcl  33014  linccl  33015  lincvalsng  33017  lincvalpr  33019  lincvalsc0  33022  linc0scn0  33024  lincdifsn  33025  linc1  33026  lincsum  33030  lincscm  33031  lspsslco  33038  snlindsntor  33072  lincresunit3lem2  33081  ldepsnlinclem1  33106  ldepsnlinclem2  33107  tpid3gVD  33642  en3lplem2VD  33644  bnj23  33771  bnj158  33784  bnj168  33785  bnj1138  33847  bnj1143  33849  bnj1454  33900  bnj110  33916  bnj882  33984  bnj893  33986  bnj916  33991  bnj970  34005  bnj983  34009  bnj984  34010  bnj1137  34051  bnj1174  34059  bnj1388  34089  bnj1398  34090  bj-csbsnlem  34470  bj-sels  34520  bj-eltag  34535  bj-sngltag  34541  bj-projun  34552  bj-elid  34599  bj-elccinfty  34617  dath  35460  diclspsn  36921  dvh4dimlem  37170  dvh2dim  37172  dvh3dim3N  37176  lcfrvalsnN  37268  mapdh6eN  37467  mapdh7dN  37477  mapdh8b  37507  hdmap1l6e  37542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator