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

Theorem eleq2 2516
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 2513 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438
This theorem is referenced by:  eleq12  2519  eleq2i  2521  eleq2dOLD  2524  nelneq2  2561  dvelimdc  2628  nelne1  2772  neleq2OLD  2784  raleqf  3036  rexeqf  3037  reueq1f  3038  rmoeq1f  3039  rabeqf  3088  clel3g  3223  clel4  3225  sbcbi2  3364  sbcel2gv  3380  csbeq2  3424  difeq2  3601  uneq1  3636  ineq1  3678  unineq  3733  n0i  3775  sbnfc2  3840  disjel  3859  elif  3966  exsnrex  4052  sneqr  4182  preqr1  4189  preq12b  4191  prel12  4192  elunii  4239  eluniab  4245  ssuni  4256  elinti  4280  elintab  4282  intss1  4286  intmin  4291  intab  4302  iineq2  4333  dfiin2g  4348  breq  4439  zfrepclf  4554  axsep2  4559  zfauscl  4560  sseliALT  4568  inuni  4599  pwne0  4607  elALT  4680  rext  4685  intid  4695  opth1  4710  opthwiener  4739  ordtri1  4901  ordtri3  4904  nsuceq0  4948  suctr  4951  ordnbtwn  4958  xpeq1  5003  xpeq2  5004  opthprc  5037  funopg  5610  dffv2  5931  fveqdmss  6011  dffo4  6032  fnsnb  6075  elunirn  6148  f1oiso  6232  canth  6239  eusvobj2  6274  mpt2eq123  6341  ndmovg  6443  snnex  6591  uniuni  6594  iunpw  6599  oneqmin  6625  onuninsuci  6660  nlimsucg  6662  limomss  6690  nnlim  6698  peano5  6708  unielxp  6821  cnvf1o  6884  smoel  7033  smo11  7037  tz7.44-2  7075  oawordeulem  7205  oaordex  7209  omordi  7217  oneo  7232  oeordi  7238  oeoa  7248  oeoe  7250  nnmordi  7282  nnaordex  7289  omabs  7298  nnneo  7302  omsmolem  7304  elqsn0  7382  qsel  7392  mapsn  7462  undifixp  7507  boxriin  7513  boxcutc  7514  fineqvlem  7736  fineqv  7737  pssnn  7740  fissuni  7827  dffi2  7885  inficl  7887  dffi3  7893  wofib  7973  zfregcl  8023  en3lplem1  8034  en3lp  8036  suc11reg  8039  inf0  8041  inf3lem2  8049  inf3lem3  8050  infeq5i  8056  axinf2  8060  dfom3  8067  elom3  8068  noinfepOLD  8080  cantnfle  8093  oemapvali  8106  cantnflem1c  8109  cantnflem1  8111  cantnfleOLD  8123  cantnflem1cOLD  8132  cantnflem1OLD  8134  tc2  8176  r1sdom  8195  rankwflemb  8214  rankval3b  8247  rankunb  8271  rankuni2b  8274  tcrank  8305  cardlim  8356  cardprclem  8363  infxpenlem  8394  alephnbtwn  8455  alephordi  8458  cardaleph  8473  alephfp  8492  alephval3  8494  aceq1  8501  aceq2  8503  dfac3  8505  dfac5lem2  8508  dfac5lem4  8510  dfac2  8514  kmlem2  8534  kmlem4  8536  coflim  8644  cfsmolem  8653  fin23lem30  8725  isf32lem2  8737  isf34lem4  8760  axdc2lem  8831  axdc3lem2  8834  axdc3lem4  8836  axdc4lem  8838  zorn2lem7  8885  axdclem  8902  brdom7disj  8912  brdom6disj  8913  axpowndlem3  8978  axpowndlem3OLD  8979  winainflem  9074  iswun  9085  eltskg  9131  inar1  9156  elgrug  9173  inaprc  9217  eltskm  9224  addnidpi  9282  indpi  9288  nqereu  9310  elnp  9368  elnpi  9369  genpnnp  9386  ltaddpr  9415  dfnn2  10556  dfnn3  10557  dfuzi  10960  uz11  11113  elfzonlteqm1  11872  om2uzlti  12042  axdc4uz  12074  hashrabsn1  12423  hashbclem  12482  hashf1lem2  12486  hash2prd  12499  hash2prv  12506  wrdsymb0  12556  lsw0  12567  prodeq1f  13696  rpnnen2lem1  13929  rpnnen2lem2  13930  sadcp1  14086  ismre  14968  isacs  15029  clatl  15724  mreclatBAD  15795  issubm  15956  cycsubg  16207  isnsg  16208  subgacs  16214  nsgacs  16215  resghm  16261  ghmeql  16267  gsmsymgreq  16435  f1otrspeq  16450  pmtrval  16454  pmtrdifellem4  16482  pmtrprfval  16490  gsumzsplit  16922  gsumzsplitOLD  16923  pgpfac1lem1  17103  pgpfac1lem5  17108  pgpfac1  17109  issubrg  17407  islss  17559  lssacs  17591  lspsneq0  17636  lmhmeql  17679  lspdisjb  17750  lidl1el  17844  lidldvgen  17881  0ring01eq  17897  mplcoe1  18105  mplcoe5  18109  mplcoe2OLD  18111  islindf4  18850  m1detdiag  19076  mdetunilem9  19099  maducoeval2  19119  madugsum  19122  chpmat1dlem  19313  istopg  19381  fiinbas  19430  topbas  19451  ppttop  19485  pptbas  19486  epttop  19487  elcls  19551  clsndisj  19553  elcls3  19561  iscldtop  19573  neiptopnei  19610  restbas  19636  restntr  19660  pnfnei  19698  mnfnei  19699  cnpimaex  19734  lmcvg  19740  iscnp4  19741  cncnpi  19756  cnconst2  19761  cnprest  19767  cnprest2  19768  cnpdis  19771  lmss  19776  lmff  19779  cnt0  19824  ist1-3  19827  cnhaus  19832  isreg2  19855  dishaus  19860  ordthauslem  19861  cmpsublem  19876  cmpsub  19877  cmpcld  19879  hauscmplem  19883  bwthOLD  19888  uncon  19907  concompid  19909  concompcon  19910  concompss  19911  1stcfb  19923  1stcrest  19931  2ndcctbss  19933  2ndcomap  19936  dis2ndc  19938  1stcelcls  19939  llyeq  19948  nllyeq  19949  restnlly  19960  restlly  19961  islly2  19962  lly1stc  19974  dislly  19975  hauspwdom  19979  finlocfin  19998  unisngl  20005  dissnlocfin  20007  locfindis  20008  comppfsc  20010  llycmpkgen2  20028  txbas  20045  eltx  20046  ptpjopn  20090  ptclsg  20093  dfac14lem  20095  txcnp  20098  ptcnplem  20099  ptcnp  20100  txlly  20114  pthaus  20116  txtube  20118  txhaus  20125  txlm  20126  tx1stc  20128  txkgen  20130  xkohaus  20131  xkopt  20133  xkococnlem  20137  tgqtop  20190  kqfvima  20208  kqt0lem  20214  isr0  20215  r0cld  20216  regr1lem  20217  kqreglem1  20219  kqreglem2  20220  reghmph  20271  fbssfi  20315  isfil  20325  filuni  20363  isufil  20381  isufil2  20386  uffix  20399  fixufil  20400  uffixfr  20401  uffixsn  20403  rnelfm  20431  flimopn  20453  flimrest  20461  flimcls  20463  flftg  20474  txflf  20484  fclsopni  20493  fclsrest  20502  fclscf  20503  fcfnei  20513  alexsublem  20521  alexsubALTlem3  20526  alexsubALT  20528  tmdgsum2  20572  symgtgp  20577  subgntr  20582  opnsubg  20583  tgpconcompeqg  20587  ghmcnp  20590  tgpt0  20594  qustgpopn  20595  tsmsi  20609  tsmssubm  20621  tsmssplit  20631  isust  20683  ustn0  20700  blssps  20904  blss  20905  blssexps  20906  blssex  20907  neibl  20981  blcld  20985  metss  20988  methaus  21000  met1stc  21001  met2ndci  21002  metrest  21004  prdsxmslem2  21009  metcnp3  21020  dscopn  21071  idnghm  21227  qdensere  21254  tgioo  21278  tgqioo  21282  zdis  21298  xrge0tsms  21316  cnheibor  21432  lmmbr  21674  bcthlem4  21743  ovolicc2lem5  21909  dyadmbllem  21985  i1fd  22065  itg11  22075  itg2gt0  22144  itgeq1f  22155  bddmulibl  22222  ellimc2  22258  limcnlp  22259  ellimc3  22260  limcflf  22262  limciun  22275  lhop1lem  22391  ig1pdvds  22554  plycpn  22661  aannenlem2  22701  efopn  23015  xrlimcnp  23274  wilthlem2  23319  wilthlem3  23320  wilth  23321  tghilbert1_1  23993  tghilbert1_2  23994  colline  24006  lmif  24127  islmib  24129  usgra2edg  24358  usgraedg4  24363  nbgraf1olem1  24417  nbgraf1olem3  24419  nb3graprlem1  24427  nb3graprlem2  24428  uvtx01vtx  24468  uvtxnbgravtx  24471  2trllemF  24527  wlkntrl  24540  constr1trl  24566  eleclclwwlkn  24809  vdgr1a  24882  vdusgra0nedg  24884  usgravd0nedg  24894  eupath2lem1  24953  vdn0frgrav2  24999  vdgn0frgrav2  25000  frgrancvvdeqlem4  25009  frgrancvvdeqlem7  25012  frgrancvvdeqlemA  25013  frgrancvvdeqlemC  25015  frgrawopreg1  25026  frgrawopreg2  25027  lpni  25157  rngoueqz  25408  issh  26101  pjoc1  26328  h1dn0  26446  spansneleqi  26463  nonbooli  26545  pjch  26588  pjnel  26620  cdjreui  27327  rexunirn  27366  rabsnel  27378  opabdm  27440  opabrn  27441  fpwrelmapffslem  27531  fpwrelmap  27532  xrge0tsmsd  27752  reff  27819  tpr2rico  27871  lmxrge0  27911  indval  28004  issiga  28088  isrnsigaOLD  28089  isrnsiga  28090  ddeval1  28183  ddeval0  28184  ddemeas  28185  ismbfm  28200  isanmbfm  28204  dya2icoseg  28225  dya2iocnrect  28229  ballotlem7  28451  erdszelem1  28612  kur14lem9  28635  cnllyscon  28667  cvmcov  28685  cvmsss2  28696  cvmcov2  28697  cvmseu  28698  cvmsiota  28699  cvmopnlem  28700  cvmliftlem15  28720  mclsssvlem  28899  mclsind  28907  rtrclreclem.trans  29046  untelirr  29057  untsucf  29059  dfon2lem4  29193  dfon2lem7  29196  dfon2lem9  29198  soseq  29309  frrlem4  29365  frrlem5e  29370  frrlem11  29374  nodenselem8  29423  nocvxminlem  29425  nofulllem5  29441  dfiota3  29548  funpartlem  29567  funpartfun  29568  tfrqfree  29576  linethru  29778  hilbert1.1  29779  hilbert1.2  29780  rankelg  29800  elhf2  29807  fin2so  30015  heicant  30024  mblfinlem1  30026  ftc1anc  30073  ftc2nc  30074  fneint  30141  neibastop2lem  30153  cover2  30179  isbnd2  30254  prdstotbnd  30265  heibor1lem  30280  grpokerinj  30322  isidl  30386  1idl  30398  0rngo  30399  ispridl  30406  smprngopr  30424  isfldidl  30440  isdmn3  30446  mpt2bi123f  30546  iineq12f  30548  mptbi12f  30550  elmzpcl  30633  diophren  30722  dford3lem2  30944  ttac  30953  pw2f1ocnv  30954  wepwsolem  30962  kelac1  30984  sdrgacs  31126  expgrowthi  31214  dvconstbi  31215  elunif  31345  fnchoice  31358  icccncfext  31597  stoweidlem27  31698  stoweidlem35  31706  stoweidlem46  31717  stoweidlem52  31723  funressnfv  32051  fnbrafvb  32077  afvco2  32099  ndmaovg  32107  aovmpt4g  32124  fzoopth  32178  usgpredgv  32237  usgvincvad  32242  usgvincvadALT  32245  usgvad2edg  32249  usg2edgneu  32250  usgedgvadf1lem1  32251  usgedgvadf1lem2  32252  usgedgvadf1ALTlem1  32254  usgedgvadf1ALTlem2  32255  usgedgleord  32257  usgedgleordALT  32258  issubmgm  32315  rngccatidOLD  32537  ringccatidOLD  32597  ldepspr  32809  tratrb  33040  suctrALT2VD  33369  suctrALT2  33370  en3lplem1VD  33376  en3lpVD  33378  tratrbVD  33394  suctrALTcf  33455  suctrALTcfVD  33456  suctrALT3  33457  unisnALT  33459  bnj145OLD  33515  bnj216  33520  bnj563  33533  bnj956  33568  bnj545  33686  bnj548  33688  bnj570  33696  bnj900  33720  bnj929  33727  bnj964  33734  bnj983  33742  bnj1001  33749  bnj1145  33782  bnj1398  33823  bnj1498  33850  bj-rabeqd  34236  bj-cleq  34267  bj-snsetex  34269  bj-nuliota  34334  bj-elopg  34342  lsateln0  34460  ispsubsp  35209  linepsubN  35216  elpcliN  35357  dvh3dim3N  36916  dochsnnz  36917  mapdindp3  37189
  Copyright terms: Public domain W3C validator