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

Theorem eleq2 2874
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 2871 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802
This theorem is referenced by:  eleq12  2875  eleq2i  2877  nelneq2  2910  dvelimdc  2970  nelne1  3074  raleqf  3323  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  raleleq  3345  rabeqf  3380  clel3g  3535  clel4  3537  sbcbi2  3682  sbcel2gv  3693  csbeq2  3732  difeq2  3921  uneq1  3959  ineq1  4006  unineq  4079  n0i  4121  sbnfc2  4205  disjel  4221  elif  4321  exsnrex  4414  elinsn  4437  sneqrg  4558  preq1b  4565  preq12b  4569  prel12OLD  4570  elpreqprb  4590  elunii  4635  elinti  4678  intss1  4684  intmin  4689  intab  4699  iineq2  4730  dfiin2g  4745  breq  4846  zfrepclf  4971  zfauscl  4977  sseliALT  4986  inuni  5018  elALT  5100  rext  5106  intid  5116  elopg  5124  opth1  5133  opthwiener  5169  xpeq1  5325  xpeq2  5331  0nelelxp  5345  opthprc  5367  ordtri1  5969  ordtri3  5972  ordtri3OLD  5973  nsuceq0  6018  suctr  6021  suctrOLD  6022  ordnbtwn  6029  ordnbtwnOLD  6030  funopg  6135  dffv2  6492  fveqdmss  6576  dffo4  6597  funopdmsn  6639  fnsnb  6657  elunirn  6733  f1oiso  6825  canth  6832  eusvobj2  6867  mpt2eq123  6944  ndmovg  7047  snnexOLD  7197  uniuni  7201  iunpw  7208  oneqmin  7235  onuninsuci  7270  nlimsucg  7272  limomss  7300  nnlim  7308  peano5  7319  unielxp  7436  cnvf1o  7510  smoel  7693  smo11  7697  tz7.44-2  7739  oawordeulem  7871  oaordex  7875  omordi  7883  oneo  7898  oeordi  7904  oeoa  7914  oeoe  7916  nnmordi  7948  nnaordex  7955  omabs  7964  nnneo  7968  omsmolem  7970  elqsn0  8051  qsel  8061  mapsnd  8134  undifixp  8181  boxriin  8187  boxcutc  8188  fineqvlem  8413  fineqv  8414  pssnn  8417  fissuni  8510  dffi2  8568  inficl  8570  dffi3  8576  wofib  8689  zfregcl  8738  en3lplem1  8754  en3lp  8756  suc11reg  8763  inf0  8765  inf3lem2  8773  inf3lem3  8774  infeq5i  8780  axinf2  8784  dfom3  8791  elom3  8792  cantnfle  8815  oemapvali  8828  cantnflem1  8833  tc2  8865  r1sdom  8884  rankwflemb  8903  rankval3b  8936  rankunb  8960  rankuni2b  8963  cardlim  9081  cardprclem  9088  infxpenlem  9119  alephnbtwn  9177  alephordi  9180  cardaleph  9195  alephfp  9214  alephval3  9216  dfac3  9227  dfac5lem2  9230  dfac5lem4  9232  dfac2b  9236  dfac2OLD  9238  kmlem2  9258  coflim  9368  cfsmolem  9377  fin23lem30  9449  isf34lem4  9484  axdc2lem  9555  axdc3lem2  9558  axdc3lem4  9560  axdc4lem  9562  zorn2lem7  9609  axdclem  9626  brdom7disj  9638  brdom6disj  9639  axpowndlem3  9706  winainflem  9800  iswun  9811  eltskg  9857  inar1  9882  elgrug  9899  inaprc  9943  eltskm  9950  addnidpi  10008  indpi  10014  nqereu  10036  elnp  10094  elnpi  10095  genpnnp  10112  ltaddpr  10141  dfnn2  11318  dfnn3  11319  dfuzi  11734  uz11  11927  elfzonlteqm1  12768  om2uzlti  12973  axdc4uz  13007  hashrabsn1  13381  hashbclem  13453  hashf1lem2  13457  hash2prb  13471  hash2prd  13474  wrdsymb0  13550  lsw0  13564  rtrclreclem3  14023  prodeq1f  14859  rpnnen2lem1  15163  rpnnen2lem2  15164  lcmfval  15553  lcmf0val  15554  ismre  16455  isacs  16516  initoid  16859  termoid  16860  initoeu2lem1  16868  clatl  17321  mreclatBAD  17392  issubm  17552  dfgrp2e  17653  cycsubg  17824  isnsg  17825  resghm  17878  ghmeql  17885  gsmsymgreq  18053  f1otrspeq  18068  pmtrval  18072  pmtrdifellem4  18100  pmtrprfval  18108  gsumzsplit  18528  pgpfac1lem1  18675  pgpfac1lem5  18680  pgpfac1  18681  issubrg  18984  lmodfopnelem2  19104  islss  19139  lspsneq0  19219  lmhmeql  19262  lspdisjb  19333  lidl1el  19427  lidldvgen  19464  0ring01eq  19480  mplcoe1  19674  mplcoe5  19677  islindf4  20387  m1detdiag  20614  mdetunilem9  20637  maducoeval2  20657  madugsum  20660  chpmat1dlem  20853  istopg  20913  toprntopon  20943  fiinbas  20970  topbas  20990  ppttop  21025  pptbas  21026  epttop  21027  elcls  21091  clsndisj  21093  iscldtop  21113  neiptopnei  21150  restbas  21176  restntr  21200  pnfnei  21238  mnfnei  21239  cnpimaex  21274  lmcvg  21280  iscnp4  21281  cncnpi  21296  cnconst2  21301  cnprest  21307  cnprest2  21308  cnpdis  21311  lmss  21316  lmff  21319  cnt0  21364  ist1-3  21367  cnhaus  21372  isreg2  21395  dishaus  21400  ordthauslem  21401  cmpsublem  21416  cmpsub  21417  cmpcld  21419  hauscmplem  21423  unconn  21446  conncompid  21448  conncompss  21450  1stcfb  21462  1stcrest  21470  2ndcctbss  21472  2ndcomap  21475  dis2ndc  21477  1stcelcls  21478  llyeq  21487  nllyeq  21488  restnlly  21499  islly2  21501  lly1stc  21513  dislly  21514  hauspwdom  21518  finlocfin  21537  unisngl  21544  dissnlocfin  21546  locfindis  21547  comppfsc  21549  llycmpkgen2  21567  txbas  21584  eltx  21585  ptpjopn  21629  ptclsg  21632  txcnp  21637  ptcnplem  21638  ptcnp  21639  txlly  21653  pthaus  21655  txtube  21657  txhaus  21664  txlm  21665  tx1stc  21667  txkgen  21669  xkohaus  21670  xkopt  21672  xkococnlem  21676  tgqtop  21729  kqfvima  21747  kqt0lem  21753  isr0  21754  regr1lem  21756  kqreglem1  21758  kqreglem2  21759  reghmph  21810  fbssfi  21854  isfil  21864  filuni  21902  isufil  21920  isufil2  21925  fixufil  21939  uffixfr  21940  uffixsn  21942  rnelfm  21970  flimopn  21992  flimrest  22000  flimcls  22002  txflf  22023  fclsopni  22032  fclsrest  22041  fclscf  22042  fcfnei  22052  alexsublem  22061  alexsubALTlem3  22066  alexsubALT  22068  tmdgsum2  22113  symgtgp  22118  subgntr  22123  opnsubg  22124  ghmcnp  22131  tgpt0  22135  qustgpopn  22136  tsmsi  22150  tsmssubm  22159  tsmssplit  22168  isust  22220  ustn0  22237  blssps  22442  blss  22443  blssexps  22444  blssex  22445  neibl  22519  blcld  22523  metss  22526  methaus  22538  met1stc  22539  met2ndci  22540  metrest  22542  prdsxmslem2  22547  metcnp3  22558  dscopn  22591  idnghm  22760  qdensere  22786  tgioo  22812  tgqioo  22816  zdis  22832  xrge0tsms  22850  cnheibor  22967  lmmbr  23268  bcthlem4  23336  ovolicc2lem5  23502  dyadmbllem  23580  i1fd  23662  itg11  23672  itg2gt0  23741  itgeq1f  23752  bddmulibl  23819  ellimc2  23855  limcnlp  23856  ellimc3  23857  limcflf  23859  limciun  23872  lhop1lem  23990  ig1pdvds  24150  plycpn  24258  aannenlem2  24298  efopn  24618  xrlimcnp  24909  wilthlem2  25009  wilthlem3  25010  tghilberti1  25746  colline  25758  lmif  25891  islmib  25893  incistruhgr  26188  upgr1eopALT  26226  uhgrvtxedgiedgb  26245  uhgrvtxedgiedgbOLD  26246  upgredg2vtx  26251  edglnl  26253  numedglnl  26254  uhgr2edg  26315  umgrvad2edg  26320  usgredg4  26324  usgredg2vtxeuALT  26329  uspgredg2vlem  26330  ushgredgedg  26336  nbgr1vtx  26470  nbusgredgeu0  26486  nbusgrf1o0  26487  nb3grprlem1  26498  nb3grprlem2  26499  uvtx01vtx  26518  uvtxa01vtx0OLD  26520  nbupgruvtxres  26530  cplgr1vlem  26553  cplgr1v  26554  vtxd0nedgb  26612  vtxduhgr0nedg  26616  1loopgrvd2  26627  1egrvtxdg0  26635  uspgrloopvtxel  26640  vtxdginducedm1lem4  26666  wlk1walk  26763  wlkp1lem1  26798  pthdivtx  26853  0enwwlksnge1  26991  umgrwwlks2on  27098  rusgr0edg  27115  eleclclwwlkn  27227  upgr4cycl4dv4e  27358  1conngr  27367  vdn0conngrumgrv2  27369  eupth2eucrct  27390  eupth2lem1  27391  frgrncvvdeqlem7  27480  frgrncvvdeqlem9  27482  frgrwopregasn  27491  frgrwopregbsn  27492  l2p  27662  lpni  27663  issh  28393  pjoc1  28621  h1dn0  28739  spansneleqi  28756  nonbooli  28838  pjch  28881  pjnel  28913  cdjreui  29619  rexunirn  29657  rabsnel  29666  opabdm  29748  opabrn  29749  fpwrelmapffslem  29834  fpwrelmap  29835  fz1nntr  29888  xrge0tsmsd  30110  reff  30231  tpr2rico  30283  lmxrge0  30323  indval  30400  issiga  30499  isrnsigaOLD  30500  isrnsiga  30501  isldsys  30544  isros  30556  issros  30563  ddeval1  30622  ddeval0  30623  ismbfm  30639  isanmbfm  30643  dya2icoseg  30664  dya2iocnrect  30668  ballotlem7  30922  bnj216  31123  bnj563  31136  bnj956  31170  bnj545  31288  bnj548  31290  bnj570  31298  bnj900  31322  bnj929  31329  bnj964  31336  bnj983  31344  bnj1001  31351  bnj1145  31384  bnj1398  31425  bnj1498  31452  erdszelem1  31496  kur14lem9  31519  cnllysconn  31550  cvmsss2  31579  cvmcov2  31580  cvmsiota  31582  cvmopnlem  31583  cvmliftlem15  31603  mclsssvlem  31782  mclsind  31790  untelirr  31907  untsucf  31909  elintfv  31984  dfon2lem4  32011  dfon2lem7  32014  dfon2lem9  32016  soseq  32075  nodenselem8  32162  noetalem3  32186  nocvxminlem  32214  dfiota3  32351  funpartlem  32370  funpartfun  32371  linethru  32581  hilbert1.1  32582  rankelg  32596  elhf2  32603  neibastop2lem  32676  bj-rabeqd  33226  bj-zfauscl  33232  bj-cleq  33259  bj-snsetex  33261  bj-nuliota  33329  mptsnunlem  33502  isbasisrelowllem1  33519  isbasisrelowllem2  33520  relowlssretop  33527  relowlpssretop  33528  finxpeq1  33539  finxpreclem5  33548  finxpreclem6  33549  unccur  33705  fin2so  33709  matunitlindflem1  33718  ptrecube  33722  poimirlem9  33731  poimirlem30  33752  poimir  33755  heicant  33757  mblfinlem1  33759  ftc1anc  33805  ftc2nc  33806  cover2  33820  isbnd2  33893  prdstotbnd  33904  heibor1lem  33919  grpokerinj  34003  rngoueqz  34050  isidl  34124  1idl  34136  0rngo  34137  ispridl  34144  smprngopr  34162  isfldidl  34178  isdmn3  34184  mpt2bi123f  34281  iineq12f  34283  mptbi12f  34285  nel02  34412  lsateln0  34775  ispsubsp  35525  linepsubN  35532  elpcliN  35673  dvh3dim3N  37230  dochsnnz  37231  mapdindp3  37503  elmzpcl  37791  diophren  37879  dford3lem2  38095  ttac  38104  pw2f1ocnv  38105  wepwsolem  38113  kelac1  38134  elmapintrab  38382  intabssd  38416  eliunov2  38471  gneispaceel2  38942  expgrowthi  39032  dvconstbi  39033  tratrb  39244  suctrALT2VD  39565  suctrALT2  39566  en3lplem1VD  39572  en3lpVD  39574  tratrbVD  39591  suctrALTcf  39652  suctrALTcfVD  39653  suctrALT3  39654  unisnALT  39656  restuni3  39793  supminfxr  40173  xlimxrre  40537  xlimmnfvlem1  40538  xlimpnfvlem1  40542  icccncfext  40580  stoweidlem27  40723  stoweidlem35  40731  stoweidlem46  40742  stoweidlem52  40748  ioorrnopnlem  41003  ioorrnopnxrlem  41005  issal  41013  intsaluni  41026  salgencntex  41040  sge0f1o  41078  smfresal  41477  funressnfv  41662  fnbrafvb  41743  afvco2  41765  ndmaovg  41773  aovmpt4g  41790  fafv2elrnb  41824  fzoopth  41912  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  sprsymrelf1lem  42309  issubmgm  42357  c0snmgmhm  42482  c0snmhm  42483  rngccatidALTV  42557  ringccatidALTV  42620  ldepspr  42830
  Copyright terms: Public domain W3C validator