Theorem eleq2 2828

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eleq2d 2825	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  eleq12  2829  eleq2i  2831  nelneq2  2865  clelsb2OLD  2869  dvelimdc  2935  raleqf  3333  rexeqf  3334  reueq1f  3335  rmoeq1f  3336  reueq1  3345  rmoeq1  3346  raleleq  3357  rabeqf  3416  rabeqiOLD  3418  rabeq  3419  clel3g  3592  clel4g  3594  clel4OLD  3596  sbcbi2  3779  sbcel2gv  3789  csbeq2  3838  difeq2  4052  uneq1  4091  unineq  4212  nel02  4267  n0i  4268  sbnfc2  4371  disjel  4391  elif  4503  exsnrex  4617  elinsn  4647  sneqrg  4771  preq1b  4778  preq12b  4782  elpreqprb  4799  elunii  4845  elinti  4889  intss1  4895  intmin  4900  intab  4910  iuneqconst  4936  iineq2  4945  dfiun2g  4961  dfiin2g  4963  breq  5077  zfrepclf  5219  zfauscl  5226  sseliALT  5234  inuni  5268  sels  5357  elALT  5359  rext  5365  intid  5374  elopg  5382  opth1  5391  opthwiener  5429  xpeq1  5604  xpeq2  5611  0nelelxp  5625  opthprc  5652  ordtri1  6303  ordtri3  6306  nsuceq0  6350  suctr  6353  ordnbtwn  6360  funopg  6475  dffv2  6872  fveqdmss  6965  dffo4  6988  funopdmsn  7031  fnsnb  7047  elunirn  7133  f1oiso  7231  canth  7238  eusvobj2  7277  mpoeq123  7356  ndmovg  7464  uniuni  7621  iunpw  7630  oneqmin  7659  onuninsuci  7696  nlimsucg  7698  limomss  7726  nnlim  7735  peano5  7749  peano5OLD  7750  unielxp  7878  cnvf1o  7960  smoel  8200  smo11  8204  tz7.44-2  8247  nlim2  8329  ord1eln01  8335  ord2eln012  8336  oawordeulem  8394  oaordex  8398  omordi  8406  oneo  8421  oeordi  8427  oeoa  8437  oeoe  8439  nnmordi  8471  nnaordex  8478  omabs  8490  nnneo  8494  omsmolem  8496  elqsn0  8584  qsel  8594  mapsnd  8683  undifixp  8731  boxriin  8737  boxcutc  8738  pssnn  8960  fineqvlem  9046  fineqv  9047  pssnnOLD  9049  fissuni  9133  dffi2  9191  inficl  9193  dffi3  9199  wofib  9313  zfregcl  9362  en3lplem1  9379  en3lp  9381  suc11reg  9386  inf0  9388  inf3lem2  9396  inf3lem3  9397  infeq5i  9403  axinf2  9407  dfom3  9414  elom3  9415  cantnfle  9438  oemapvali  9451  cantnflem1  9456  tc2  9509  r1sdom  9541  rankwflemb  9560  rankval3b  9593  rankunb  9617  rankuni2b  9620  cardlim  9739  cardprclem  9746  infxpenlem  9778  alephnbtwn  9836  alephordi  9839  cardaleph  9854  alephfp  9873  alephval3  9875  dfac3  9886  dfac5lem2  9889  dfac5lem4  9891  dfac2b  9895  kmlem2  9916  coflim  10026  cfsmolem  10035  fin23lem30  10107  isf34lem4  10142  axdc2lem  10213  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  zorn2lem7  10267  axdclem  10284  brdom7disj  10296  brdom6disj  10297  axpowndlem3  10364  winainflem  10458  iswun  10469  eltskg  10515  inar1  10540  elgrug  10557  inaprc  10601  eltskm  10608  addnidpi  10666  indpi  10672  nqereu  10694  elnp  10752  elnpi  10753  genpnnp  10770  ltaddpr  10799  dfnn2  11995  dfnn3  11996  dfuzi  12420  uz11  12616  elfzonlteqm1  13472  om2uzlti  13679  axdc4uz  13713  hashrabsn1  14098  hashbclem  14173  hashf1lem2  14179  hash2prb  14195  hash2prd  14198  wrdsymb0  14261  lsw0  14277  swrdwrdsymb  14384  rtrclreclem3  14780  prodeq1f  15627  rpnnen2lem1  15932  rpnnen2lem2  15933  lcmfval  16335  lcmf0val  16336  ismre  17308  isacs  17369  initoid  17725  termoid  17726  initoeu2lem1  17738  clatl  18235  mreclatBAD  18290  issubm  18451  dfgrp2e  18614  isnsg  18792  cycsubg  18836  resghm  18859  ghmeql  18866  gsmsymgreq  19049  f1otrspeq  19064  pmtrval  19068  pmtrdifellem4  19096  pmtrprfval  19104  gsumzsplit  19537  pgpfac1lem1  19686  pgpfac1lem5  19691  pgpfac1  19692  ablsimpnosubgd  19716  issubrg  20033  lmodfopnelem2  20169  islss  20205  lspsneq0  20283  lmhmeql  20326  lspdisjb  20397  lidl1el  20498  lidldvgen  20535  0ring01eq  20551  islindf4  21054  mplcoe1  21247  mplcoe5  21250  selvfval  21336  m1detdiag  21755  mdetunilem9  21778  maducoeval2  21798  madugsum  21801  chpmat1dlem  21993  istopg  22053  toprntopon  22083  fiinbas  22111  topbas  22131  ppttop  22166  pptbas  22167  epttop  22168  elcls  22233  clsndisj  22235  iscldtop  22255  neiptopnei  22292  restbas  22318  restntr  22342  pnfnei  22380  mnfnei  22381  cnpimaex  22416  lmcvg  22422  iscnp4  22423  cncnpi  22438  cnconst2  22443  cnprest  22449  cnprest2  22450  cnpdis  22453  lmss  22458  lmff  22461  cnt0  22506  ist1-3  22509  cnhaus  22514  isreg2  22537  dishaus  22542  ordthauslem  22543  cmpsublem  22559  cmpsub  22560  cmpcld  22562  hauscmplem  22566  unconn  22589  conncompid  22591  conncompss  22593  1stcfb  22605  1stcrest  22613  2ndcctbss  22615  2ndcomap  22618  dis2ndc  22620  1stcelcls  22621  llyeq  22630  nllyeq  22631  restnlly  22642  islly2  22644  lly1stc  22656  dislly  22657  hauspwdom  22661  finlocfin  22680  unisngl  22687  dissnlocfin  22689  locfindis  22690  comppfsc  22692  llycmpkgen2  22710  txbas  22727  eltx  22728  ptpjopn  22772  ptclsg  22775  txcnp  22780  ptcnplem  22781  ptcnp  22782  txlly  22796  pthaus  22798  txtube  22800  txhaus  22807  txlm  22808  tx1stc  22810  txkgen  22812  xkohaus  22813  xkopt  22815  xkococnlem  22819  tgqtop  22872  kqfvima  22890  kqt0lem  22896  isr0  22897  regr1lem  22899  kqreglem1  22901  kqreglem2  22902  reghmph  22953  fbssfi  22997  isfil  23007  filuni  23045  isufil  23063  isufil2  23068  fixufil  23082  uffixfr  23083  uffixsn  23085  rnelfm  23113  flimopn  23135  flimrest  23143  flimcls  23145  txflf  23166  fclsopni  23175  fclsrest  23184  fclscf  23185  fcfnei  23195  alexsublem  23204  alexsubALTlem3  23209  alexsubALT  23211  tmdgsum2  23256  symgtgp  23266  subgntr  23267  opnsubg  23268  ghmcnp  23275  tgpt0  23279  qustgpopn  23280  tsmsi  23294  tsmssubm  23303  tsmssplit  23312  isust  23364  ustn0  23381  blssps  23586  blss  23587  blssexps  23588  blssex  23589  neibl  23666  blcld  23670  metss  23673  methaus  23685  met1stc  23686  met2ndci  23687  metrest  23689  prdsxmslem2  23694  metcnp3  23705  dscopn  23738  idnghm  23916  qdensere  23942  tgioo  23968  tgqioo  23972  zdis  23988  xrge0tsms  24006  cnheibor  24127  lmmbr  24431  bcthlem4  24500  ovolicc2lem5  24694  dyadmbllem  24772  i1fd  24854  itg11  24864  itg2gt0  24934  itgeq1f  24945  bddmulibl  25012  ellimc2  25050  limcnlp  25051  ellimc3  25052  limcflf  25054  limciun  25067  lhop1lem  25186  ig1pdvds  25350  plycpn  25458  aannenlem2  25498  efopn  25822  xrlimcnp  26127  wilthlem2  26227  wilthlem3  26228  tghilberti1  27007  colline  27019  lmif  27155  islmib  27157  incistruhgr  27458  upgr1eopALT  27496  uhgrvtxedgiedgb  27515  upgredg2vtx  27520  edglnl  27522  numedglnl  27523  uhgr2edg  27584  umgrvad2edg  27589  usgredg4  27593  usgredg2vtxeuALT  27598  uspgredg2vlem  27599  ushgredgedg  27605  nbgr1vtx  27734  nbusgredgeu0  27744  nbusgrf1o0  27745  nb3grprlem1  27756  nb3grprlem2  27757  uvtx01vtx  27773  nbupgruvtxres  27783  cplgr1vlem  27805  cplgr1v  27806  vtxd0nedgb  27864  vtxduhgr0nedg  27868  1loopgrvd2  27879  1egrvtxdg0  27887  uspgrloopvtxel  27892  vtxdginducedm1lem4  27918  wlk1walk  28015  wlkp1lem1  28050  pthdivtx  28106  0enwwlksnge1  28238  umgrwwlks2on  28331  rusgr0edg  28347  eleclclwwlkn  28449  upgr4cycl4dv4e  28558  1conngr  28567  vdn0conngrumgrv2  28569  eupth2eucrct  28590  eupth2lem1  28591  frgrncvvdeqlem7  28678  frgrncvvdeqlem9  28680  frgrwopregasn  28689  frgrwopregbsn  28690  l2p  28850  lpni  28851  issh  29579  pjoc1  29805  h1dn0  29923  spansneleqi  29940  nonbooli  30022  pjch  30065  pjnel  30097  cdjreui  30803  rexunirn  30849  rabsnel  30856  nelun  30868  iinabrex  30917  opabdm  30960  opabrn  30961  fpwrelmapffslem  31076  fpwrelmap  31077  fz1nntr  31134  xrge0tsmsd  31326  nsgqusf1olem3  31609  elrspunidl  31615  isprmidl  31622  reff  31798  tpr2rico  31871  lmxrge0  31911  indval  31990  issiga  32089  isrnsiga  32090  isldsys  32133  isros  32145  issros  32152  ddeval1  32211  ddeval0  32212  ismbfm  32228  isanmbfm  32232  dya2icoseg  32253  dya2iocnrect  32257  ballotlem7  32511  bnj216  32720  bnj563  32732  bnj956  32765  bnj545  32884  bnj548  32886  bnj570  32894  bnj900  32918  bnj929  32925  bnj964  32932  bnj983  32940  bnj1001  32948  bnj1145  32982  bnj1398  33023  bnj1498  33050  erdszelem1  33162  kur14lem9  33185  cnllysconn  33216  cvmsss2  33245  cvmcov2  33246  cvmsiota  33248  cvmopnlem  33249  cvmliftlem15  33269  satfv1  33334  satfdmlem  33339  mclsssvlem  33533  mclsind  33541  untelirr  33658  untsucf  33660  elintfv  33747  dfon2lem4  33771  dfon2lem7  33774  dfon2lem9  33776  soseq  33812  nodenselem8  33903  noetasuplem4  33948  noetainflem4  33952  nocvxminlem  33981  lrrecfr  34109  dfiota3  34234  funpartlem  34253  funpartfun  34254  linethru  34464  hilbert1.1  34465  rankelg  34479  elhf2  34486  neibastop2lem  34558  bj-rabeqd  35116  bj-zfauscl  35121  bj-cleq  35161  bj-snsetex  35162  bj-clel3gALT  35230  bj-nuliota  35237  bj-isrvec  35474  mptsnunlem  35518  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlssretop  35543  relowlpssretop  35544  exrecfnlem  35559  finxpeq1  35566  finxpreclem5  35575  finxpreclem6  35576  nlpineqsn  35588  fvineqsneu  35591  fvineqsneq  35592  pibt2  35597  unccur  35769  fin2so  35773  matunitlindflem1  35782  ptrecube  35786  poimirlem9  35795  poimirlem30  35816  poimir  35819  heicant  35821  mblfinlem1  35823  ftc1anc  35867  ftc2nc  35868  cover2  35881  isbnd2  35950  prdstotbnd  35961  heibor1lem  35976  grpokerinj  36060  rngoueqz  36107  isidl  36181  1idl  36193  0rngo  36194  ispridl  36201  smprngopr  36219  isfldidl  36235  isdmn3  36241  mpobi123f  36329  iineq12f  36331  mptbi12f  36333  eqvrelqsel  36736  n0eldmqseq  36769  dmqseqim2  36776  lsateln0  37016  ispsubsp  37766  linepsubN  37773  elpcliN  37914  dvh3dim3N  39470  dochsnnz  39471  mapdindp3  39743  sn-iotalem  40196  prjspval  40449  prjcrv0  40477  elmzpcl  40555  diophren  40642  dford3lem2  40856  ttac  40865  pw2f1ocnv  40866  wepwsolem  40874  kelac1  40895  nlimsuc  41055  intabssd  41133  elmapintrab  41191  eliunov2  41294  gneispaceel2  41761  mnuop23d  41891  mnuunid  41902  mnurndlem1  41906  expgrowthi  41958  dvconstbi  41959  tratrb  42163  suctrALT2VD  42463  suctrALT2  42464  en3lplem1VD  42470  en3lpVD  42472  tratrbVD  42488  suctrALTcf  42549  suctrALTcfVD  42550  suctrALT3  42551  unisnALT  42553  restuni3  42674  supminfxr  43011  xlimxrre  43379  xlimmnfvlem1  43380  xlimpnfvlem1  43384  icccncfext  43435  stoweidlem27  43575  stoweidlem35  43583  stoweidlem46  43594  stoweidlem52  43600  ioorrnopnlem  43852  ioorrnopnxrlem  43854  issal  43862  intsaluni  43875  salgencntex  43889  sge0f1o  43927  smfresal  44333  funressnfv  44548  fnbrafvb  44657  afvco2  44679  ndmaovg  44687  aovmpt4g  44704  fafv2elrnb  44738  fzoopth  44830  fvelsetpreimafv  44850  elsetpreimafvbi  44854  sprsymrelf1lem  44954  paireqne  44974  fpprbasnn  45192  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  issubmgm  45354  c0snmgmhm  45483  c0snmhm  45484  rngccatidALTV  45558  ringccatidALTV  45621  ldepspr  45825  mosn  46169  indthinc  46344  indthincALT  46345