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

Theorem eleq2 2839
Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Assertion
Ref Expression
eleq2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem eleq2
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21eleq2d 2836 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767
This theorem is referenced by:  eleq12  2840  eleq2i  2842  nelneq2  2875  dvelimdc  2935  nelne1  3039  raleqf  3283  rexeqf  3284  reueq1f  3285  rmoeq1f  3286  raleleq  3305  rabeqf  3340  clel3g  3491  clel4  3493  sbcbi2  3636  sbcel2gv  3647  csbeq2  3686  difeq2  3873  uneq1  3911  ineq1  3958  unineq  4026  n0i  4068  sbnfc2  4151  disjel  4167  elif  4267  exsnrex  4359  elinsn  4382  sneqrg  4503  preq1b  4509  preq12b  4513  prel12OLD  4514  elpreqprb  4534  elunii  4579  elinti  4620  intss1  4626  intmin  4631  intab  4641  iineq2  4672  dfiin2g  4687  breq  4788  zfrepclf  4911  zfauscl  4917  sseliALT  4925  inuni  4957  elALT  5038  rext  5044  intid  5054  elopg  5062  opth1  5071  opthwiener  5107  xpeq1  5263  xpeq2  5269  0nelelxp  5285  opthprc  5307  ordtri1  5899  ordtri3  5902  ordtri3OLD  5903  nsuceq0  5948  suctr  5951  suctrOLD  5952  ordnbtwn  5959  ordnbtwnOLD  5960  funopg  6065  dffv2  6413  fveqdmss  6497  dffo4  6518  funopdmsn  6558  fnsnb  6576  elunirn  6652  f1oiso  6744  canth  6751  eusvobj2  6786  mpt2eq123  6861  ndmovg  6964  snnexOLD  7114  uniuni  7118  iunpw  7125  oneqmin  7152  onuninsuci  7187  nlimsucg  7189  limomss  7217  nnlim  7225  peano5  7236  unielxp  7353  cnvf1o  7427  smoel  7610  smo11  7614  tz7.44-2  7656  oawordeulem  7788  oaordex  7792  omordi  7800  oneo  7815  oeordi  7821  oeoa  7831  oeoe  7833  nnmordi  7865  nnaordex  7872  omabs  7881  nnneo  7885  omsmolem  7887  elqsn0  7968  qsel  7978  mapsnd  8051  undifixp  8098  boxriin  8104  boxcutc  8105  fineqvlem  8330  fineqv  8331  pssnn  8334  fissuni  8427  dffi2  8485  inficl  8487  dffi3  8493  wofib  8606  zfregcl  8655  en3lplem1  8671  en3lp  8673  suc11reg  8680  inf0  8682  inf3lem2  8690  inf3lem3  8691  infeq5i  8697  axinf2  8701  dfom3  8708  elom3  8709  cantnfle  8732  oemapvali  8745  cantnflem1  8750  tc2  8782  r1sdom  8801  rankwflemb  8820  rankval3b  8853  rankunb  8877  rankuni2b  8880  cardlim  8998  cardprclem  9005  infxpenlem  9036  alephnbtwn  9094  alephordi  9097  cardaleph  9112  alephfp  9131  alephval3  9133  dfac3  9144  dfac5lem2  9147  dfac5lem4  9149  dfac2b  9153  dfac2OLD  9155  kmlem2  9175  coflim  9285  cfsmolem  9294  fin23lem30  9366  isf34lem4  9401  axdc2lem  9472  axdc3lem2  9475  axdc3lem4  9477  axdc4lem  9479  zorn2lem7  9526  axdclem  9543  brdom7disj  9555  brdom6disj  9556  axpowndlem3  9623  winainflem  9717  iswun  9728  eltskg  9774  inar1  9799  elgrug  9816  inaprc  9860  eltskm  9867  addnidpi  9925  indpi  9931  nqereu  9953  elnp  10011  elnpi  10012  genpnnp  10029  ltaddpr  10058  dfnn2  11235  dfnn3  11236  dfuzi  11670  uz11  11911  elfzonlteqm1  12752  om2uzlti  12957  axdc4uz  12991  hashrabsn1  13365  hashbclem  13438  hashf1lem2  13442  hash2prb  13456  hash2prd  13459  wrdsymb0  13535  lsw0  13549  rtrclreclem3  14008  prodeq1f  14845  rpnnen2lem1  15149  rpnnen2lem2  15150  lcmfval  15542  lcmf0val  15543  ismre  16458  isacs  16519  initoid  16862  termoid  16863  initoeu2lem1  16871  clatl  17324  mreclatBAD  17395  issubm  17555  dfgrp2e  17656  cycsubg  17830  isnsg  17831  resghm  17884  ghmeql  17891  gsmsymgreq  18059  f1otrspeq  18074  pmtrval  18078  pmtrdifellem4  18106  pmtrprfval  18114  gsumzsplit  18534  pgpfac1lem1  18681  pgpfac1lem5  18686  pgpfac1  18687  issubrg  18990  lmodfopnelem2  19110  islss  19145  lspsneq0  19225  lmhmeql  19268  lspdisjb  19339  lidl1el  19433  lidldvgen  19470  0ring01eq  19486  mplcoe1  19680  mplcoe5  19683  islindf4  20394  m1detdiag  20621  mdetunilem9  20644  maducoeval2  20664  madugsum  20667  chpmat1dlem  20860  istopg  20920  toprntopon  20950  fiinbas  20977  topbas  20997  ppttop  21032  pptbas  21033  epttop  21034  elcls  21098  clsndisj  21100  iscldtop  21120  neiptopnei  21157  restbas  21183  restntr  21207  pnfnei  21245  mnfnei  21246  cnpimaex  21281  lmcvg  21287  iscnp4  21288  cncnpi  21303  cnconst2  21308  cnprest  21314  cnprest2  21315  cnpdis  21318  lmss  21323  lmff  21326  cnt0  21371  ist1-3  21374  cnhaus  21379  isreg2  21402  dishaus  21407  ordthauslem  21408  cmpsublem  21423  cmpsub  21424  cmpcld  21426  hauscmplem  21430  unconn  21453  conncompid  21455  conncompss  21457  1stcfb  21469  1stcrest  21477  2ndcctbss  21479  2ndcomap  21482  dis2ndc  21484  1stcelcls  21485  llyeq  21494  nllyeq  21495  restnlly  21506  islly2  21508  lly1stc  21520  dislly  21521  hauspwdom  21525  finlocfin  21544  unisngl  21551  dissnlocfin  21553  locfindis  21554  comppfsc  21556  llycmpkgen2  21574  txbas  21591  eltx  21592  ptpjopn  21636  ptclsg  21639  txcnp  21644  ptcnplem  21645  ptcnp  21646  txlly  21660  pthaus  21662  txtube  21664  txhaus  21671  txlm  21672  tx1stc  21674  txkgen  21676  xkohaus  21677  xkopt  21679  xkococnlem  21683  tgqtop  21736  kqfvima  21754  kqt0lem  21760  isr0  21761  regr1lem  21763  kqreglem1  21765  kqreglem2  21766  reghmph  21817  fbssfi  21861  isfil  21871  filuni  21909  isufil  21927  isufil2  21932  fixufil  21946  uffixfr  21947  uffixsn  21949  rnelfm  21977  flimopn  21999  flimrest  22007  flimcls  22009  txflf  22030  fclsopni  22039  fclsrest  22048  fclscf  22049  fcfnei  22059  alexsublem  22068  alexsubALTlem3  22073  alexsubALT  22075  tmdgsum2  22120  symgtgp  22125  subgntr  22130  opnsubg  22131  ghmcnp  22138  tgpt0  22142  qustgpopn  22143  tsmsi  22157  tsmssubm  22166  tsmssplit  22175  isust  22227  ustn0  22244  blssps  22449  blss  22450  blssexps  22451  blssex  22452  neibl  22526  blcld  22530  metss  22533  methaus  22545  met1stc  22546  met2ndci  22547  metrest  22549  prdsxmslem2  22554  metcnp3  22565  dscopn  22598  idnghm  22767  qdensere  22793  tgioo  22819  tgqioo  22823  zdis  22839  xrge0tsms  22857  cnheibor  22974  lmmbr  23275  bcthlem4  23343  ovolicc2lem5  23509  dyadmbllem  23587  i1fd  23668  itg11  23678  itg2gt0  23747  itgeq1f  23758  bddmulibl  23825  ellimc2  23861  limcnlp  23862  ellimc3  23863  limcflf  23865  limciun  23878  lhop1lem  23996  ig1pdvds  24156  plycpn  24264  aannenlem2  24304  efopn  24625  xrlimcnp  24916  wilthlem2  25016  wilthlem3  25017  tghilberti1  25753  colline  25765  lmif  25898  islmib  25900  incistruhgr  26195  upgr1eopALT  26233  uhgrvtxedgiedgb  26252  uhgrvtxedgiedgbOLD  26253  upgredg2vtx  26258  edglnl  26260  numedglnl  26261  uhgr2edg  26322  umgrvad2edg  26327  usgredg4  26331  usgredg2vtxeuALT  26336  uspgredg2vlem  26337  ushgredgedg  26343  nbgr1vtx  26477  nbusgredgeu0  26493  nbusgrf1o0  26494  nb3grprlem1  26505  nb3grprlem2  26506  uvtx01vtx  26525  uvtxa01vtx0OLD  26527  nbupgruvtxres  26537  cplgr1vlem  26560  cplgr1v  26561  vtxd0nedgb  26619  vtxduhgr0nedg  26623  1loopgrvd2  26634  1egrvtxdg0  26642  uspgrloopvtxel  26647  vtxdginducedm1lem4  26673  wlk1walk  26770  wlkp1lem1  26805  pthdivtx  26860  0enwwlksnge1  26998  umgrwwlks2on  27105  rusgr0edg  27122  eleclclwwlkn  27234  upgr4cycl4dv4e  27365  1conngr  27374  vdn0conngrumgrv2  27376  eupth2eucrct  27397  eupth2lem1  27398  frgrncvvdeqlem7  27487  frgrncvvdeqlem9  27489  frgrwopregasn  27498  frgrwopregbsn  27499  l2p  27673  lpni  27674  issh  28405  pjoc1  28633  h1dn0  28751  spansneleqi  28768  nonbooli  28850  pjch  28893  pjnel  28925  cdjreui  29631  rexunirn  29670  rabsnel  29679  opabdm  29761  opabrn  29762  fpwrelmapffslem  29847  fpwrelmap  29848  fz1nntr  29901  xrge0tsmsd  30125  reff  30246  tpr2rico  30298  lmxrge0  30338  indval  30415  issiga  30514  isrnsigaOLD  30515  isrnsiga  30516  isldsys  30559  isros  30571  issros  30578  ddeval1  30637  ddeval0  30638  ismbfm  30654  isanmbfm  30658  dya2icoseg  30679  dya2iocnrect  30683  ballotlem7  30937  bnj216  31138  bnj563  31151  bnj956  31185  bnj545  31303  bnj548  31305  bnj570  31313  bnj900  31337  bnj929  31344  bnj964  31351  bnj983  31359  bnj1001  31366  bnj1145  31399  bnj1398  31440  bnj1498  31467  erdszelem1  31511  kur14lem9  31534  cnllysconn  31565  cvmsss2  31594  cvmcov2  31595  cvmsiota  31597  cvmopnlem  31598  cvmliftlem15  31618  mclsssvlem  31797  mclsind  31805  untelirr  31923  untsucf  31925  elintfv  32000  dfon2lem4  32027  dfon2lem7  32030  dfon2lem9  32032  soseq  32091  nodenselem8  32178  noetalem3  32202  nocvxminlem  32230  dfiota3  32367  funpartlem  32386  funpartfun  32387  linethru  32597  hilbert1.1  32598  rankelg  32612  elhf2  32619  neibastop2lem  32692  bj-rabeqd  33247  bj-zfauscl  33253  bj-cleq  33280  bj-snsetex  33282  bj-nuliota  33350  mptsnunlem  33522  isbasisrelowllem1  33540  isbasisrelowllem2  33541  relowlssretop  33548  relowlpssretop  33549  finxpeq1  33560  finxpreclem5  33569  finxpreclem6  33570  unccur  33725  fin2so  33729  matunitlindflem1  33738  ptrecube  33742  poimirlem9  33751  poimirlem30  33772  poimir  33775  heicant  33777  mblfinlem1  33779  ftc1anc  33825  ftc2nc  33826  cover2  33840  isbnd2  33914  prdstotbnd  33925  heibor1lem  33940  grpokerinj  34024  rngoueqz  34071  isidl  34145  1idl  34157  0rngo  34158  ispridl  34165  smprngopr  34183  isfldidl  34199  isdmn3  34205  mpt2bi123f  34303  iineq12f  34305  mptbi12f  34307  nel02  34440  lsateln0  34804  ispsubsp  35553  linepsubN  35560  elpcliN  35701  dvh3dim3N  37259  dochsnnz  37260  mapdindp3  37532  elmzpcl  37815  diophren  37903  dford3lem2  38120  ttac  38129  pw2f1ocnv  38130  wepwsolem  38138  kelac1  38159  elmapintrab  38408  intabssd  38442  eliunov2  38497  gneispaceel2  38968  expgrowthi  39058  dvconstbi  39059  tratrb  39271  suctrALT2VD  39593  suctrALT2  39594  en3lplem1VD  39600  en3lpVD  39602  tratrbVD  39619  suctrALTcf  39680  suctrALTcfVD  39681  suctrALT3  39682  unisnALT  39684  restuni3  39822  supminfxr  40210  xlimxrre  40575  xlimmnfvlem1  40576  xlimpnfvlem1  40580  icccncfext  40618  stoweidlem27  40761  stoweidlem35  40769  stoweidlem46  40780  stoweidlem52  40786  ioorrnopnlem  41041  ioorrnopnxrlem  41043  issal  41051  intsaluni  41064  salgencntex  41078  sge0f1o  41116  smfresal  41515  funressnfv  41728  fnbrafvb  41754  afvco2  41776  ndmaovg  41784  aovmpt4g  41801  fzoopth  41865  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  sprsymrelf1lem  42269  issubmgm  42317  c0snmgmhm  42442  c0snmhm  42443  rngccatidALTV  42517  ringccatidALTV  42580  ldepspr  42790
  Copyright terms: Public domain W3C validator