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

Theorem eleq2 2518
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 2514 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1444    e. wcel 1887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-cleq 2444  df-clel 2447
This theorem is referenced by:  eleq12  2519  eleq2i  2521  nelneq2  2554  dvelimdc  2613  nelne1  2720  raleqf  2983  rexeqf  2984  reueq1f  2985  rmoeq1f  2986  raleleq  3005  rabeqf  3037  clel3g  3176  clel4  3178  sbcbi2  3316  sbcel2gv  3327  csbeq2  3367  difeq2  3545  uneq1  3581  ineq1  3627  unineq  3693  n0i  3736  sbnfc2  3796  disjel  3811  elif  3921  exsnrex  4009  sneqr  4139  preq1b  4146  preqr1OLD  4149  preq12b  4151  prel12  4152  elpreqprb  4162  elunii  4203  eluniab  4209  ssuni  4220  elinti  4243  elintab  4245  intss1  4249  intmin  4254  intab  4265  iineq2  4296  dfiin2g  4311  breq  4404  zfrepclf  4521  axsep2  4526  zfauscl  4527  sseliALT  4536  inuni  4565  pwne0  4573  elALT  4643  rext  4648  intid  4658  elopg  4666  opth1  4675  opthwiener  4703  xpeq1  4848  xpeq2  4849  opthprc  4882  ordtri1  5456  ordtri3  5459  nsuceq0  5503  suctr  5506  ordnbtwn  5513  funopg  5614  dffv2  5938  fveqdmss  6017  dffo4  6038  fnsnb  6083  elunirn  6156  f1oiso  6242  canth  6249  eusvobj2  6283  mpt2eq123  6350  ndmovg  6452  snnex  6597  uniuni  6600  iunpw  6605  oneqmin  6632  onuninsuci  6667  nlimsucg  6669  limomss  6697  nnlim  6705  peano5  6716  unielxp  6829  cnvf1o  6895  smoel  7079  smo11  7083  tz7.44-2  7125  oawordeulem  7255  oaordex  7259  omordi  7267  oneo  7282  oeordi  7288  oeoa  7298  oeoe  7300  nnmordi  7332  nnaordex  7339  omabs  7348  nnneo  7352  omsmolem  7354  elqsn0  7432  qsel  7442  mapsn  7513  undifixp  7558  boxriin  7564  boxcutc  7565  fineqvlem  7786  fineqv  7787  pssnn  7790  fissuni  7879  dffi2  7937  inficl  7939  dffi3  7945  wofib  8060  zfregcl  8109  en3lplem1  8119  en3lp  8121  suc11reg  8124  inf0  8126  inf3lem2  8134  inf3lem3  8135  infeq5i  8141  axinf2  8145  dfom3  8152  elom3  8153  cantnfle  8176  oemapvali  8189  cantnflem1c  8192  cantnflem1  8194  tc2  8226  r1sdom  8245  rankwflemb  8264  rankval3b  8297  rankunb  8321  rankuni2b  8324  tcrank  8355  cardlim  8406  cardprclem  8413  infxpenlem  8444  alephnbtwn  8502  alephordi  8505  cardaleph  8520  alephfp  8539  alephval3  8541  aceq1  8548  aceq2  8550  dfac3  8552  dfac5lem2  8555  dfac5lem4  8557  dfac2  8561  kmlem2  8581  kmlem4  8583  coflim  8691  cfsmolem  8700  fin23lem30  8772  isf32lem2  8784  isf34lem4  8807  axdc2lem  8878  axdc3lem2  8881  axdc3lem4  8883  axdc4lem  8885  zorn2lem7  8932  axdclem  8949  brdom7disj  8959  brdom6disj  8960  axpowndlem3  9024  winainflem  9118  iswun  9129  eltskg  9175  inar1  9200  elgrug  9217  inaprc  9261  eltskm  9268  addnidpi  9326  indpi  9332  nqereu  9354  elnp  9412  elnpi  9413  genpnnp  9430  ltaddpr  9459  dfnn2  10622  dfnn3  10623  dfuzi  11026  uz11  11181  elfzonlteqm1  11989  om2uzlti  12164  axdc4uz  12196  hashrabsn1  12553  hashbclem  12615  hashf1lem2  12619  hash2prb  12633  hash2prd  12634  wrdsymb0  12701  lsw0  12712  rtrclreclem3  13123  prodeq1f  13962  rpnnen2lem1  14267  rpnnen2lem2  14268  sadcp1  14429  lcmfval  14591  lcmf0val  14592  lcmfvalOLD  14595  ismre  15496  isacs  15557  initoid  15900  termoid  15901  initoeu2lem1  15909  clatl  16362  mreclatBAD  16433  issubm  16594  cycsubg  16845  isnsg  16846  subgacs  16852  nsgacs  16853  resghm  16899  ghmeql  16905  gsmsymgreq  17073  f1otrspeq  17088  pmtrval  17092  pmtrdifellem4  17120  pmtrprfval  17128  gsumzsplit  17560  pgpfac1lem1  17707  pgpfac1lem5  17712  pgpfac1  17713  issubrg  18008  islss  18158  lssacs  18190  lspsneq0  18235  lmhmeql  18278  lspdisjb  18349  lidl1el  18442  lidldvgen  18479  0ring01eq  18495  mplcoe1  18689  mplcoe5  18692  islindf4  19396  m1detdiag  19622  mdetunilem9  19645  maducoeval2  19665  madugsum  19668  chpmat1dlem  19859  istopg  19925  fiinbas  19967  topbas  19988  ppttop  20022  pptbas  20023  epttop  20024  elcls  20089  clsndisj  20091  elcls3  20099  iscldtop  20111  neiptopnei  20148  restbas  20174  restntr  20198  pnfnei  20236  mnfnei  20237  cnpimaex  20272  lmcvg  20278  iscnp4  20279  cncnpi  20294  cnconst2  20299  cnprest  20305  cnprest2  20306  cnpdis  20309  lmss  20314  lmff  20317  cnt0  20362  ist1-3  20365  cnhaus  20370  isreg2  20393  dishaus  20398  ordthauslem  20399  cmpsublem  20414  cmpsub  20415  cmpcld  20417  hauscmplem  20421  uncon  20444  concompid  20446  concompcon  20447  concompss  20448  1stcfb  20460  1stcrest  20468  2ndcctbss  20470  2ndcomap  20473  dis2ndc  20475  1stcelcls  20476  llyeq  20485  nllyeq  20486  restnlly  20497  restlly  20498  islly2  20499  lly1stc  20511  dislly  20512  hauspwdom  20516  finlocfin  20535  unisngl  20542  dissnlocfin  20544  locfindis  20545  comppfsc  20547  llycmpkgen2  20565  txbas  20582  eltx  20583  ptpjopn  20627  ptclsg  20630  dfac14lem  20632  txcnp  20635  ptcnplem  20636  ptcnp  20637  txlly  20651  pthaus  20653  txtube  20655  txhaus  20662  txlm  20663  tx1stc  20665  txkgen  20667  xkohaus  20668  xkopt  20670  xkococnlem  20674  tgqtop  20727  kqfvima  20745  kqt0lem  20751  isr0  20752  r0cld  20753  regr1lem  20754  kqreglem1  20756  kqreglem2  20757  reghmph  20808  fbssfi  20852  isfil  20862  filuni  20900  isufil  20918  isufil2  20923  uffix  20936  fixufil  20937  uffixfr  20938  uffixsn  20940  rnelfm  20968  flimopn  20990  flimrest  20998  flimcls  21000  flftg  21011  txflf  21021  fclsopni  21030  fclsrest  21039  fclscf  21040  fcfnei  21050  alexsublem  21059  alexsubALTlem3  21064  alexsubALT  21066  tmdgsum2  21111  symgtgp  21116  subgntr  21121  opnsubg  21122  tgpconcompeqg  21126  ghmcnp  21129  tgpt0  21133  qustgpopn  21134  tsmsi  21148  tsmssubm  21157  tsmssplit  21166  isust  21218  ustn0  21235  blssps  21439  blss  21440  blssexps  21441  blssex  21442  neibl  21516  blcld  21520  metss  21523  methaus  21535  met1stc  21536  met2ndci  21537  metrest  21539  prdsxmslem2  21544  metcnp3  21555  dscopn  21588  idnghm  21764  qdensere  21790  tgioo  21814  tgqioo  21818  zdis  21834  xrge0tsms  21852  cnheibor  21983  lmmbr  22228  bcthlem4  22295  ovolicc2lem5  22475  dyadmbllem  22557  i1fd  22639  itg11  22649  itg2gt0  22718  itgeq1f  22729  bddmulibl  22796  ellimc2  22832  limcnlp  22833  ellimc3  22834  limcflf  22836  limciun  22849  lhop1lem  22965  ig1pdvds  23128  ig1pdvdsOLD  23134  plycpn  23242  aannenlem2  23285  efopn  23603  xrlimcnp  23894  wilthlem2  23994  wilthlem3  23995  wilth  23996  tghilberti1  24682  tghilberti2  24683  colline  24694  lmif  24827  islmib  24829  usgra2edg  25109  usgraedg4  25114  nbgraf1olem1  25169  nbgraf1olem3  25171  nb3graprlem1  25179  nb3graprlem2  25180  uvtx01vtx  25220  uvtxnbgravtx  25223  2trllemF  25279  wlkntrl  25292  constr1trl  25318  eleclclwwlkn  25561  vdgr1a  25634  vdusgra0nedg  25636  usgravd0nedg  25646  eupath2lem1  25705  vdn0frgrav2  25751  vdgn0frgrav2  25752  frgrancvvdeqlem4  25761  frgrancvvdeqlem7  25764  frgrancvvdeqlemA  25765  frgrancvvdeqlemC  25767  frgrawopreg1  25778  frgrawopreg2  25779  lpni  25911  rngoueqz  26158  issh  26861  pjoc1  27087  h1dn0  27205  spansneleqi  27222  nonbooli  27304  pjch  27347  pjnel  27379  cdjreui  28085  rexunirn  28127  rabsnel  28138  opabdm  28219  opabrn  28220  fpwrelmapffslem  28317  fpwrelmap  28318  fz1nntr  28378  xrge0tsmsd  28548  reff  28666  tpr2rico  28718  lmxrge0  28758  indval  28835  issiga  28933  isrnsigaOLD  28934  isrnsiga  28935  isldsys  28978  isros  28990  issros  28997  ddeval1  29057  ddeval0  29058  ddemeas  29059  ismbfm  29074  isanmbfm  29078  dya2icoseg  29099  dya2iocnrect  29103  ballotlem7  29368  ballotlem7OLD  29406  bnj145OLD  29535  bnj216  29540  bnj563  29553  bnj956  29588  bnj545  29706  bnj548  29708  bnj570  29716  bnj900  29740  bnj929  29747  bnj964  29754  bnj983  29762  bnj1001  29769  bnj1145  29802  bnj1398  29843  bnj1498  29870  erdszelem1  29914  kur14lem9  29937  cnllyscon  29968  cvmcov  29986  cvmsss2  29997  cvmcov2  29998  cvmseu  29999  cvmsiota  30000  cvmopnlem  30001  cvmliftlem15  30021  mclsssvlem  30200  mclsind  30208  untelirr  30335  untsucf  30337  dfon2lem4  30432  dfon2lem7  30435  dfon2lem9  30437  soseq  30492  frrlem4  30517  frrlem5e  30522  frrlem11  30526  nodenselem8  30577  nocvxminlem  30579  nofulllem5  30595  dfiota3  30690  funpartlem  30709  funpartfun  30710  linethru  30920  hilbert1.1  30921  hilbert1.2  30922  rankelg  30935  elhf2  30942  fneint  31004  neibastop2lem  31016  bj-rabeqd  31523  bj-cleq  31555  bj-snsetex  31557  bj-nuliota  31623  mptsnunlem  31740  isbasisrelowllem1  31758  isbasisrelowllem2  31759  relowlssretop  31766  relowlpssretop  31767  finxpeq1  31778  finxpreclem5  31787  finxpreclem6  31788  fin2so  31932  ptrecube  31940  poimirlem9  31949  poimirlem30  31970  poimir  31973  heicant  31975  mblfinlem1  31977  ftc1anc  32025  ftc2nc  32026  cover2  32040  isbnd2  32115  prdstotbnd  32126  heibor1lem  32141  grpokerinj  32183  isidl  32247  1idl  32259  0rngo  32260  ispridl  32267  smprngopr  32285  isfldidl  32301  isdmn3  32307  mpt2bi123f  32406  iineq12f  32408  mptbi12f  32410  lsateln0  32561  ispsubsp  33310  linepsubN  33317  elpcliN  33458  dvh3dim3N  35017  dochsnnz  35018  mapdindp3  35290  elmzpcl  35568  diophren  35656  dford3lem2  35882  ttac  35891  pw2f1ocnv  35892  wepwsolem  35900  kelac1  35921  sdrgacs  36067  elintabg  36180  elmapintrab  36182  intabssd  36216  eliunov2  36271  expgrowthi  36682  dvconstbi  36683  tratrb  36897  suctrALT2VD  37232  suctrALT2  37233  en3lplem1VD  37239  en3lpVD  37241  tratrbVD  37258  suctrALTcf  37319  suctrALTcfVD  37320  suctrALT3  37321  unisnALT  37323  elunif  37337  fnchoice  37350  mapsnd  37476  icccncfext  37765  stoweidlem27  37887  stoweidlem35  37896  stoweidlem46  37907  stoweidlem52  37913  issal  38175  intsaluni  38188  salgencntex  38202  sge0f1o  38224  funressnfv  38629  fnbrafvb  38656  afvco2  38678  ndmaovg  38686  aovmpt4g  38703  nnsum4primeseven  38895  nnsum4primesevenALTV  38896  fundmge2nop  39026  fzoopth  39063  incistruhgr  39171  upgr1eopALT  39205  uhgrvtxedgiedgb  39227  upgredg2vtx  39231  usgr2edg  39291  usgredg4  39294  usgredg2vtxeuALT  39299  uspgredg2vlem  39300  uspgredg2v  39301  ushgredgedga  39306  usgredgaleordALT  39311  nbgr1vtx  39426  nbusgredgeu0  39442  nbusgrf1o0  39443  nbusgrf1o  39445  nb3grprlem1  39454  nb3grprlem2  39455  uvtxa01vtx0  39469  nbupgruvtxres  39480  cplgr1v  39497  vtxdushgrfvedglem  39542  uhgrvd0nedgb  39545  vtxduhgr0nedg  39546  uspgrloopvd2  39557  1wlk1walk  39648  usgpredgv  39764  usgvincvad  39769  usgvincvadALT  39772  usgvad2edg  39776  usg2edgneu  39777  usgedgvadf1lem1  39778  usgedgvadf1lem2  39779  usgedgvadf1ALTlem1  39781  usgedgvadf1ALTlem2  39782  usgedgleord  39784  usgedgleordALT  39785  issubmgm  39842  c0snmgmhm  39967  c0snmhm  39968  rngccatidALTV  40044  ringccatidALTV  40107  ldepspr  40319
  Copyright terms: Public domain W3C validator