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

Theorem eleq2 2688
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 2685 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616
This theorem is referenced by:  eleq12  2689  eleq2i  2691  nelneq2  2724  dvelimdc  2783  nelne1  2887  raleqf  3129  rexeqf  3130  reueq1f  3131  rmoeq1f  3132  raleleq  3151  rabeqf  3185  clel3g  3334  clel4  3336  sbcbi2  3478  sbcel2gv  3490  csbeq2  3530  difeq2  3714  uneq1  3752  ineq1  3799  unineq  3869  n0i  3912  sbnfc2  3998  disjel  4014  elif  4119  exsnrex  4212  elinsn  4236  sneqrg  4361  preq1b  4368  preqr1OLD  4371  preq12b  4373  prel12  4374  elpreqprb  4388  elunii  4432  eluniab  4438  ssuniOLD  4451  elinti  4476  elintab  4478  intss1  4483  intmin  4488  intab  4498  iineq2  4529  dfiin2g  4544  breq  4646  zfrepclf  4768  zfauscl  4774  sseliALT  4782  inuni  4817  elALT  4901  rext  4907  intid  4917  elopg  4925  opth1  4934  opthwiener  4966  xpeq1  5118  xpeq2  5119  0nelelxp  5135  opthprc  5157  ordtri1  5744  ordtri3  5747  ordtri3OLD  5748  nsuceq0  5793  suctr  5796  suctrOLD  5797  ordnbtwn  5804  ordnbtwnOLD  5805  funopg  5910  dffv2  6258  fveqdmss  6340  dffo4  6361  funopdmsn  6400  fnsnb  6417  elunirn  6494  f1oiso  6586  canth  6593  eusvobj2  6628  mpt2eq123  6699  ndmovg  6802  snnexOLD  6952  uniuni  6956  iunpw  6963  oneqmin  6990  onuninsuci  7025  nlimsucg  7027  limomss  7055  nnlim  7063  peano5  7074  unielxp  7189  cnvf1o  7261  smoel  7442  smo11  7446  tz7.44-2  7488  oawordeulem  7619  oaordex  7623  omordi  7631  oneo  7646  oeordi  7652  oeoa  7662  oeoe  7664  nnmordi  7696  nnaordex  7703  omabs  7712  nnneo  7716  omsmolem  7718  elqsn0  7801  qsel  7811  mapsn  7884  undifixp  7929  boxriin  7935  boxcutc  7936  fineqvlem  8159  fineqv  8160  pssnn  8163  fissuni  8256  dffi2  8314  inficl  8316  dffi3  8322  wofib  8435  zfregcl  8484  zfregclOLD  8486  en3lplem1  8496  en3lp  8498  suc11reg  8501  inf0  8503  inf3lem2  8511  inf3lem3  8512  infeq5i  8518  axinf2  8522  dfom3  8529  elom3  8530  cantnfle  8553  oemapvali  8566  cantnflem1c  8569  cantnflem1  8571  tc2  8603  r1sdom  8622  rankwflemb  8641  rankval3b  8674  rankunb  8698  rankuni2b  8701  tcrank  8732  cardlim  8783  cardprclem  8790  infxpenlem  8821  alephnbtwn  8879  alephordi  8882  cardaleph  8897  alephfp  8916  alephval3  8918  dfac3  8929  dfac5lem2  8932  dfac5lem4  8934  dfac2  8938  kmlem2  8958  coflim  9068  cfsmolem  9077  fin23lem30  9149  isf32lem2  9161  isf34lem4  9184  axdc2lem  9255  axdc3lem2  9258  axdc3lem4  9260  axdc4lem  9262  zorn2lem7  9309  axdclem  9326  brdom7disj  9338  brdom6disj  9339  axpowndlem3  9406  winainflem  9500  iswun  9511  eltskg  9557  inar1  9582  elgrug  9599  inaprc  9643  eltskm  9650  addnidpi  9708  indpi  9714  nqereu  9736  elnp  9794  elnpi  9795  genpnnp  9812  ltaddpr  9841  dfnn2  11018  dfnn3  11019  dfuzi  11453  uz11  11695  elfzonlteqm1  12527  om2uzlti  12732  axdc4uz  12766  hashrabsn1  13146  hashbclem  13219  hashf1lem2  13223  hash2prb  13237  hash2prd  13240  wrdsymb0  13322  lsw0  13335  rtrclreclem3  13781  prodeq1f  14619  rpnnen2lem1  14924  rpnnen2lem2  14925  sadcp1  15158  lcmfval  15315  lcmf0val  15316  ismre  16231  isacs  16293  initoid  16636  termoid  16637  initoeu2lem1  16645  clatl  17097  mreclatBAD  17168  issubm  17328  dfgrp2e  17429  cycsubg  17603  isnsg  17604  subgacs  17610  nsgacs  17611  resghm  17657  ghmeql  17664  gsmsymgreq  17833  f1otrspeq  17848  pmtrval  17852  pmtrdifellem4  17880  pmtrprfval  17888  gsumzsplit  18308  pgpfac1lem1  18454  pgpfac1lem5  18459  pgpfac1  18460  issubrg  18761  lmodfopnelem2  18881  islss  18916  lssacs  18948  lspsneq0  18993  lmhmeql  19036  lspdisjb  19107  lidl1el  19199  lidldvgen  19236  0ring01eq  19252  mplcoe1  19446  mplcoe5  19449  islindf4  20158  m1detdiag  20384  mdetunilem9  20407  maducoeval2  20427  madugsum  20430  chpmat1dlem  20621  istopg  20681  toprntopon  20710  fiinbas  20737  topbas  20757  ppttop  20792  pptbas  20793  epttop  20794  elcls  20858  clsndisj  20860  elcls3  20868  iscldtop  20880  neiptopnei  20917  restbas  20943  restntr  20967  pnfnei  21005  mnfnei  21006  cnpimaex  21041  lmcvg  21047  iscnp4  21048  cncnpi  21063  cnconst2  21068  cnprest  21074  cnprest2  21075  cnpdis  21078  lmss  21083  lmff  21086  cnt0  21131  ist1-3  21134  cnhaus  21139  isreg2  21162  dishaus  21167  ordthauslem  21168  cmpsublem  21183  cmpsub  21184  cmpcld  21186  hauscmplem  21190  unconn  21213  conncompid  21215  conncompconn  21216  conncompss  21217  1stcfb  21229  1stcrest  21237  2ndcctbss  21239  2ndcomap  21242  dis2ndc  21244  1stcelcls  21245  llyeq  21254  nllyeq  21255  restnlly  21266  islly2  21268  lly1stc  21280  dislly  21281  hauspwdom  21285  finlocfin  21304  unisngl  21311  dissnlocfin  21313  locfindis  21314  comppfsc  21316  llycmpkgen2  21334  txbas  21351  eltx  21352  ptpjopn  21396  ptclsg  21399  dfac14lem  21401  txcnp  21404  ptcnplem  21405  ptcnp  21406  txlly  21420  pthaus  21422  txtube  21424  txhaus  21431  txlm  21432  tx1stc  21434  txkgen  21436  xkohaus  21437  xkopt  21439  xkococnlem  21443  tgqtop  21496  kqfvima  21514  kqt0lem  21520  isr0  21521  r0cld  21522  regr1lem  21523  kqreglem1  21525  kqreglem2  21526  reghmph  21577  fbssfi  21622  isfil  21632  filuni  21670  isufil  21688  isufil2  21693  uffix  21706  fixufil  21707  uffixfr  21708  uffixsn  21710  rnelfm  21738  flimopn  21760  flimrest  21768  flimcls  21770  flftg  21781  txflf  21791  fclsopni  21800  fclsrest  21809  fclscf  21810  fcfnei  21820  alexsublem  21829  alexsubALTlem3  21834  alexsubALT  21836  tmdgsum2  21881  symgtgp  21886  subgntr  21891  opnsubg  21892  tgpconncompeqg  21896  ghmcnp  21899  tgpt0  21903  qustgpopn  21904  tsmsi  21918  tsmssubm  21927  tsmssplit  21936  isust  21988  ustn0  22005  blssps  22210  blss  22211  blssexps  22212  blssex  22213  neibl  22287  blcld  22291  metss  22294  methaus  22306  met1stc  22307  met2ndci  22308  metrest  22310  prdsxmslem2  22315  metcnp3  22326  dscopn  22359  idnghm  22528  qdensere  22554  tgioo  22580  tgqioo  22584  zdis  22600  xrge0tsms  22618  cnheibor  22735  lmmbr  23037  bcthlem4  23105  ovolicc2lem5  23270  dyadmbllem  23348  i1fd  23429  itg11  23439  itg2gt0  23508  itgeq1f  23519  bddmulibl  23586  ellimc2  23622  limcnlp  23623  ellimc3  23624  limcflf  23626  limciun  23639  lhop1lem  23757  ig1pdvds  23917  plycpn  24025  aannenlem2  24065  efopn  24385  xrlimcnp  24676  wilthlem2  24776  wilthlem3  24777  wilth  24778  tghilberti1  25513  tghilberti2  25514  colline  25525  lmif  25658  islmib  25660  incistruhgr  25955  upgr1eopALT  25993  uhgrvtxedgiedgb  26012  upgredg2vtx  26017  edglnl  26019  numedglnl  26020  uhgr2edg  26081  umgrvad2edg  26086  umgr2edgneu  26087  usgredg4  26090  usgredg2vtxeuALT  26095  uspgredg2vlem  26096  uspgredg2v  26097  ushgredgedg  26102  nbgr1vtx  26235  nbusgredgeu0  26251  nbusgrf1o0  26252  nbusgrf1o  26254  nb3grprlem1  26263  nb3grprlem2  26264  uvtxa01vtx0  26278  nbupgruvtxres  26289  cplgr1vlem  26306  cplgr1v  26307  vtxd0nedgb  26365  vtxduhgr0nedg  26369  1loopgrvd2  26380  1egrvtxdg0  26388  uspgrloopvtxel  26393  vtxdginducedm1lem4  26419  wlk1walk  26516  wlkp1lem1  26551  pthdivtx  26606  0enwwlksnge1  26730  umgrwwlks2on  26831  rusgr0edg  26849  eleclclwwlksn  26933  upgr4cycl4dv4e  27025  1conngr  27034  vdn0conngrumgrv2  27036  eupth2eucrct  27057  eupth2lem1  27058  frgrncvvdeqlem7  27149  frgrncvvdeqlem9  27151  frgrwopreg1  27160  frgrwopreg2  27161  l2p  27301  lpni  27302  issh  28035  pjoc1  28263  h1dn0  28381  spansneleqi  28398  nonbooli  28480  pjch  28523  pjnel  28555  cdjreui  29261  rexunirn  29303  rabsnel  29313  opabdm  29395  opabrn  29396  fpwrelmapffslem  29481  fpwrelmap  29482  fz1nntr  29535  xrge0tsmsd  29759  reff  29880  tpr2rico  29932  lmxrge0  29972  indval  30049  issiga  30148  isrnsigaOLD  30149  isrnsiga  30150  isldsys  30193  isros  30205  issros  30212  ddeval1  30271  ddeval0  30272  ddemeas  30273  ismbfm  30288  isanmbfm  30292  dya2icoseg  30313  dya2iocnrect  30317  ballotlem7  30571  bnj145OLD  30769  bnj216  30774  bnj563  30787  bnj956  30821  bnj545  30939  bnj548  30941  bnj570  30949  bnj900  30973  bnj929  30980  bnj964  30987  bnj983  30995  bnj1001  31002  bnj1145  31035  bnj1398  31076  bnj1498  31103  erdszelem1  31147  kur14lem9  31170  cnllysconn  31201  cvmcov  31219  cvmsss2  31230  cvmcov2  31231  cvmseu  31232  cvmsiota  31233  cvmopnlem  31234  cvmliftlem15  31254  mclsssvlem  31433  mclsind  31441  untelirr  31559  untsucf  31561  elintfv  31638  dfon2lem4  31665  dfon2lem7  31668  dfon2lem9  31670  soseq  31725  frrlem4  31757  frrlem5e  31762  frrlem11  31766  nodenselem8  31815  noetalem3  31839  nocvxminlem  31867  dfiota3  32005  funpartlem  32024  funpartfun  32025  linethru  32235  hilbert1.1  32236  hilbert1.2  32237  rankelg  32250  elhf2  32257  fneint  32318  neibastop2lem  32330  bj-rabeqd  32891  bj-cleq  32924  bj-snsetex  32926  bj-nuliota  32994  mptsnunlem  33156  isbasisrelowllem1  33174  isbasisrelowllem2  33175  relowlssretop  33182  relowlpssretop  33183  finxpeq1  33194  finxpreclem5  33203  finxpreclem6  33204  unccur  33363  fin2so  33367  matunitlindflem1  33376  ptrecube  33380  poimirlem9  33389  poimirlem30  33410  poimir  33413  heicant  33415  mblfinlem1  33417  ftc1anc  33464  ftc2nc  33465  cover2  33479  isbnd2  33553  prdstotbnd  33564  heibor1lem  33579  grpokerinj  33663  rngoueqz  33710  isidl  33784  1idl  33796  0rngo  33797  ispridl  33804  smprngopr  33822  isfldidl  33838  isdmn3  33844  mpt2bi123f  33942  iineq12f  33944  mptbi12f  33946  lsateln0  34101  ispsubsp  34850  linepsubN  34857  elpcliN  34998  dvh3dim3N  36557  dochsnnz  36558  mapdindp3  36830  elmzpcl  37108  diophren  37196  dford3lem2  37413  ttac  37422  pw2f1ocnv  37423  wepwsolem  37431  kelac1  37452  sdrgacs  37590  elintabg  37699  elmapintrab  37701  intabssd  37735  eliunov2  37790  gneispaceel2  38262  expgrowthi  38352  dvconstbi  38353  tratrb  38566  suctrALT2VD  38891  suctrALT2  38892  en3lplem1VD  38898  en3lpVD  38900  tratrbVD  38917  suctrALTcf  38978  suctrALTcfVD  38979  suctrALT3  38980  unisnALT  38982  elunif  38995  fnchoice  39008  restuni3  39121  mapsnd  39204  supminfxr  39507  icccncfext  39863  stoweidlem27  40007  stoweidlem35  40015  stoweidlem46  40026  stoweidlem52  40032  ioorrnopnlem  40287  ioorrnopnxrlem  40289  issal  40297  intsaluni  40310  salgencntex  40324  sge0f1o  40362  smfresal  40758  funressnfv  40971  fnbrafvb  40997  afvco2  41019  ndmaovg  41027  aovmpt4g  41044  fzoopth  41100  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  sprsymrelf1lem  41506  issubmgm  41554  c0snmgmhm  41679  c0snmhm  41680  rngccatidALTV  41754  ringccatidALTV  41817  ldepspr  42027
  Copyright terms: Public domain W3C validator