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

Theorem eleq2 2901
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 2898 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893
This theorem is referenced by:  eleq12  2902  eleq2i  2904  nelneq2  2938  dvelimdc  3005  nelne1OLD  3114  raleqf  3398  rexeqf  3399  reueq1f  3400  rmoeq1f  3401  reueq1  3408  rmoeq1  3409  raleleq  3428  rabeqf  3482  rabeqi  3483  rabeq  3484  clel3g  3653  clel4  3655  sbcbi2OLD  3831  sbcel2gv  3840  csbeq2  3887  difeq2  4092  uneq1  4131  ineq1OLD  4181  unineq  4253  nel02  4297  n0i  4298  sbnfc2  4387  disjel  4404  elif  4507  exsnrex  4612  elinsn  4640  sneqrg  4764  preq1b  4771  preq12b  4775  elpreqprb  4792  elunii  4837  elinti  4878  intss1  4884  intmin  4889  intab  4899  iineq2  4931  dfiin2g  4949  breq  5060  zfrepclf  5190  zfauscl  5197  sseliALT  5205  inuni  5238  sels  5325  elALT  5326  rext  5332  intid  5342  elopg  5350  opth1  5359  opthwiener  5396  xpeq1  5563  xpeq2  5570  0nelelxp  5584  opthprc  5610  ordtri1  6218  ordtri3  6221  nsuceq0  6265  suctr  6268  ordnbtwn  6275  funopg  6383  dffv2  6750  fveqdmss  6839  dffo4  6862  funopdmsn  6905  fnsnb  6921  elunirn  7001  f1oiso  7093  canth  7100  eusvobj2  7138  mpoeq123  7215  ndmovg  7320  uniuni  7472  iunpw  7481  oneqmin  7508  onuninsuci  7543  nlimsucg  7545  limomss  7573  nnlim  7581  peano5  7593  unielxp  7718  cnvf1o  7797  smoel  7988  smo11  7992  tz7.44-2  8034  oawordeulem  8170  oaordex  8174  omordi  8182  oneo  8197  oeordi  8203  oeoa  8213  oeoe  8215  nnmordi  8247  nnaordex  8254  omabs  8264  nnneo  8268  omsmolem  8270  elqsn0  8356  qsel  8366  mapsnd  8439  undifixp  8487  boxriin  8493  boxcutc  8494  fineqvlem  8721  fineqv  8722  pssnn  8725  fissuni  8818  dffi2  8876  inficl  8878  dffi3  8884  wofib  8998  zfregcl  9047  en3lplem1  9064  en3lp  9066  suc11reg  9071  inf0  9073  inf3lem2  9081  inf3lem3  9082  infeq5i  9088  axinf2  9092  dfom3  9099  elom3  9100  cantnfle  9123  oemapvali  9136  cantnflem1  9141  tc2  9173  r1sdom  9192  rankwflemb  9211  rankval3b  9244  rankunb  9268  rankuni2b  9271  cardlim  9390  cardprclem  9397  infxpenlem  9428  alephnbtwn  9486  alephordi  9489  cardaleph  9504  alephfp  9523  alephval3  9525  dfac3  9536  dfac5lem2  9539  dfac5lem4  9541  dfac2b  9545  kmlem2  9566  coflim  9672  cfsmolem  9681  fin23lem30  9753  isf34lem4  9788  axdc2lem  9859  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  zorn2lem7  9913  axdclem  9930  brdom7disj  9942  brdom6disj  9943  axpowndlem3  10010  winainflem  10104  iswun  10115  eltskg  10161  inar1  10186  elgrug  10203  inaprc  10247  eltskm  10254  addnidpi  10312  indpi  10318  nqereu  10340  elnp  10398  elnpi  10399  genpnnp  10416  ltaddpr  10445  dfnn2  11640  dfnn3  11641  dfuzi  12062  uz11  12256  elfzonlteqm1  13103  om2uzlti  13308  axdc4uz  13342  hashrabsn1  13725  hashbclem  13800  hashf1lem2  13804  hash2prb  13820  hash2prd  13823  wrdsymb0  13891  lsw0  13907  swrdwrdsymb  14014  rtrclreclem3  14409  prodeq1f  15252  rpnnen2lem1  15557  rpnnen2lem2  15558  lcmfval  15955  lcmf0val  15956  ismre  16851  isacs  16912  initoid  17255  termoid  17256  initoeu2lem1  17264  clatl  17716  mreclatBAD  17787  issubm  17958  dfgrp2e  18069  isnsg  18247  cycsubg  18291  resghm  18314  ghmeql  18321  gsmsymgreq  18491  f1otrspeq  18506  pmtrval  18510  pmtrdifellem4  18538  pmtrprfval  18546  gsumzsplit  18978  pgpfac1lem1  19127  pgpfac1lem5  19132  pgpfac1  19133  ablsimpnosubgd  19157  issubrg  19466  lmodfopnelem2  19602  islss  19637  lspsneq0  19715  lmhmeql  19758  lspdisjb  19829  lidl1el  19921  lidldvgen  19958  0ring01eq  19974  mplcoe1  20176  mplcoe5  20179  selvfval  20260  islindf4  20912  m1detdiag  21136  mdetunilem9  21159  maducoeval2  21179  madugsum  21182  chpmat1dlem  21373  istopg  21433  toprntopon  21463  fiinbas  21490  topbas  21510  ppttop  21545  pptbas  21546  epttop  21547  elcls  21611  clsndisj  21613  iscldtop  21633  neiptopnei  21670  restbas  21696  restntr  21720  pnfnei  21758  mnfnei  21759  cnpimaex  21794  lmcvg  21800  iscnp4  21801  cncnpi  21816  cnconst2  21821  cnprest  21827  cnprest2  21828  cnpdis  21831  lmss  21836  lmff  21839  cnt0  21884  ist1-3  21887  cnhaus  21892  isreg2  21915  dishaus  21920  ordthauslem  21921  cmpsublem  21937  cmpsub  21938  cmpcld  21940  hauscmplem  21944  unconn  21967  conncompid  21969  conncompss  21971  1stcfb  21983  1stcrest  21991  2ndcctbss  21993  2ndcomap  21996  dis2ndc  21998  1stcelcls  21999  llyeq  22008  nllyeq  22009  restnlly  22020  islly2  22022  lly1stc  22034  dislly  22035  hauspwdom  22039  finlocfin  22058  unisngl  22065  dissnlocfin  22067  locfindis  22068  comppfsc  22070  llycmpkgen2  22088  txbas  22105  eltx  22106  ptpjopn  22150  ptclsg  22153  txcnp  22158  ptcnplem  22159  ptcnp  22160  txlly  22174  pthaus  22176  txtube  22178  txhaus  22185  txlm  22186  tx1stc  22188  txkgen  22190  xkohaus  22191  xkopt  22193  xkococnlem  22197  tgqtop  22250  kqfvima  22268  kqt0lem  22274  isr0  22275  regr1lem  22277  kqreglem1  22279  kqreglem2  22280  reghmph  22331  fbssfi  22375  isfil  22385  filuni  22423  isufil  22441  isufil2  22446  fixufil  22460  uffixfr  22461  uffixsn  22463  rnelfm  22491  flimopn  22513  flimrest  22521  flimcls  22523  txflf  22544  fclsopni  22553  fclsrest  22562  fclscf  22563  fcfnei  22573  alexsublem  22582  alexsubALTlem3  22587  alexsubALT  22589  tmdgsum2  22634  symgtgp  22639  subgntr  22644  opnsubg  22645  ghmcnp  22652  tgpt0  22656  qustgpopn  22657  tsmsi  22671  tsmssubm  22680  tsmssplit  22689  isust  22741  ustn0  22758  blssps  22963  blss  22964  blssexps  22965  blssex  22966  neibl  23040  blcld  23044  metss  23047  methaus  23059  met1stc  23060  met2ndci  23061  metrest  23063  prdsxmslem2  23068  metcnp3  23079  dscopn  23112  idnghm  23281  qdensere  23307  tgioo  23333  tgqioo  23337  zdis  23353  xrge0tsms  23371  cnheibor  23488  lmmbr  23790  bcthlem4  23859  ovolicc2lem5  24051  dyadmbllem  24129  i1fd  24211  itg11  24221  itg2gt0  24290  itgeq1f  24301  bddmulibl  24368  ellimc2  24404  limcnlp  24405  ellimc3  24406  limcflf  24408  limciun  24421  lhop1lem  24539  ig1pdvds  24699  plycpn  24807  aannenlem2  24847  efopn  25168  xrlimcnp  25474  wilthlem2  25574  wilthlem3  25575  tghilberti1  26351  colline  26363  lmif  26499  islmib  26501  incistruhgr  26792  upgr1eopALT  26830  uhgrvtxedgiedgb  26849  upgredg2vtx  26854  edglnl  26856  numedglnl  26857  uhgr2edg  26918  umgrvad2edg  26923  usgredg4  26927  usgredg2vtxeuALT  26932  uspgredg2vlem  26933  ushgredgedg  26939  nbgr1vtx  27068  nbusgredgeu0  27078  nbusgrf1o0  27079  nb3grprlem1  27090  nb3grprlem2  27091  uvtx01vtx  27107  nbupgruvtxres  27117  cplgr1vlem  27139  cplgr1v  27140  vtxd0nedgb  27198  vtxduhgr0nedg  27202  1loopgrvd2  27213  1egrvtxdg0  27221  uspgrloopvtxel  27226  vtxdginducedm1lem4  27252  wlk1walk  27348  wlkp1lem1  27383  pthdivtx  27438  0enwwlksnge1  27570  umgrwwlks2on  27664  rusgr0edg  27680  eleclclwwlkn  27783  upgr4cycl4dv4e  27892  1conngr  27901  vdn0conngrumgrv2  27903  eupth2eucrct  27924  eupth2lem1  27925  frgrncvvdeqlem7  28012  frgrncvvdeqlem9  28014  frgrwopregasn  28023  frgrwopregbsn  28024  l2p  28184  lpni  28185  issh  28913  pjoc1  29139  h1dn0  29257  spansneleqi  29274  nonbooli  29356  pjch  29399  pjnel  29431  cdjreui  30137  rexunirn  30184  rabsnel  30191  nelun  30202  opabdm  30291  opabrn  30292  fpwrelmapffslem  30395  fpwrelmap  30396  fz1nntr  30454  xrge0tsmsd  30620  isprmidl  30875  reff  31003  tpr2rico  31055  lmxrge0  31095  indval  31172  issiga  31271  isrnsiga  31272  isldsys  31315  isros  31327  issros  31334  ddeval1  31393  ddeval0  31394  ismbfm  31410  isanmbfm  31414  dya2icoseg  31435  dya2iocnrect  31439  ballotlem7  31693  bnj216  31902  bnj563  31914  bnj956  31948  bnj545  32067  bnj548  32069  bnj570  32077  bnj900  32101  bnj929  32108  bnj964  32115  bnj983  32123  bnj1001  32130  bnj1145  32163  bnj1398  32204  bnj1498  32231  erdszelem1  32336  kur14lem9  32359  cnllysconn  32390  cvmsss2  32419  cvmcov2  32420  cvmsiota  32422  cvmopnlem  32423  cvmliftlem15  32443  satfv1  32508  satfdmlem  32513  mclsssvlem  32707  mclsind  32715  untelirr  32832  untsucf  32834  elintfv  32905  dfon2lem4  32929  dfon2lem7  32932  dfon2lem9  32934  soseq  32994  nodenselem8  33093  noetalem3  33117  nocvxminlem  33145  dfiota3  33282  funpartlem  33301  funpartfun  33302  linethru  33512  hilbert1.1  33513  rankelg  33527  elhf2  33534  neibastop2lem  33606  bj-rabeqd  34136  bj-zfauscl  34141  bj-cleq  34172  bj-snsetex  34173  bj-nuliota  34245  mptsnunlem  34502  isbasisrelowllem1  34519  isbasisrelowllem2  34520  relowlssretop  34527  relowlpssretop  34528  exrecfnlem  34543  finxpeq1  34550  finxpreclem5  34559  finxpreclem6  34560  nlpineqsn  34572  fvineqsneu  34575  fvineqsneq  34576  pibt2  34581  unccur  34757  fin2so  34761  matunitlindflem1  34770  ptrecube  34774  poimirlem9  34783  poimirlem30  34804  poimir  34807  heicant  34809  mblfinlem1  34811  ftc1anc  34857  ftc2nc  34858  cover2  34872  isbnd2  34944  prdstotbnd  34955  heibor1lem  34970  grpokerinj  35054  rngoueqz  35101  isidl  35175  1idl  35187  0rngo  35188  ispridl  35195  smprngopr  35213  isfldidl  35229  isdmn3  35235  mpobi123f  35323  iineq12f  35325  mptbi12f  35327  eqvrelqsel  35733  n0eldmqseq  35766  dmqseqim2  35773  lsateln0  36013  ispsubsp  36763  linepsubN  36770  elpcliN  36911  dvh3dim3N  38467  dochsnnz  38468  mapdindp3  38740  prjspval  39133  elmzpcl  39203  diophren  39290  dford3lem2  39504  ttac  39513  pw2f1ocnv  39514  wepwsolem  39522  kelac1  39543  intabssd  39765  elmapintrab  39816  eliunov2  39904  gneispaceel2  40374  mnuop23d  40482  mnuunid  40493  mnurndlem1  40497  expgrowthi  40545  dvconstbi  40546  tratrb  40750  suctrALT2VD  41050  suctrALT2  41051  en3lplem1VD  41057  en3lpVD  41059  tratrbVD  41075  suctrALTcf  41136  suctrALTcfVD  41137  suctrALT3  41138  unisnALT  41140  restuni3  41265  supminfxr  41620  xlimxrre  41992  xlimmnfvlem1  41993  xlimpnfvlem1  41997  icccncfext  42050  stoweidlem27  42193  stoweidlem35  42201  stoweidlem46  42212  stoweidlem52  42218  ioorrnopnlem  42470  ioorrnopnxrlem  42472  issal  42480  intsaluni  42493  salgencntex  42507  sge0f1o  42545  smfresal  42944  funressnfv  43159  fnbrafvb  43234  afvco2  43256  ndmaovg  43264  aovmpt4g  43281  fafv2elrnb  43315  fzoopth  43408  sprsymrelf1lem  43500  paireqne  43520  fpprbasnn  43741  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  issubmgm  43903  c0snmgmhm  44083  c0snmhm  44084  rngccatidALTV  44158  ringccatidALTV  44221  ldepspr  44426
  Copyright terms: Public domain W3C validator