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 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eleq12  2829  eleq2i  2831  nelneq2  2864  dvelimdc  2925  raleqf  3320  rmoeq1f  3381  rabeq  3405  rabeqd  3419  rabeqf  3425  clel3g  3599  clel4g  3601  sbcel2gv  3789  csbeq2  3836  difeq2  4051  uneq1  4091  unineq  4216  nel02  4267  sbnfc2  4367  disjel  4385  elif  4498  exsnrex  4612  elinsn  4642  sneqrg  4770  preq1b  4777  preq12b  4781  elpreqprb  4799  elunii  4843  elinti  4886  intss1  4893  intmin  4898  intab  4908  iuneqconst  4933  iineq2  4942  dfiun2g  4959  breq  5074  zfrepclf  5213  zfauscl  5220  sseliALT  5231  vneqv  5238  inuni  5278  selsALT  5380  rext  5387  intidg  5396  elopg  5406  opth1  5415  opthwiener  5455  xpeq1  5632  xpeq2  5639  0nelelxp  5653  opthprc  5682  ordtri1  6343  ordtri3  6346  nsuceq0  6395  suctr  6398  ordnbtwn  6405  funopg  6519  dffv2  6922  fveqdmss  7019  dffo4  7044  funopdmsn  7093  fnsnbOLD  7110  elunirn  7195  f1oiso  7295  canth  7310  eusvobj2  7348  mpoeq123  7428  ndmovg  7539  uniuni  7705  iunpw  7714  oneqmin  7743  onuninsuci  7780  nlimsucg  7782  limomss  7811  nnlim  7820  peano5  7833  unielxp  7969  cnvf1o  8050  soseq  8099  smoel  8290  smo11  8294  tz7.44-2  8336  nlim2  8415  ord1eln01  8421  ord2eln012  8422  oawordeulem  8479  oaordex  8483  omordi  8491  oneo  8506  oeordi  8513  oeoa  8523  oeoe  8525  nnmordi  8557  nnaordex  8564  nnaordex2  8565  omabs  8577  nnneo  8581  omsmolem  8583  elqsn0  8721  qsel  8733  mapsnd  8824  undifixp  8872  boxriin  8878  boxcutc  8879  pssnn  9093  fineqvlem  9166  fineqv  9167  en1eqsn  9175  fissuni  9257  dffi2  9326  inficl  9328  dffi3  9334  wofib  9450  zfregcl  9499  zfregclOLD  9500  nelaneq  9507  nelaneqOLD  9508  en3lplem1  9524  en3lp  9526  suc11reg  9531  inf0  9533  inf3lem2  9541  inf3lem3  9542  infeq5i  9548  axinf2  9552  dfom3  9559  elom3  9560  cantnfle  9583  oemapvali  9596  cantnflem1  9601  tc2  9652  r1sdom  9689  rankwflemb  9708  rankval3b  9741  rankunb  9765  rankuni2b  9768  cardlim  9887  cardprclem  9894  infxpenlem  9926  alephnbtwn  9984  alephordi  9987  cardaleph  10002  alephfp  10021  alephval3  10023  dfac3  10034  dfac5lem2  10037  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  kmlem2  10065  coflim  10174  cfsmolem  10183  fin23lem30  10255  isf34lem4  10290  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  zorn2lem7  10415  axdclem  10432  brdom7disj  10444  brdom6disj  10445  axpowndlem3  10513  winainflem  10607  iswun  10618  eltskg  10664  inar1  10689  elgrug  10706  inaprc  10750  eltskm  10757  addnidpi  10815  indpi  10821  nqereu  10843  elnp  10901  elnpi  10902  genpnnp  10919  ltaddpr  10948  indval  12153  dfnn2  12178  dfnn3  12179  dfuzi  12611  uz11  12804  elfzonlteqm1  13687  fzoopth  13708  om2uzlti  13903  axdc4uz  13937  hashrabsn1  14327  hashbclem  14405  hashf1lem2  14409  hash2prb  14425  hash2prd  14428  hash3tpb  14448  wrdsymb0  14502  lsw0  14518  swrdwrdsymb  14616  rtrclreclem3  15013  prodeq1f  15862  prodeq1  15863  rpnnen2lem1  16172  rpnnen2lem2  16173  lcmfval  16581  lcmf0val  16582  ismre  17543  isacs  17608  initoid  17959  termoid  17960  initoeu2lem1  17972  clatl  18465  mreclatBAD  18520  issubmgm  18661  issubm  18762  dfgrp2e  18930  isnsg  19121  cycsubg  19174  resghm  19198  ghmeql  19205  gsmsymgreq  19398  f1otrspeq  19413  pmtrval  19417  pmtrdifellem4  19445  pmtrprfval  19453  gsumzsplit  19893  pgpfac1lem1  20042  pgpfac1lem5  20047  pgpfac1  20048  ablsimpnosubgd  20072  c0snmgmhm  20433  c0snmhm  20434  0ring01eq  20501  issubrg  20543  lmodfopnelem2  20889  islss  20924  lspsneq0  21002  lmhmeql  21045  lspdisjb  21119  lidl1el  21219  rngqiprngfulem2  21305  rngqipring1  21309  lidldvgen  21327  islindf4  21813  mplcoe1  22013  mplcoe5  22016  selvfval  22095  m1detdiag  22580  mdetunilem9  22603  maducoeval2  22623  madugsum  22626  chpmat1dlem  22818  istopg  22878  toprntopon  22908  fiinbas  22935  topbas  22955  ppttop  22990  pptbas  22991  epttop  22992  elcls  23056  clsndisj  23058  iscldtop  23078  neiptopnei  23115  restbas  23141  restntr  23165  pnfnei  23203  mnfnei  23204  cnpimaex  23239  lmcvg  23245  iscnp4  23246  cncnpi  23261  cnconst2  23266  cnprest  23272  cnprest2  23273  cnpdis  23276  lmss  23281  lmff  23284  cnt0  23329  ist1-3  23332  cnhaus  23337  isreg2  23360  dishaus  23365  ordthauslem  23366  cmpsublem  23382  cmpsub  23383  cmpcld  23385  hauscmplem  23389  unconn  23412  conncompid  23414  conncompss  23416  1stcfb  23428  1stcrest  23436  2ndcctbss  23438  2ndcomap  23441  dis2ndc  23443  1stcelcls  23444  llyeq  23453  nllyeq  23454  restnlly  23465  islly2  23467  lly1stc  23479  dislly  23480  hauspwdom  23484  finlocfin  23503  unisngl  23510  dissnlocfin  23512  locfindis  23513  comppfsc  23515  llycmpkgen2  23533  txbas  23550  eltx  23551  ptpjopn  23595  ptclsg  23598  txcnp  23603  ptcnplem  23604  ptcnp  23605  txlly  23619  pthaus  23621  txtube  23623  txhaus  23630  txlm  23631  tx1stc  23633  txkgen  23635  xkohaus  23636  xkopt  23638  xkococnlem  23642  tgqtop  23695  kqfvima  23713  kqt0lem  23719  isr0  23720  regr1lem  23722  kqreglem1  23724  kqreglem2  23725  reghmph  23776  fbssfi  23820  isfil  23830  filuni  23868  isufil  23886  isufil2  23891  fixufil  23905  uffixfr  23906  uffixsn  23908  rnelfm  23936  flimopn  23958  flimrest  23966  flimcls  23968  txflf  23989  fclsopni  23998  fclsrest  24007  fclscf  24008  fcfnei  24018  alexsublem  24027  alexsubALTlem3  24032  alexsubALT  24034  tmdgsum2  24079  symgtgp  24089  subgntr  24090  opnsubg  24091  ghmcnp  24098  tgpt0  24102  qustgpopn  24103  tsmsi  24117  tsmssubm  24126  tsmssplit  24135  isust  24187  ustn0  24204  blssps  24407  blss  24408  blssexps  24409  blssex  24410  neibl  24484  blcld  24488  metss  24491  methaus  24503  met1stc  24504  met2ndci  24505  metrest  24507  prdsxmslem2  24512  metcnp3  24523  dscopn  24556  idnghm  24726  qdensere  24752  tgioo  24779  tgqioo  24783  zdis  24800  xrge0tsms  24818  cnheibor  24940  lmmbr  25243  bcthlem4  25312  ovolicc2lem5  25506  dyadmbllem  25584  i1fd  25666  itg11  25676  itg2gt0  25745  itgeq1f  25756  itgeq1fOLD  25757  itgeq1  25758  bddmulibl  25824  ellimc2  25862  limcnlp  25863  ellimc3  25864  limcflf  25866  limciun  25879  lhop1lem  25998  ig1pdvds  26163  plycpn  26273  aannenlem2  26313  efopn  26640  xrlimcnp  26950  wilthlem2  27050  wilthlem3  27051  nodenselem8  27673  noetasuplem4  27718  noetainflem4  27722  nocvxminlem  27764  lrrecfr  27953  addsprop  27986  bdayons  28286  addonbday  28289  dfn0s2  28342  tghilberti1  28723  colline  28735  lmif  28871  islmib  28873  incistruhgr  29166  upgr1eopALT  29204  uhgrvtxedgiedgb  29223  upgredg2vtx  29228  edglnl  29230  numedglnl  29231  uhgr2edg  29295  umgrvad2edg  29300  usgredg4  29304  usgredg2vtxeuALT  29309  uspgredg2vlem  29310  ushgredgedg  29316  nbgr1vtx  29445  nbusgredgeu0  29455  nbusgrf1o0  29456  nb3grprlem1  29467  nb3grprlem2  29468  uvtx01vtx  29484  nbupgruvtxres  29494  cplgr1vlem  29516  cplgr1v  29517  vtxd0nedgb  29575  vtxduhgr0nedg  29579  1loopgrvd2  29590  1egrvtxdg0  29598  uspgrloopvtxel  29603  vtxdginducedm1lem4  29629  wlk1walk  29725  wlkp1lem1  29758  pthdivtx  29813  0enwwlksnge1  29950  usgrwwlks2on  30044  umgrwwlks2on  30045  rusgr0edg  30062  eleclclwwlkn  30164  upgr4cycl4dv4e  30273  1conngr  30282  vdn0conngrumgrv2  30284  eupth2eucrct  30305  eupth2lem1  30306  frgrncvvdeqlem7  30393  frgrncvvdeqlem9  30395  frgrwopregasn  30404  frgrwopregbsn  30405  l2p  30568  lpni  30569  issh  31297  pjoc1  31523  h1dn0  31641  spansneleqi  31658  nonbooli  31740  pjch  31783  pjnel  31815  cdjreui  32521  rexunirn  32579  rabsnel  32588  nelun  32601  iinabrex  32658  opabdm  32703  opabrn  32704  fpwrelmapffslem  32824  fpwrelmap  32825  fz1nntr  32894  xrge0tsmsd  33154  nsgqusf1olem3  33498  elrspunidl  33511  isprmidl  33521  constrmon  33928  reff  34023  tpr2rico  34096  lmxrge0  34136  issiga  34296  isrnsiga  34297  isldsys  34340  isros  34352  issros  34359  ddeval1  34418  ddeval0  34419  ismbfm  34435  dya2icoseg  34461  dya2iocnrect  34465  ballotlem7  34720  bnj216  34915  bnj563  34926  bnj956  34959  bnj545  35077  bnj548  35079  bnj570  35087  bnj900  35111  bnj929  35118  bnj964  35125  bnj983  35133  bnj1001  35141  bnj1145  35175  bnj1398  35216  bnj1498  35243  fineqvnttrclselem2  35303  fineqvnttrclse  35305  fineqvinfep  35306  wevgblacfn  35337  erdszelem1  35419  kur14lem9  35442  cnllysconn  35473  cvmsss2  35502  cvmcov2  35503  cvmsiota  35505  cvmopnlem  35506  cvmliftlem15  35526  satfv1  35591  satfdmlem  35596  mclsssvlem  35790  mclsind  35798  untelirr  35936  untsucf  35938  elintfv  35993  dfon2lem4  36012  dfon2lem7  36015  dfon2lem9  36017  dfiota3  36149  funpartlem  36170  funpartfun  36171  linethru  36381  hilbert1.1  36382  rankelg  36396  elhf2  36403  neibastop2lem  36588  regsfromregtco  36766  regsfromunir1  36768  bj-zfauscl  37277  bj-cleq  37315  bj-snsetex  37316  bj-clel3gALT  37401  bj-nuliota  37410  bj-isrvec  37654  mptsnunlem  37700  isbasisrelowllem1  37717  isbasisrelowllem2  37718  relowlssretop  37725  relowlpssretop  37726  exrecfnlem  37741  finxpeq1  37748  finxpreclem5  37757  finxpreclem6  37758  nlpineqsn  37770  fvineqsneq  37774  pibt2  37779  unccur  37970  fin2so  37974  matunitlindflem1  37983  ptrecube  37987  poimirlem9  37996  poimirlem30  38017  poimir  38020  heicant  38022  mblfinlem1  38024  ftc1anc  38068  ftc2nc  38069  cover2  38082  isbnd2  38150  prdstotbnd  38161  heibor1lem  38176  grpokerinj  38260  rngoueqz  38307  isidl  38381  1idl  38393  0rngo  38394  ispridl  38401  smprngopr  38419  isfldidl  38435  isdmn3  38441  mpobi123f  38529  iineq12f  38531  mptbi12f  38533  dfsuccl4  38841  eqvrelqsel  39067  n0eldmqseq  39101  dmqseqim2  39109  suceldisj  39185  disjlem17  39269  lsateln0  39487  ispsubsp  40237  linepsubN  40244  elpcliN  40385  dvh3dim3N  41941  dochsnnz  41942  mapdindp3  42214  sn-iotalem  42708  prjspval  43053  elmzpcl  43175  diophren  43258  dford3lem2  43472  ttac  43481  pw2f1ocnv  43482  wepwsolem  43487  kelac1  43508  onexgt  43685  onexlimgt  43688  ordnexbtwnsuc  43712  oaordnr  43741  omnord1  43750  nnoeomeqom  43757  oenord1  43761  succlg  43773  oacl2g  43775  omabs2  43777  omcl2  43778  omcl3g  43779  naddwordnexlem4  43846  nlimsuc  43885  intabssd  43963  elmapintrab  44020  eliunov2  44123  gneispaceel2  44588  mnuop23d  44710  mnuunid  44721  mnurndlem1  44725  expgrowthi  44777  dvconstbi  44778  tratrb  44980  suctrALT2VD  45279  suctrALT2  45280  en3lplem1VD  45286  en3lpVD  45288  tratrbVD  45304  suctrALTcf  45365  suctrALTcfVD  45366  suctrALT3  45367  unisnALT  45369  0elaxnul  45427  pwclaxpow  45428  prclaxpr  45429  uniclaxun  45430  omssaxinf2  45432  wfaxrep  45438  restuni3  45565  supminfxr  45907  xlimxrre  46274  xlimmnfvlem1  46275  xlimpnfvlem1  46279  icccncfext  46330  stoweidlem27  46470  stoweidlem35  46478  stoweidlem46  46489  stoweidlem52  46495  ioorrnopnlem  46747  ioorrnopnxrlem  46749  issal  46757  intsaluni  46772  salgencntex  46786  smfresal  47231  tannpoly  47353  funressnfv  47506  fnbrafvb  47617  afvco2  47639  ndmaovg  47647  aovmpt4g  47664  fafv2elrnb  47698  fvelsetpreimafv  47862  elsetpreimafvbi  47866  sprsymrelf1lem  47966  paireqne  47986  fpprbasnn  48220  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  dfclnbgr6  48347  dfsclnbgr6  48349  grtri  48431  stgrvtx0  48453  stgrnbgr0  48455  isubgr3stgrlem3  48459  gpgvtx0  48544  gpgvtx1  48545  gpg3kgrtriex  48580  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  rngccatidALTV  48763  ringccatidALTV  48797  ldepspr  48964  mosn  49303  indthinc  49952  indthincALT  49953