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

Theorem eleq2 2475
Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21eleq2d 2472 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405    e. wcel 1842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397
This theorem is referenced by:  eleq12  2478  eleq2i  2480  eleq2dOLD  2483  nelneq2  2520  dvelimdc  2587  nelne1  2732  neleq2OLD  2744  raleqf  2999  rexeqf  3000  reueq1f  3001  rmoeq1f  3002  rabeqf  3051  clel3g  3186  clel4  3188  sbcbi2  3325  sbcel2gv  3336  csbeq2  3376  difeq2  3554  uneq1  3589  ineq1  3633  unineq  3699  n0i  3742  sbnfc2  3800  disjel  3815  elif  3924  exsnrex  4009  sneqr  4138  preqr1  4145  preq12b  4147  prel12  4148  elunii  4195  eluniab  4201  ssuni  4212  elinti  4235  elintab  4237  intss1  4241  intmin  4246  intab  4257  iineq2  4288  dfiin2g  4303  breq  4396  zfrepclf  4512  axsep2  4517  zfauscl  4518  sseliALT  4526  inuni  4555  pwne0  4563  elALT  4633  rext  4638  intid  4648  opth1  4663  opthwiener  4691  xpeq1  4836  xpeq2  4837  opthprc  4870  ordtri1  5442  ordtri3  5445  nsuceq0  5489  suctr  5492  ordnbtwn  5499  funopg  5600  dffv2  5921  fveqdmss  6003  dffo4  6024  fnsnb  6069  elunirn  6143  f1oiso  6229  canth  6236  eusvobj2  6270  mpt2eq123  6336  ndmovg  6438  snnex  6587  uniuni  6590  iunpw  6595  oneqmin  6622  onuninsuci  6657  nlimsucg  6659  limomss  6687  nnlim  6695  peano5  6706  unielxp  6819  cnvf1o  6882  smoel  7063  smo11  7067  tz7.44-2  7109  oawordeulem  7239  oaordex  7243  omordi  7251  oneo  7266  oeordi  7272  oeoa  7282  oeoe  7284  nnmordi  7316  nnaordex  7323  omabs  7332  nnneo  7336  omsmolem  7338  elqsn0  7416  qsel  7426  mapsn  7497  undifixp  7542  boxriin  7548  boxcutc  7549  fineqvlem  7768  fineqv  7769  pssnn  7772  fissuni  7858  dffi2  7916  inficl  7918  dffi3  7924  wofib  8003  zfregcl  8053  en3lplem1  8063  en3lp  8065  suc11reg  8068  inf0  8070  inf3lem2  8078  inf3lem3  8079  infeq5i  8085  axinf2  8089  dfom3  8096  elom3  8097  cantnfle  8121  oemapvali  8134  cantnflem1c  8137  cantnflem1  8139  cantnfleOLD  8151  cantnflem1cOLD  8160  cantnflem1OLD  8162  tc2  8204  r1sdom  8223  rankwflemb  8242  rankval3b  8275  rankunb  8299  rankuni2b  8302  tcrank  8333  cardlim  8384  cardprclem  8391  infxpenlem  8422  alephnbtwn  8483  alephordi  8486  cardaleph  8501  alephfp  8520  alephval3  8522  aceq1  8529  aceq2  8531  dfac3  8533  dfac5lem2  8536  dfac5lem4  8538  dfac2  8542  kmlem2  8562  kmlem4  8564  coflim  8672  cfsmolem  8681  fin23lem30  8753  isf32lem2  8765  isf34lem4  8788  axdc2lem  8859  axdc3lem2  8862  axdc3lem4  8864  axdc4lem  8866  zorn2lem7  8913  axdclem  8930  brdom7disj  8940  brdom6disj  8941  axpowndlem3  9005  winainflem  9100  iswun  9111  eltskg  9157  inar1  9182  elgrug  9199  inaprc  9243  eltskm  9250  addnidpi  9308  indpi  9314  nqereu  9336  elnp  9394  elnpi  9395  genpnnp  9412  ltaddpr  9441  dfnn2  10588  dfnn3  10589  dfuzi  10993  uz11  11148  elfzonlteqm1  11925  om2uzlti  12100  axdc4uz  12132  hashrabsn1  12488  hashbclem  12548  hashf1lem2  12552  hash2prd  12565  hash2prv  12572  wrdsymb0  12626  lsw0  12637  rtrclreclem3  13040  prodeq1f  13865  rpnnen2lem1  14155  rpnnen2lem2  14156  sadcp1  14312  ismre  15202  isacs  15263  initoid  15606  termoid  15607  initoeu2lem1  15615  clatl  16068  mreclatBAD  16139  issubm  16300  cycsubg  16551  isnsg  16552  subgacs  16558  nsgacs  16559  resghm  16605  ghmeql  16611  gsmsymgreq  16779  f1otrspeq  16794  pmtrval  16798  pmtrdifellem4  16826  pmtrprfval  16834  gsumzsplit  17266  gsumzsplitOLD  17267  pgpfac1lem1  17443  pgpfac1lem5  17448  pgpfac1  17449  issubrg  17747  islss  17899  lssacs  17931  lspsneq0  17976  lmhmeql  18019  lspdisjb  18090  lidl1el  18184  lidldvgen  18221  0ring01eq  18237  mplcoe1  18445  mplcoe5  18449  mplcoe2OLD  18451  islindf4  19163  m1detdiag  19389  mdetunilem9  19412  maducoeval2  19432  madugsum  19435  chpmat1dlem  19626  istopg  19694  fiinbas  19743  topbas  19764  ppttop  19798  pptbas  19799  epttop  19800  elcls  19865  clsndisj  19867  elcls3  19875  iscldtop  19887  neiptopnei  19924  restbas  19950  restntr  19974  pnfnei  20012  mnfnei  20013  cnpimaex  20048  lmcvg  20054  iscnp4  20055  cncnpi  20070  cnconst2  20075  cnprest  20081  cnprest2  20082  cnpdis  20085  lmss  20090  lmff  20093  cnt0  20138  ist1-3  20141  cnhaus  20146  isreg2  20169  dishaus  20174  ordthauslem  20175  cmpsublem  20190  cmpsub  20191  cmpcld  20193  hauscmplem  20197  uncon  20220  concompid  20222  concompcon  20223  concompss  20224  1stcfb  20236  1stcrest  20244  2ndcctbss  20246  2ndcomap  20249  dis2ndc  20251  1stcelcls  20252  llyeq  20261  nllyeq  20262  restnlly  20273  restlly  20274  islly2  20275  lly1stc  20287  dislly  20288  hauspwdom  20292  finlocfin  20311  unisngl  20318  dissnlocfin  20320  locfindis  20321  comppfsc  20323  llycmpkgen2  20341  txbas  20358  eltx  20359  ptpjopn  20403  ptclsg  20406  dfac14lem  20408  txcnp  20411  ptcnplem  20412  ptcnp  20413  txlly  20427  pthaus  20429  txtube  20431  txhaus  20438  txlm  20439  tx1stc  20441  txkgen  20443  xkohaus  20444  xkopt  20446  xkococnlem  20450  tgqtop  20503  kqfvima  20521  kqt0lem  20527  isr0  20528  r0cld  20529  regr1lem  20530  kqreglem1  20532  kqreglem2  20533  reghmph  20584  fbssfi  20628  isfil  20638  filuni  20676  isufil  20694  isufil2  20699  uffix  20712  fixufil  20713  uffixfr  20714  uffixsn  20716  rnelfm  20744  flimopn  20766  flimrest  20774  flimcls  20776  flftg  20787  txflf  20797  fclsopni  20806  fclsrest  20815  fclscf  20816  fcfnei  20826  alexsublem  20834  alexsubALTlem3  20839  alexsubALT  20841  tmdgsum2  20885  symgtgp  20890  subgntr  20895  opnsubg  20896  tgpconcompeqg  20900  ghmcnp  20903  tgpt0  20907  qustgpopn  20908  tsmsi  20922  tsmssubm  20934  tsmssplit  20944  isust  20996  ustn0  21013  blssps  21217  blss  21218  blssexps  21219  blssex  21220  neibl  21294  blcld  21298  metss  21301  methaus  21313  met1stc  21314  met2ndci  21315  metrest  21317  prdsxmslem2  21322  metcnp3  21333  dscopn  21384  idnghm  21540  qdensere  21567  tgioo  21591  tgqioo  21595  zdis  21611  xrge0tsms  21629  cnheibor  21745  lmmbr  21987  bcthlem4  22056  ovolicc2lem5  22222  dyadmbllem  22298  i1fd  22378  itg11  22388  itg2gt0  22457  itgeq1f  22468  bddmulibl  22535  ellimc2  22571  limcnlp  22572  ellimc3  22573  limcflf  22575  limciun  22588  lhop1lem  22704  ig1pdvds  22867  plycpn  22975  aannenlem2  23015  efopn  23331  xrlimcnp  23622  wilthlem2  23722  wilthlem3  23723  wilth  23724  tghilberti1  24400  tghilberti2  24401  colline  24413  lmif  24534  islmib  24536  usgra2edg  24786  usgraedg4  24791  nbgraf1olem1  24845  nbgraf1olem3  24847  nb3graprlem1  24855  nb3graprlem2  24856  uvtx01vtx  24896  uvtxnbgravtx  24899  2trllemF  24955  wlkntrl  24968  constr1trl  24994  eleclclwwlkn  25237  vdgr1a  25310  vdusgra0nedg  25312  usgravd0nedg  25322  eupath2lem1  25381  vdn0frgrav2  25427  vdgn0frgrav2  25428  frgrancvvdeqlem4  25437  frgrancvvdeqlem7  25440  frgrancvvdeqlemA  25441  frgrancvvdeqlemC  25443  frgrawopreg1  25454  frgrawopreg2  25455  lpni  25585  rngoueqz  25832  issh  26525  pjoc1  26752  h1dn0  26870  spansneleqi  26887  nonbooli  26969  pjch  27012  pjnel  27044  cdjreui  27750  rexunirn  27791  rabsnel  27803  opabdm  27887  opabrn  27888  fpwrelmapffslem  27988  fpwrelmap  27989  fz1nntr  28041  xrge0tsmsd  28214  reff  28281  tpr2rico  28333  lmxrge0  28373  indval  28447  issiga  28545  isrnsigaOLD  28546  isrnsiga  28547  isldsys  28590  isros  28602  issros  28609  ddeval1  28669  ddeval0  28670  ddemeas  28671  ismbfm  28686  isanmbfm  28690  dya2icoseg  28711  dya2iocnrect  28715  ballotlem7  28966  bnj145OLD  29096  bnj216  29101  bnj563  29114  bnj956  29149  bnj545  29267  bnj548  29269  bnj570  29277  bnj900  29301  bnj929  29308  bnj964  29315  bnj983  29323  bnj1001  29330  bnj1145  29363  bnj1398  29404  bnj1498  29431  erdszelem1  29475  kur14lem9  29498  cnllyscon  29529  cvmcov  29547  cvmsss2  29558  cvmcov2  29559  cvmseu  29560  cvmsiota  29561  cvmopnlem  29562  cvmliftlem15  29582  mclsssvlem  29761  mclsind  29769  untelirr  29896  untsucf  29898  dfon2lem4  29992  dfon2lem7  29995  dfon2lem9  29997  soseq  30052  frrlem4  30077  frrlem5e  30082  frrlem11  30086  nodenselem8  30135  nocvxminlem  30137  nofulllem5  30153  dfiota3  30248  funpartlem  30267  funpartfun  30268  linethru  30478  hilbert1.1  30479  hilbert1.2  30480  rankelg  30493  elhf2  30500  fneint  30563  neibastop2lem  30575  bj-rabeqd  31039  bj-cleq  31071  bj-snsetex  31073  bj-nuliota  31138  bj-elopg  31154  mptsnunlem  31241  isbasisrelowllem1  31259  isbasisrelowllem2  31260  relowlssretop  31266  fin2so  31392  heicant  31401  mblfinlem1  31403  ftc1anc  31451  ftc2nc  31452  cover2  31466  isbnd2  31541  prdstotbnd  31552  heibor1lem  31567  grpokerinj  31609  isidl  31673  1idl  31685  0rngo  31686  ispridl  31693  smprngopr  31711  isfldidl  31727  isdmn3  31733  mpt2bi123f  31833  iineq12f  31835  mptbi12f  31837  lsateln0  31993  ispsubsp  32742  linepsubN  32749  elpcliN  32890  dvh3dim3N  34449  dochsnnz  34450  mapdindp3  34722  elmzpcl  35000  diophren  35088  dford3lem2  35311  ttac  35320  pw2f1ocnv  35321  wepwsolem  35329  kelac1  35351  sdrgacs  35494  eliunov2  35638  expgrowthi  36066  dvconstbi  36067  tratrb  36307  suctrALT2VD  36646  suctrALT2  36647  en3lplem1VD  36653  en3lpVD  36655  tratrbVD  36672  suctrALTcf  36733  suctrALTcfVD  36734  suctrALT3  36735  unisnALT  36737  elunif  36751  fnchoice  36764  icccncfext  37039  stoweidlem27  37158  stoweidlem35  37166  stoweidlem46  37177  stoweidlem52  37183  funressnfv  37562  fnbrafvb  37588  afvco2  37610  ndmaovg  37618  aovmpt4g  37635  nnsum4primeseven  37829  nnsum4primesevenALTV  37830  fzoopth  37952  usgpredgv  38009  usgvincvad  38014  usgvincvadALT  38017  usgvad2edg  38021  usg2edgneu  38022  usgedgvadf1lem1  38023  usgedgvadf1lem2  38024  usgedgvadf1ALTlem1  38026  usgedgvadf1ALTlem2  38027  usgedgleord  38029  usgedgleordALT  38030  issubmgm  38087  c0snmgmhm  38212  c0snmhm  38213  rngccatidALTV  38289  ringccatidALTV  38352  ldepspr  38566
  Copyright terms: Public domain W3C validator