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

Theorem eleq2 2496
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 23 . 2  |-  ( A  =  B  ->  A  =  B )
21eleq2d 2493 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438    e. wcel 1869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-cleq 2415  df-clel 2418
This theorem is referenced by:  eleq12  2499  eleq2i  2501  eleq2dOLD  2504  nelneq2  2541  dvelimdc  2608  nelne1  2754  neleq2OLD  2767  raleqf  3022  rexeqf  3023  reueq1f  3024  rmoeq1f  3025  rabeqf  3074  clel3g  3210  clel4  3212  sbcbi2  3349  sbcel2gv  3360  csbeq2  3400  difeq2  3578  uneq1  3614  ineq1  3658  unineq  3724  n0i  3767  sbnfc2  3825  disjel  3840  elif  3950  exsnrex  4035  sneqr  4165  preqr1  4172  preq12b  4174  prel12  4175  elunii  4222  eluniab  4228  ssuni  4239  elinti  4262  elintab  4264  intss1  4268  intmin  4273  intab  4284  iineq2  4315  dfiin2g  4330  breq  4423  zfrepclf  4540  axsep2  4545  zfauscl  4546  sseliALT  4555  inuni  4584  pwne0  4592  elALT  4662  rext  4667  intid  4677  opth1  4692  opthwiener  4720  xpeq1  4865  xpeq2  4866  opthprc  4899  ordtri1  5473  ordtri3  5476  nsuceq0  5520  suctr  5523  ordnbtwn  5530  funopg  5631  dffv2  5952  fveqdmss  6030  dffo4  6051  fnsnb  6096  elunirn  6169  f1oiso  6255  canth  6262  eusvobj2  6296  mpt2eq123  6362  ndmovg  6464  snnex  6609  uniuni  6612  iunpw  6617  oneqmin  6644  onuninsuci  6679  nlimsucg  6681  limomss  6709  nnlim  6717  peano5  6728  unielxp  6841  cnvf1o  6904  smoel  7085  smo11  7089  tz7.44-2  7131  oawordeulem  7261  oaordex  7265  omordi  7273  oneo  7288  oeordi  7294  oeoa  7304  oeoe  7306  nnmordi  7338  nnaordex  7345  omabs  7354  nnneo  7358  omsmolem  7360  elqsn0  7438  qsel  7448  mapsn  7519  undifixp  7564  boxriin  7570  boxcutc  7571  fineqvlem  7790  fineqv  7791  pssnn  7794  fissuni  7883  dffi2  7941  inficl  7943  dffi3  7949  wofib  8064  zfregcl  8113  en3lplem1  8123  en3lp  8125  suc11reg  8128  inf0  8130  inf3lem2  8138  inf3lem3  8139  infeq5i  8145  axinf2  8149  dfom3  8156  elom3  8157  cantnfle  8179  oemapvali  8192  cantnflem1c  8195  cantnflem1  8197  tc2  8229  r1sdom  8248  rankwflemb  8267  rankval3b  8300  rankunb  8324  rankuni2b  8327  tcrank  8358  cardlim  8409  cardprclem  8416  infxpenlem  8447  alephnbtwn  8504  alephordi  8507  cardaleph  8522  alephfp  8541  alephval3  8543  aceq1  8550  aceq2  8552  dfac3  8554  dfac5lem2  8557  dfac5lem4  8559  dfac2  8563  kmlem2  8583  kmlem4  8585  coflim  8693  cfsmolem  8702  fin23lem30  8774  isf32lem2  8786  isf34lem4  8809  axdc2lem  8880  axdc3lem2  8883  axdc3lem4  8885  axdc4lem  8887  zorn2lem7  8934  axdclem  8951  brdom7disj  8961  brdom6disj  8962  axpowndlem3  9026  winainflem  9120  iswun  9131  eltskg  9177  inar1  9202  elgrug  9219  inaprc  9263  eltskm  9270  addnidpi  9328  indpi  9334  nqereu  9356  elnp  9414  elnpi  9415  genpnnp  9432  ltaddpr  9461  dfnn2  10624  dfnn3  10625  dfuzi  11028  uz11  11183  elfzonlteqm1  11990  om2uzlti  12165  axdc4uz  12197  hashrabsn1  12554  hashbclem  12614  hashf1lem2  12618  hash2prd  12632  hash2prv  12641  wrdsymb0  12699  lsw0  12710  rtrclreclem3  13117  prodeq1f  13955  rpnnen2lem1  14260  rpnnen2lem2  14261  sadcp1  14422  lcmfval  14584  lcmf0val  14585  lcmfvalOLD  14588  ismre  15489  isacs  15550  initoid  15893  termoid  15894  initoeu2lem1  15902  clatl  16355  mreclatBAD  16426  issubm  16587  cycsubg  16838  isnsg  16839  subgacs  16845  nsgacs  16846  resghm  16892  ghmeql  16898  gsmsymgreq  17066  f1otrspeq  17081  pmtrval  17085  pmtrdifellem4  17113  pmtrprfval  17121  gsumzsplit  17553  pgpfac1lem1  17700  pgpfac1lem5  17705  pgpfac1  17706  issubrg  18001  islss  18151  lssacs  18183  lspsneq0  18228  lmhmeql  18271  lspdisjb  18342  lidl1el  18435  lidldvgen  18472  0ring01eq  18488  mplcoe1  18682  mplcoe5  18685  islindf4  19388  m1detdiag  19614  mdetunilem9  19637  maducoeval2  19657  madugsum  19660  chpmat1dlem  19851  istopg  19917  fiinbas  19959  topbas  19980  ppttop  20014  pptbas  20015  epttop  20016  elcls  20081  clsndisj  20083  elcls3  20091  iscldtop  20103  neiptopnei  20140  restbas  20166  restntr  20190  pnfnei  20228  mnfnei  20229  cnpimaex  20264  lmcvg  20270  iscnp4  20271  cncnpi  20286  cnconst2  20291  cnprest  20297  cnprest2  20298  cnpdis  20301  lmss  20306  lmff  20309  cnt0  20354  ist1-3  20357  cnhaus  20362  isreg2  20385  dishaus  20390  ordthauslem  20391  cmpsublem  20406  cmpsub  20407  cmpcld  20409  hauscmplem  20413  uncon  20436  concompid  20438  concompcon  20439  concompss  20440  1stcfb  20452  1stcrest  20460  2ndcctbss  20462  2ndcomap  20465  dis2ndc  20467  1stcelcls  20468  llyeq  20477  nllyeq  20478  restnlly  20489  restlly  20490  islly2  20491  lly1stc  20503  dislly  20504  hauspwdom  20508  finlocfin  20527  unisngl  20534  dissnlocfin  20536  locfindis  20537  comppfsc  20539  llycmpkgen2  20557  txbas  20574  eltx  20575  ptpjopn  20619  ptclsg  20622  dfac14lem  20624  txcnp  20627  ptcnplem  20628  ptcnp  20629  txlly  20643  pthaus  20645  txtube  20647  txhaus  20654  txlm  20655  tx1stc  20657  txkgen  20659  xkohaus  20660  xkopt  20662  xkococnlem  20666  tgqtop  20719  kqfvima  20737  kqt0lem  20743  isr0  20744  r0cld  20745  regr1lem  20746  kqreglem1  20748  kqreglem2  20749  reghmph  20800  fbssfi  20844  isfil  20854  filuni  20892  isufil  20910  isufil2  20915  uffix  20928  fixufil  20929  uffixfr  20930  uffixsn  20932  rnelfm  20960  flimopn  20982  flimrest  20990  flimcls  20992  flftg  21003  txflf  21013  fclsopni  21022  fclsrest  21031  fclscf  21032  fcfnei  21042  alexsublem  21051  alexsubALTlem3  21056  alexsubALT  21058  tmdgsum2  21103  symgtgp  21108  subgntr  21113  opnsubg  21114  tgpconcompeqg  21118  ghmcnp  21121  tgpt0  21125  qustgpopn  21126  tsmsi  21140  tsmssubm  21149  tsmssplit  21158  isust  21210  ustn0  21227  blssps  21431  blss  21432  blssexps  21433  blssex  21434  neibl  21508  blcld  21512  metss  21515  methaus  21527  met1stc  21528  met2ndci  21529  metrest  21531  prdsxmslem2  21536  metcnp3  21547  dscopn  21580  idnghm  21756  qdensere  21782  tgioo  21806  tgqioo  21810  zdis  21826  xrge0tsms  21844  cnheibor  21975  lmmbr  22220  bcthlem4  22287  ovolicc2lem5  22467  dyadmbllem  22549  i1fd  22631  itg11  22641  itg2gt0  22710  itgeq1f  22721  bddmulibl  22788  ellimc2  22824  limcnlp  22825  ellimc3  22826  limcflf  22828  limciun  22841  lhop1lem  22957  ig1pdvds  23120  ig1pdvdsOLD  23126  plycpn  23234  aannenlem2  23277  efopn  23595  xrlimcnp  23886  wilthlem2  23986  wilthlem3  23987  wilth  23988  tghilberti1  24674  tghilberti2  24675  colline  24686  lmif  24819  islmib  24821  usgra2edg  25101  usgraedg4  25106  nbgraf1olem1  25161  nbgraf1olem3  25163  nb3graprlem1  25171  nb3graprlem2  25172  uvtx01vtx  25212  uvtxnbgravtx  25215  2trllemF  25271  wlkntrl  25284  constr1trl  25310  eleclclwwlkn  25553  vdgr1a  25626  vdusgra0nedg  25628  usgravd0nedg  25638  eupath2lem1  25697  vdn0frgrav2  25743  vdgn0frgrav2  25744  frgrancvvdeqlem4  25753  frgrancvvdeqlem7  25756  frgrancvvdeqlemA  25757  frgrancvvdeqlemC  25759  frgrawopreg1  25770  frgrawopreg2  25771  lpni  25903  rngoueqz  26150  issh  26853  pjoc1  27079  h1dn0  27197  spansneleqi  27214  nonbooli  27296  pjch  27339  pjnel  27371  cdjreui  28077  rexunirn  28119  rabsnel  28131  opabdm  28215  opabrn  28216  fpwrelmapffslem  28317  fpwrelmap  28318  fz1nntr  28378  xrge0tsmsd  28550  reff  28668  tpr2rico  28720  lmxrge0  28760  indval  28837  issiga  28935  isrnsigaOLD  28936  isrnsiga  28937  isldsys  28980  isros  28992  issros  28999  ddeval1  29059  ddeval0  29060  ddemeas  29061  ismbfm  29076  isanmbfm  29080  dya2icoseg  29101  dya2iocnrect  29105  ballotlem7  29370  ballotlem7OLD  29408  bnj145OLD  29537  bnj216  29542  bnj563  29555  bnj956  29590  bnj545  29708  bnj548  29710  bnj570  29718  bnj900  29742  bnj929  29749  bnj964  29756  bnj983  29764  bnj1001  29771  bnj1145  29804  bnj1398  29845  bnj1498  29872  erdszelem1  29916  kur14lem9  29939  cnllyscon  29970  cvmcov  29988  cvmsss2  29999  cvmcov2  30000  cvmseu  30001  cvmsiota  30002  cvmopnlem  30003  cvmliftlem15  30023  mclsssvlem  30202  mclsind  30210  untelirr  30337  untsucf  30339  dfon2lem4  30433  dfon2lem7  30436  dfon2lem9  30438  soseq  30493  frrlem4  30518  frrlem5e  30523  frrlem11  30527  nodenselem8  30576  nocvxminlem  30578  nofulllem5  30594  dfiota3  30689  funpartlem  30708  funpartfun  30709  linethru  30919  hilbert1.1  30920  hilbert1.2  30921  rankelg  30934  elhf2  30941  fneint  31003  neibastop2lem  31015  bj-rabeqd  31486  bj-cleq  31517  bj-snsetex  31519  bj-nuliota  31584  bj-elopg  31600  mptsnunlem  31687  isbasisrelowllem1  31705  isbasisrelowllem2  31706  relowlssretop  31713  relowlpssretop  31714  fin2so  31852  ptrecube  31860  poimirlem9  31869  poimirlem30  31890  poimir  31893  heicant  31895  mblfinlem1  31897  ftc1anc  31945  ftc2nc  31946  cover2  31960  isbnd2  32035  prdstotbnd  32046  heibor1lem  32061  grpokerinj  32103  isidl  32167  1idl  32179  0rngo  32180  ispridl  32187  smprngopr  32205  isfldidl  32221  isdmn3  32227  mpt2bi123f  32326  iineq12f  32328  mptbi12f  32330  lsateln0  32486  ispsubsp  33235  linepsubN  33242  elpcliN  33383  dvh3dim3N  34942  dochsnnz  34943  mapdindp3  35215  elmzpcl  35493  diophren  35581  dford3lem2  35808  ttac  35817  pw2f1ocnv  35818  wepwsolem  35826  kelac1  35847  sdrgacs  35993  eliunov2  36137  expgrowthi  36546  dvconstbi  36547  tratrb  36761  suctrALT2VD  37099  suctrALT2  37100  en3lplem1VD  37106  en3lpVD  37108  tratrbVD  37125  suctrALTcf  37186  suctrALTcfVD  37187  suctrALT3  37188  unisnALT  37190  elunif  37204  fnchoice  37217  icccncfext  37591  stoweidlem27  37713  stoweidlem35  37722  stoweidlem46  37733  stoweidlem52  37739  issal  37982  intsaluni  37995  sge0f1o  38018  funressnfv  38348  fnbrafvb  38374  afvco2  38396  ndmaovg  38404  aovmpt4g  38421  nnsum4primeseven  38613  nnsum4primesevenALTV  38614  fundmge2nop  38730  fzoopth  38758  umgr1opALT  38860  usgr2edg  38916  usgredg4  38921  usgredg2vtx  38923  usgredg2vtxeuALT  38925  usgredgedga  38931  usgredgaleord  38932  usgpredgv  39015  usgvincvad  39020  usgvincvadALT  39023  usgvad2edg  39027  usg2edgneu  39028  usgedgvadf1lem1  39029  usgedgvadf1lem2  39030  usgedgvadf1ALTlem1  39032  usgedgvadf1ALTlem2  39033  usgedgleord  39035  usgedgleordALT  39036  issubmgm  39093  c0snmgmhm  39218  c0snmhm  39219  rngccatidALTV  39295  ringccatidALTV  39358  ldepspr  39572
  Copyright terms: Public domain W3C validator