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

Theorem eleq2 2904
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 2901 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896
This theorem is referenced by:  eleq12  2905  eleq2i  2907  nelneq2  2941  dvelimdc  3006  raleqf  3388  rexeqf  3389  reueq1f  3390  rmoeq1f  3391  reueq1  3398  rmoeq1  3399  raleleq  3410  rabeqf  3466  rabeqiOLD  3468  rabeq  3469  clel3g  3640  clel4  3642  sbcbi2  3816  sbcel2gv  3825  csbeq2  3871  difeq2  4079  uneq1  4118  ineq1OLD  4167  unineq  4239  nel02  4281  n0i  4282  sbnfc2  4371  disjel  4389  elif  4492  exsnrex  4603  elinsn  4631  sneqrg  4754  preq1b  4761  preq12b  4765  elpreqprb  4782  elunii  4829  elinti  4871  intss1  4877  intmin  4882  intab  4892  iuneqconst  4916  iineq2  4925  dfiin2g  4943  breq  5055  zfrepclf  5185  zfauscl  5192  sseliALT  5200  inuni  5233  sels  5322  elALT  5323  rext  5329  intid  5338  elopg  5346  opth1  5355  opthwiener  5392  xpeq1  5557  xpeq2  5564  0nelelxp  5578  opthprc  5604  ordtri1  6213  ordtri3  6216  nsuceq0  6260  suctr  6263  ordnbtwn  6270  funopg  6379  dffv2  6749  fveqdmss  6839  dffo4  6862  funopdmsn  6905  fnsnb  6921  elunirn  7004  f1oiso  7099  canth  7106  eusvobj2  7144  mpoeq123  7221  ndmovg  7327  uniuni  7480  iunpw  7489  oneqmin  7516  onuninsuci  7551  nlimsucg  7553  limomss  7581  nnlim  7589  peano5  7601  unielxp  7724  cnvf1o  7804  smoel  7995  smo11  7999  tz7.44-2  8041  oawordeulem  8178  oaordex  8182  omordi  8190  oneo  8205  oeordi  8211  oeoa  8221  oeoe  8223  nnmordi  8255  nnaordex  8262  omabs  8272  nnneo  8276  omsmolem  8278  elqsn0  8364  qsel  8374  mapsnd  8448  undifixp  8496  boxriin  8502  boxcutc  8503  fineqvlem  8731  fineqv  8732  pssnn  8735  fissuni  8828  dffi2  8886  inficl  8888  dffi3  8894  wofib  9008  zfregcl  9057  en3lplem1  9074  en3lp  9076  suc11reg  9081  inf0  9083  inf3lem2  9091  inf3lem3  9092  infeq5i  9098  axinf2  9102  dfom3  9109  elom3  9110  cantnfle  9133  oemapvali  9146  cantnflem1  9151  tc2  9183  r1sdom  9202  rankwflemb  9221  rankval3b  9254  rankunb  9278  rankuni2b  9281  cardlim  9400  cardprclem  9407  infxpenlem  9439  alephnbtwn  9497  alephordi  9500  cardaleph  9515  alephfp  9534  alephval3  9536  dfac3  9547  dfac5lem2  9550  dfac5lem4  9552  dfac2b  9556  kmlem2  9577  coflim  9683  cfsmolem  9692  fin23lem30  9764  isf34lem4  9799  axdc2lem  9870  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  zorn2lem7  9924  axdclem  9941  brdom7disj  9953  brdom6disj  9954  axpowndlem3  10021  winainflem  10115  iswun  10126  eltskg  10172  inar1  10197  elgrug  10214  inaprc  10258  eltskm  10265  addnidpi  10323  indpi  10329  nqereu  10351  elnp  10409  elnpi  10410  genpnnp  10427  ltaddpr  10456  dfnn2  11649  dfnn3  11650  dfuzi  12072  uz11  12266  elfzonlteqm1  13119  om2uzlti  13324  axdc4uz  13358  hashrabsn1  13742  hashbclem  13817  hashf1lem2  13821  hash2prb  13837  hash2prd  13840  wrdsymb0  13903  lsw0  13919  swrdwrdsymb  14026  rtrclreclem3  14421  prodeq1f  15264  rpnnen2lem1  15569  rpnnen2lem2  15570  lcmfval  15965  lcmf0val  15966  ismre  16863  isacs  16924  initoid  17267  termoid  17268  initoeu2lem1  17276  clatl  17728  mreclatBAD  17799  issubm  17970  dfgrp2e  18131  isnsg  18309  cycsubg  18353  resghm  18376  ghmeql  18383  gsmsymgreq  18562  f1otrspeq  18577  pmtrval  18581  pmtrdifellem4  18609  pmtrprfval  18617  gsumzsplit  19049  pgpfac1lem1  19198  pgpfac1lem5  19203  pgpfac1  19204  ablsimpnosubgd  19228  issubrg  19537  lmodfopnelem2  19673  islss  19708  lspsneq0  19786  lmhmeql  19829  lspdisjb  19900  lidl1el  19993  lidldvgen  20030  0ring01eq  20046  islindf4  20536  mplcoe1  20714  mplcoe5  20717  selvfval  20798  m1detdiag  21211  mdetunilem9  21234  maducoeval2  21254  madugsum  21257  chpmat1dlem  21449  istopg  21509  toprntopon  21539  fiinbas  21566  topbas  21586  ppttop  21621  pptbas  21622  epttop  21623  elcls  21687  clsndisj  21689  iscldtop  21709  neiptopnei  21746  restbas  21772  restntr  21796  pnfnei  21834  mnfnei  21835  cnpimaex  21870  lmcvg  21876  iscnp4  21877  cncnpi  21892  cnconst2  21897  cnprest  21903  cnprest2  21904  cnpdis  21907  lmss  21912  lmff  21915  cnt0  21960  ist1-3  21963  cnhaus  21968  isreg2  21991  dishaus  21996  ordthauslem  21997  cmpsublem  22013  cmpsub  22014  cmpcld  22016  hauscmplem  22020  unconn  22043  conncompid  22045  conncompss  22047  1stcfb  22059  1stcrest  22067  2ndcctbss  22069  2ndcomap  22072  dis2ndc  22074  1stcelcls  22075  llyeq  22084  nllyeq  22085  restnlly  22096  islly2  22098  lly1stc  22110  dislly  22111  hauspwdom  22115  finlocfin  22134  unisngl  22141  dissnlocfin  22143  locfindis  22144  comppfsc  22146  llycmpkgen2  22164  txbas  22181  eltx  22182  ptpjopn  22226  ptclsg  22229  txcnp  22234  ptcnplem  22235  ptcnp  22236  txlly  22250  pthaus  22252  txtube  22254  txhaus  22261  txlm  22262  tx1stc  22264  txkgen  22266  xkohaus  22267  xkopt  22269  xkococnlem  22273  tgqtop  22326  kqfvima  22344  kqt0lem  22350  isr0  22351  regr1lem  22353  kqreglem1  22355  kqreglem2  22356  reghmph  22407  fbssfi  22451  isfil  22461  filuni  22499  isufil  22517  isufil2  22522  fixufil  22536  uffixfr  22537  uffixsn  22539  rnelfm  22567  flimopn  22589  flimrest  22597  flimcls  22599  txflf  22620  fclsopni  22629  fclsrest  22638  fclscf  22639  fcfnei  22649  alexsublem  22658  alexsubALTlem3  22663  alexsubALT  22665  tmdgsum2  22710  symgtgp  22720  subgntr  22721  opnsubg  22722  ghmcnp  22729  tgpt0  22733  qustgpopn  22734  tsmsi  22748  tsmssubm  22757  tsmssplit  22766  isust  22818  ustn0  22835  blssps  23040  blss  23041  blssexps  23042  blssex  23043  neibl  23117  blcld  23121  metss  23124  methaus  23136  met1stc  23137  met2ndci  23138  metrest  23140  prdsxmslem2  23145  metcnp3  23156  dscopn  23189  idnghm  23358  qdensere  23384  tgioo  23410  tgqioo  23414  zdis  23430  xrge0tsms  23448  cnheibor  23569  lmmbr  23871  bcthlem4  23940  ovolicc2lem5  24134  dyadmbllem  24212  i1fd  24294  itg11  24304  itg2gt0  24373  itgeq1f  24384  bddmulibl  24451  ellimc2  24489  limcnlp  24490  ellimc3  24491  limcflf  24493  limciun  24506  lhop1lem  24625  ig1pdvds  24786  plycpn  24894  aannenlem2  24934  efopn  25258  xrlimcnp  25563  wilthlem2  25663  wilthlem3  25664  tghilberti1  26440  colline  26452  lmif  26588  islmib  26590  incistruhgr  26881  upgr1eopALT  26919  uhgrvtxedgiedgb  26938  upgredg2vtx  26943  edglnl  26945  numedglnl  26946  uhgr2edg  27007  umgrvad2edg  27012  usgredg4  27016  usgredg2vtxeuALT  27021  uspgredg2vlem  27022  ushgredgedg  27028  nbgr1vtx  27157  nbusgredgeu0  27167  nbusgrf1o0  27168  nb3grprlem1  27179  nb3grprlem2  27180  uvtx01vtx  27196  nbupgruvtxres  27206  cplgr1vlem  27228  cplgr1v  27229  vtxd0nedgb  27287  vtxduhgr0nedg  27291  1loopgrvd2  27302  1egrvtxdg0  27310  uspgrloopvtxel  27315  vtxdginducedm1lem4  27341  wlk1walk  27437  wlkp1lem1  27472  pthdivtx  27527  0enwwlksnge1  27659  umgrwwlks2on  27752  rusgr0edg  27768  eleclclwwlkn  27870  upgr4cycl4dv4e  27979  1conngr  27988  vdn0conngrumgrv2  27990  eupth2eucrct  28011  eupth2lem1  28012  frgrncvvdeqlem7  28099  frgrncvvdeqlem9  28101  frgrwopregasn  28110  frgrwopregbsn  28111  l2p  28271  lpni  28272  issh  29000  pjoc1  29226  h1dn0  29344  spansneleqi  29361  nonbooli  29443  pjch  29486  pjnel  29518  cdjreui  30224  rexunirn  30272  rabsnel  30279  nelun  30291  iinabrex  30338  opabdm  30381  opabrn  30382  fpwrelmapffslem  30489  fpwrelmap  30490  fz1nntr  30548  xrge0tsmsd  30734  isprmidl  31006  reff  31172  tpr2rico  31240  lmxrge0  31280  indval  31357  issiga  31456  isrnsiga  31457  isldsys  31500  isros  31512  issros  31519  ddeval1  31578  ddeval0  31579  ismbfm  31595  isanmbfm  31599  dya2icoseg  31620  dya2iocnrect  31624  ballotlem7  31878  bnj216  32087  bnj563  32099  bnj956  32133  bnj545  32252  bnj548  32254  bnj570  32262  bnj900  32286  bnj929  32293  bnj964  32300  bnj983  32308  bnj1001  32316  bnj1145  32350  bnj1398  32391  bnj1498  32418  erdszelem1  32523  kur14lem9  32546  cnllysconn  32577  cvmsss2  32606  cvmcov2  32607  cvmsiota  32609  cvmopnlem  32610  cvmliftlem15  32630  satfv1  32695  satfdmlem  32700  mclsssvlem  32894  mclsind  32902  untelirr  33019  untsucf  33021  elintfv  33092  dfon2lem4  33116  dfon2lem7  33119  dfon2lem9  33121  soseq  33181  nodenselem8  33280  noetalem3  33304  nocvxminlem  33332  dfiota3  33469  funpartlem  33488  funpartfun  33489  linethru  33699  hilbert1.1  33700  rankelg  33714  elhf2  33721  neibastop2lem  33793  bj-rabeqd  34334  bj-zfauscl  34339  bj-cleq  34370  bj-snsetex  34371  bj-nuliota  34446  mptsnunlem  34727  isbasisrelowllem1  34744  isbasisrelowllem2  34745  relowlssretop  34752  relowlpssretop  34753  exrecfnlem  34768  finxpeq1  34775  finxpreclem5  34784  finxpreclem6  34785  nlpineqsn  34797  fvineqsneu  34800  fvineqsneq  34801  pibt2  34806  unccur  35012  fin2so  35016  matunitlindflem1  35025  ptrecube  35029  poimirlem9  35038  poimirlem30  35059  poimir  35062  heicant  35064  mblfinlem1  35066  ftc1anc  35110  ftc2nc  35111  cover2  35124  isbnd2  35193  prdstotbnd  35204  heibor1lem  35219  grpokerinj  35303  rngoueqz  35350  isidl  35424  1idl  35436  0rngo  35437  ispridl  35444  smprngopr  35462  isfldidl  35478  isdmn3  35484  mpobi123f  35572  iineq12f  35574  mptbi12f  35576  eqvrelqsel  35983  n0eldmqseq  36016  dmqseqim2  36023  lsateln0  36263  ispsubsp  37013  linepsubN  37020  elpcliN  37161  dvh3dim3N  38717  dochsnnz  38718  mapdindp3  38990  prjspval  39541  elmzpcl  39611  diophren  39698  dford3lem2  39912  ttac  39921  pw2f1ocnv  39922  wepwsolem  39930  kelac1  39951  intabssd  40171  elmapintrab  40220  eliunov2  40324  gneispaceel2  40794  mnuop23d  40922  mnuunid  40933  mnurndlem1  40937  expgrowthi  40985  dvconstbi  40986  tratrb  41190  suctrALT2VD  41490  suctrALT2  41491  en3lplem1VD  41497  en3lpVD  41499  tratrbVD  41515  suctrALTcf  41576  suctrALTcfVD  41577  suctrALT3  41578  unisnALT  41580  restuni3  41703  supminfxr  42056  xlimxrre  42426  xlimmnfvlem1  42427  xlimpnfvlem1  42431  icccncfext  42482  stoweidlem27  42622  stoweidlem35  42630  stoweidlem46  42641  stoweidlem52  42647  ioorrnopnlem  42899  ioorrnopnxrlem  42901  issal  42909  intsaluni  42922  salgencntex  42936  sge0f1o  42974  smfresal  43373  funressnfv  43588  fnbrafvb  43663  afvco2  43685  ndmaovg  43693  aovmpt4g  43710  fafv2elrnb  43744  fzoopth  43837  fvelsetpreimafv  43857  elsetpreimafvbi  43861  sprsymrelf1lem  43961  paireqne  43981  fpprbasnn  44200  nnsum4primeseven  44271  nnsum4primesevenALTV  44272  issubmgm  44362  c0snmgmhm  44491  c0snmhm  44492  rngccatidALTV  44566  ringccatidALTV  44629  ldepspr  44835
  Copyright terms: Public domain W3C validator