Theorem eleq2 2852

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

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eleq2d 2849	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eleq12  2853  eleq2i  2855  nelneq2  2888  dvelimdc  2949  raleqf  3345  rmoeq1f  3406  rabeq  3430  rabeqd  3444  rabeqf  3450  clel3g  3620  clel4g  3622  sbcel2gv  3810  csbeq2  3858  difeq2  4075  uneq1  4115  unineq  4241  nel02  4292  sbnfc2  4404  disjel  4417  elif  4531  exsnrex  4646  elinsn  4676  sneqrg  4804  preq1b  4811  preq12b  4815  elpreqprb  4833  elunii  4877  elinti  4921  intss1  4928  intmin  4933  intab  4943  iuneqconst  4968  iineq2  4977  dfiun2g  4994  breq  5111  zfrepclf  5252  sepg  5259  zfausclOLD  5261  sseliALT  5272  vneqv  5279  inuni  5320  selsALT  5422  rext  5429  intidg  5438  elopg  5448  opth1  5457  opthwiener  5497  xpeq1  5675  xpeq2  5682  0nelelxp  5696  opthprc  5725  ordtri1  6394  ordtri3  6397  nsuceq0  6446  suctr  6449  ordnbtwn  6456  funopg  6570  dffv2  6976  fveqdmss  7073  dffo4  7098  funopdmsn  7147  fnsnbOLD  7164  elunirn  7249  f1oiso  7349  canth  7364  eusvobj2  7402  mpoeq123  7482  ndmovg  7593  uniuni  7757  iunpw  7766  oneqmin  7795  onuninsuci  7832  nlimsucg  7834  limomss  7863  nnlim  7872  peano5  7886  unielxp  8020  cnvf1o  8102  soseq  8151  smoel  8343  smo11  8347  tz7.44-2  8390  nlim2  8471  ord1eln01  8477  ord2eln012  8478  oawordeulem  8535  oaordex  8539  omordi  8547  oneo  8562  oeordi  8569  oeoa  8579  oeoe  8581  nnmordi  8613  nnaordex  8620  nnaordex2  8621  omabs  8633  nnneo  8637  omsmolem  8639  elqsn0  8778  qsel  8790  mapsnd  8880  undifixp  8928  boxriin  8934  boxcutc  8935  pssnn  9149  fineqvlem  9222  fineqv  9223  en1eqsn  9231  fissuni  9310  dffi2  9379  inficl  9381  dffi3  9387  wofib  9503  zfregcl  9552  zfregclOLD  9553  nelaneq  9560  nelaneqOLD  9561  en3lplem1  9577  en3lp  9579  suc11reg  9584  inf0  9586  inf3lem2  9594  inf3lem3  9595  infeq5i  9601  axinf2  9605  dfom3  9612  elom3  9613  cantnfle  9636  oemapvali  9649  cantnflem1  9654  tc2  9705  r1sdom  9742  rankwflemb  9761  rankval3b  9794  rankunb  9818  rankuni2b  9821  cardlim  9954  cardprclem  9961  infxpenlem  9993  alephnbtwn  10051  alephordi  10054  cardaleph  10069  alephfp  10088  alephval3  10090  dfac3  10101  dfac5lem2  10104  dfac5lem4  10106  dfac2b  10110  kmlem2  10131  coflim  10240  cfsmolem  10249  fin23lem30  10321  isf34lem4  10356  axdc2lem  10427  axdc3lem2  10430  axdc3lem4  10432  axdc4lem  10434  zorn2lem7  10481  axdclem  10498  brdom7disj  10510  brdom6disj  10511  axpowndlem3  10579  winainflem  10673  iswun  10684  eltskg  10730  inar1  10755  elgrug  10772  inaprc  10816  eltskm  10823  addnidpi  10881  indpi  10887  nqereu  10909  elnp  10967  elnpi  10968  genpnnp  10985  ltaddpr  11014  indval  12216  dfnn2  12241  dfnn3  12242  dfuzi  12682  uz11  12882  elfzonlteqm1  13766  fzoopth  13787  om2uzlti  13982  axdc4uz  14016  hashrabsn1  14406  hashbclem  14485  hashf1lem2  14489  hash2prb  14505  hash2prd  14508  hash3tpb  14528  wrdsymb0  14582  lsw0  14598  swrdwrdsymb  14696  rtrclreclem3  15093  prodeq1f  15956  prodeq1  15957  rpnnen2lem1  16265  rpnnen2lem2  16266  lcmfval  16674  lcmf0val  16675  ismre  17637  isacs  17702  initoid  18053  termoid  18054  initoeu2lem1  18066  clatl  18559  mreclatBAD  18614  issubmgm  18755  issubm  18856  dfgrp2e  19025  isnsg  19216  cycsubg  19274  resghm  19297  ghmeql  19304  gsmsymgreq  19497  f1otrspeq  19512  pmtrval  19516  pmtrdifellem4  19544  pmtrprfval  19552  gsumzsplit  19992  pgpfac1lem1  20141  pgpfac1lem5  20146  pgpfac1  20147  ablsimpnosubgd  20171  c0snmgmhm  20540  c0snmhm  20541  0ring01eq  20627  issubrg  20670  lmodfopnelem2  21020  islss  21055  lspsneq0  21133  lmhmeql  21176  lspdisjb  21250  lidl1el  21351  rngqiprngfulem2  21452  rngqipring1  21456  isprmidl  21463  lidldvgen  21502  islindf4  21988  mplcoe1  22188  mplcoe5  22191  selvfval  22270  m1detdiag  22754  mdetunilem9  22777  maducoeval2  22797  madugsum  22800  chpmat1dlem  22992  istopg  23052  toprntopon  23082  fiinbas  23109  topbas  23129  ppttop  23164  pptbas  23165  epttop  23166  elcls  23230  clsndisj  23232  iscldtop  23252  neiptopnei  23289  restbas  23315  restntr  23339  pnfnei  23377  mnfnei  23378  cnpimaex  23413  lmcvg  23419  iscnp4  23420  cncnpi  23435  cnconst2  23440  cnprest  23446  cnprest2  23447  cnpdis  23450  lmss  23455  lmff  23458  cnt0  23503  ist1-3  23506  cnhaus  23511  isreg2  23534  dishaus  23539  ordthauslem  23540  cmpsublem  23556  cmpsub  23557  cmpcld  23559  hauscmplem  23563  unconn  23586  conncompid  23588  conncompss  23590  1stcfb  23602  1stcrest  23610  2ndcctbss  23612  2ndcomap  23615  dis2ndc  23617  1stcelcls  23618  llyeq  23627  nllyeq  23628  restnlly  23639  islly2  23641  lly1stc  23653  dislly  23654  hauspwdom  23658  finlocfin  23677  unisngl  23684  dissnlocfin  23686  locfindis  23687  comppfsc  23689  llycmpkgen2  23707  txbas  23724  eltx  23725  ptpjopn  23769  ptclsg  23772  txcnp  23777  ptcnplem  23778  ptcnp  23779  txlly  23793  pthaus  23795  txtube  23797  txhaus  23804  txlm  23805  tx1stc  23807  txkgen  23809  xkohaus  23810  xkopt  23812  xkococnlem  23816  tgqtop  23869  kqfvima  23887  kqt0lem  23893  isr0  23894  regr1lem  23896  kqreglem1  23898  kqreglem2  23899  reghmph  23950  fbssfi  23994  isfil  24004  filuni  24042  isufil  24060  isufil2  24065  fixufil  24079  uffixfr  24080  uffixsn  24082  rnelfm  24110  flimopn  24132  flimrest  24140  flimcls  24142  txflf  24163  fclsopni  24172  fclsrest  24181  fclscf  24182  fcfnei  24192  alexsublem  24201  alexsubALTlem3  24206  alexsubALT  24208  tmdgsum2  24253  symgtgp  24263  subgntr  24264  opnsubg  24265  ghmcnp  24272  tgpt0  24276  qustgpopn  24277  tsmsi  24291  tsmssubm  24300  tsmssplit  24309  isust  24361  ustn0  24378  blssps  24581  blss  24582  blssexps  24583  blssex  24584  neibl  24658  blcld  24662  metss  24665  methaus  24677  met1stc  24678  met2ndci  24679  metrest  24681  prdsxmslem2  24686  metcnp3  24697  dscopn  24730  idnghm  24900  qdensere  24926  tgioo  24953  tgqioo  24957  zdis  24974  xrge0tsms  24992  cnheibor  25114  lmmbr  25417  bcthlem4  25486  ovolicc2lem5  25680  dyadmbllem  25758  i1fd  25840  itg11  25850  itg2gt0  25919  itgeq1f  25930  itgeq1fOLD  25931  itgeq1  25932  bddmulibl  25998  ellimc2  26036  limcnlp  26037  ellimc3  26038  limcflf  26040  limciun  26053  lhop1lem  26172  ig1pdvds  26337  plycpn  26450  aannenlem2  26492  efopn  26823  xrlimcnp  27133  wilthlem2  27233  wilthlem3  27234  nodenselem8  27855  noetasuplem4  27900  noetainflem4  27904  nocvxminlem  27947  lrrecfr  28136  addsprop  28169  bdayons  28469  addonbday  28472  dfn0s2  28525  tghilberti1  28910  colline  28923  lmif  29094  islmib  29096  prlngex  29201  prlngeq  29207  incistruhgr  29429  upgr1eopALT  29467  uhgrvtxedgiedgb  29486  upgredg2vtx  29491  edglnl  29493  numedglnl  29494  uhgr2edg  29558  umgrvad2edg  29563  usgredg4  29567  usgredg2vtxeuALT  29572  uspgredg2vlem  29573  ushgredgedg  29579  nbgr1vtx  29708  nbusgredgeu0  29718  nbusgrf1o0  29719  nb3grprlem1  29730  nb3grprlem2  29731  uvtx01vtx  29747  nbupgruvtxres  29757  cplgr1vlem  29779  cplgr1v  29780  vtxd0nedgb  29838  vtxduhgr0nedg  29842  1loopgrvd2  29853  1egrvtxdg0  29861  uspgrloopvtxel  29866  vtxdginducedm1lem4  29892  wlk1walk  29988  wlkp1lem1  30021  pthdivtx  30076  0enwwlksnge1  30213  usgrwwlks2on  30307  umgrwwlks2on  30308  rusgr0edg  30325  eleclclwwlkn  30427  upgr4cycl4dv4e  30536  1conngr  30545  vdn0conngrumgrv2  30547  eupth2eucrct  30568  eupth2lem1  30569  frgrncvvdeqlem7  30656  frgrncvvdeqlem9  30658  frgrwopregasn  30667  frgrwopregbsn  30668  l2p  30831  lpni  30832  issh  31560  pjoc1  31786  h1dn0  31904  spansneleqi  31921  nonbooli  32003  pjch  32046  pjnel  32078  cdjreui  32784  rexunirn  32838  rabsnel  32846  nelun  32859  iinabrex  32914  opabdm  32956  opabrn  32957  fpwrelmapffslem  33077  fpwrelmap  33078  fz1nntr  33147  xrge0tsmsd  33393  nsgqusf1olem3  33724  elrspunidl  33736  constrmon  34134  reff  34229  tpr2rico  34302  lmxrge0  34342  issiga  34502  isrnsiga  34503  isldsys  34546  isros  34558  issros  34565  ddeval1  34624  ddeval0  34625  ismbfm  34641  dya2icoseg  34667  dya2iocnrect  34671  ballotlem7  34926  bnj216  35121  bnj563  35132  bnj956  35165  bnj545  35283  bnj548  35285  bnj570  35293  bnj900  35317  bnj929  35324  bnj964  35331  bnj983  35339  bnj1001  35347  bnj1145  35381  bnj1398  35422  bnj1498  35449  fineqvnttrclselem2  35535  fineqvnttrclse  35537  fineqvinfep  35538  wevgblacfn  35595  erdszelem1  35683  kur14lem9  35706  cnllysconn  35737  cvmsss2  35766  cvmcov2  35767  cvmsiota  35769  cvmopnlem  35770  cvmliftlem15  35790  satfv1  35855  satfdmlem  35860  mclsssvlem  36054  mclsind  36062  untelirr  36200  untsucf  36202  elintfv  36257  dfon2lem4  36276  dfon2lem7  36279  dfon2lem9  36281  dfiota3  36413  funpartlem  36434  funpartfun  36435  linethru  36645  hilbert1.1  36646  rankelg  36660  elhf2  36667  ltnadd  36710  neibastop2lem  36891  regsfromregtco  37069  regsfromunir1  37071  bj-sepg  37579  bj-cleq  37618  bj-snsetex  37619  bj-clel3gALT  37704  bj-nuliota  37713  bj-isrvec  37958  mptsnunlem  38004  isbasisrelowllem1  38021  isbasisrelowllem2  38022  relowlssretop  38029  relowlpssretop  38030  exrecfnlem  38045  finxpeq1  38052  finxpreclem5  38061  finxpreclem6  38062  nlpineqsn  38074  fvineqsneq  38078  pibt2  38083  unccur  38274  fin2so  38278  matunitlindflem1  38287  ptrecube  38291  poimirlem9  38300  poimirlem30  38321  poimir  38324  heicant  38326  mblfinlem1  38328  ftc1anc  38372  ftc2nc  38373  cover2  38386  isbnd2  38454  prdstotbnd  38465  heibor1lem  38480  grpokerinj  38564  rngoueqz  38611  isidl  38685  1idl  38697  0rngo  38698  ispridl  38705  smprngopr  38723  isfldidl  38739  isdmn3  38745  mpobi123f  38831  iineq12f  38833  mptbi12f  38835  dfsuccl4  39143  eqvrelqsel  39369  n0eldmqseq  39403  dmqseqim2  39411  suceldisj  39487  disjlem17  39571  lsateln0  39789  ispsubsp  40539  linepsubN  40546  elpcliN  40687  dvh3dim3N  42243  dochsnnz  42244  mapdindp3  42516  sn-iotalem  43012  prjspval  43355  elmzpcl  43477  diophren  43560  dford3lem2  43774  ttac  43783  pw2f1ocnv  43784  wepwsolem  43789  kelac1  43810  onexgt  43987  onexlimgt  43990  ordnexbtwnsuc  44014  oaordnr  44043  omnord1  44052  nnoeomeqom  44059  oenord1  44063  succlg  44075  oacl2g  44077  omabs2  44079  omcl2  44080  omcl3g  44081  naddwordnexlem4  44148  nlimsuc  44187  intabssd  44265  elmapintrab  44322  eliunov2  44425  gneispaceel2  44890  mnuop23d  44996  mnuunid  45007  mnurndlem1  45011  expgrowthi  45063  dvconstbi  45064  tratrb  45265  suctrALT2VD  45564  suctrALT2  45565  en3lplem1VD  45571  en3lpVD  45573  tratrbVD  45589  suctrALTcf  45650  suctrALTcfVD  45651  suctrALT3  45652  unisnALT  45654  0elaxnul  45712  pwclaxpow  45713  prclaxpr  45714  uniclaxun  45715  omssaxinf2  45717  wfaxrep  45723  restuni3  45856  supminfxr  46198  xlimxrre  46565  xlimmnfvlem1  46566  xlimpnfvlem1  46570  icccncfext  46621  stoweidlem27  46761  stoweidlem35  46769  stoweidlem46  46780  stoweidlem52  46786  ioorrnopnlem  47038  ioorrnopnxrlem  47040  issal  47048  intsaluni  47063  salgencntex  47077  smfresal  47522  tannpoly  47647  funressnfv  47800  fnbrafvb  47911  afvco2  47933  ndmaovg  47941  aovmpt4g  47958  fafv2elrnb  47992  fvelsetpreimafv  48156  elsetpreimafvbi  48160  sprsymrelf1lem  48260  paireqne  48280  fpprbasnn  48514  nnsum4primeseven  48585  nnsum4primesevenALTV  48586  dfclnbgr6  48641  dfsclnbgr6  48643  grtri  48725  stgrvtx0  48747  stgrnbgr0  48749  isubgr3stgrlem3  48753  gpgvtx0  48838  gpgvtx1  48839  gpg3kgrtriex  48874  pgnbgreunbgrlem3  48903  pgnbgreunbgrlem6  48909  rngccatidALTV  49057  ringccatidALTV  49091  prmringnzring  49122  isidom3  49130  ldepspr  49273  mosn  49611  indthinc  50260  indthincALT  50261