Theorem eleq2 2858

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 2855	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eleq12  2859  eleq2i  2861  nelneq2  2894  dvelimdc  2955  raleqf  3352  rmoeq1f  3413  rabeq  3437  rabeqd  3451  rabeqf  3457  clel3g  3629  clel4g  3631  sbcel2gv  3819  csbeq2  3866  difeq2  4083  uneq1  4123  unineq  4249  nel02  4300  sbnfc2  4410  disjel  4423  elif  4536  exsnrex  4651  elinsn  4681  sneqrg  4808  preq1b  4815  preq12b  4819  elpreqprb  4837  elunii  4881  elinti  4925  intss1  4932  intmin  4937  intab  4947  iuneqconst  4972  iineq2  4981  dfiun2g  4998  breq  5115  zfrepclf  5256  zfauscl  5263  sseliALT  5274  vneqv  5281  inuni  5321  selsALT  5423  rext  5430  intidg  5439  elopg  5449  opth1  5458  opthwiener  5498  xpeq1  5676  xpeq2  5683  0nelelxp  5697  opthprc  5726  ordtri1  6395  ordtri3  6398  nsuceq0  6447  suctr  6450  ordnbtwn  6457  funopg  6571  dffv2  6977  fveqdmss  7074  dffo4  7099  funopdmsn  7148  fnsnbOLD  7165  elunirn  7250  f1oiso  7350  canth  7365  eusvobj2  7403  mpoeq123  7483  ndmovg  7594  uniuni  7761  iunpw  7770  oneqmin  7799  onuninsuci  7836  nlimsucg  7838  limomss  7867  nnlim  7876  peano5  7890  unielxp  8024  cnvf1o  8106  soseq  8155  smoel  8347  smo11  8351  tz7.44-2  8394  nlim2  8475  ord1eln01  8481  ord2eln012  8482  oawordeulem  8539  oaordex  8543  omordi  8551  oneo  8566  oeordi  8573  oeoa  8583  oeoe  8585  nnmordi  8617  nnaordex  8624  nnaordex2  8625  omabs  8637  nnneo  8641  omsmolem  8643  elqsn0  8782  qsel  8794  mapsnd  8884  undifixp  8932  boxriin  8938  boxcutc  8939  pssnn  9153  fineqvlem  9226  fineqv  9227  en1eqsn  9235  fissuni  9314  dffi2  9383  inficl  9385  dffi3  9391  wofib  9507  zfregcl  9556  zfregclOLD  9557  nelaneq  9564  nelaneqOLD  9565  en3lplem1  9581  en3lp  9583  suc11reg  9588  inf0  9590  inf3lem2  9598  inf3lem3  9599  infeq5i  9605  axinf2  9609  dfom3  9616  elom3  9617  cantnfle  9640  oemapvali  9653  cantnflem1  9658  tc2  9709  r1sdom  9746  rankwflemb  9765  rankval3b  9798  rankunb  9822  rankuni2b  9825  cardlim  9958  cardprclem  9965  infxpenlem  9997  alephnbtwn  10055  alephordi  10058  cardaleph  10073  alephfp  10092  alephval3  10094  dfac3  10105  dfac5lem2  10108  dfac5lem4  10110  dfac2b  10114  kmlem2  10135  coflim  10245  cfsmolem  10254  fin23lem30  10326  isf34lem4  10361  axdc2lem  10432  axdc3lem2  10435  axdc3lem4  10437  axdc4lem  10439  zorn2lem7  10486  axdclem  10503  brdom7disj  10515  brdom6disj  10516  axpowndlem3  10584  winainflem  10678  iswun  10689  eltskg  10735  inar1  10760  elgrug  10777  inaprc  10821  eltskm  10828  addnidpi  10886  indpi  10892  nqereu  10914  elnp  10972  elnpi  10973  genpnnp  10990  ltaddpr  11019  indval  12221  dfnn2  12246  dfnn3  12247  dfuzi  12687  uz11  12887  elfzonlteqm1  13770  fzoopth  13791  om2uzlti  13986  axdc4uz  14020  hashrabsn1  14410  hashbclem  14489  hashf1lem2  14493  hash2prb  14509  hash2prd  14512  hash3tpb  14532  wrdsymb0  14586  lsw0  14602  swrdwrdsymb  14700  rtrclreclem3  15097  prodeq1f  15960  prodeq1  15961  rpnnen2lem1  16270  rpnnen2lem2  16271  lcmfval  16679  lcmf0val  16680  ismre  17642  isacs  17707  initoid  18058  termoid  18059  initoeu2lem1  18071  clatl  18564  mreclatBAD  18619  issubmgm  18760  issubm  18861  dfgrp2e  19030  isnsg  19221  cycsubg  19279  resghm  19302  ghmeql  19309  gsmsymgreq  19502  f1otrspeq  19517  pmtrval  19521  pmtrdifellem4  19549  pmtrprfval  19557  gsumzsplit  19997  pgpfac1lem1  20146  pgpfac1lem5  20151  pgpfac1  20152  ablsimpnosubgd  20176  c0snmgmhm  20544  c0snmhm  20545  0ring01eq  20613  issubrg  20656  lmodfopnelem2  20998  islss  21033  lspsneq0  21111  lmhmeql  21154  lspdisjb  21228  lidl1el  21329  rngqiprngfulem2  21423  rngqipring1  21427  isprmidl  21434  lidldvgen  21471  islindf4  21957  mplcoe1  22157  mplcoe5  22160  selvfval  22239  m1detdiag  22723  mdetunilem9  22746  maducoeval2  22766  madugsum  22769  chpmat1dlem  22961  istopg  23021  toprntopon  23051  fiinbas  23078  topbas  23098  ppttop  23133  pptbas  23134  epttop  23135  elcls  23199  clsndisj  23201  iscldtop  23221  neiptopnei  23258  restbas  23284  restntr  23308  pnfnei  23346  mnfnei  23347  cnpimaex  23382  lmcvg  23388  iscnp4  23389  cncnpi  23404  cnconst2  23409  cnprest  23415  cnprest2  23416  cnpdis  23419  lmss  23424  lmff  23427  cnt0  23472  ist1-3  23475  cnhaus  23480  isreg2  23503  dishaus  23508  ordthauslem  23509  cmpsublem  23525  cmpsub  23526  cmpcld  23528  hauscmplem  23532  unconn  23555  conncompid  23557  conncompss  23559  1stcfb  23571  1stcrest  23579  2ndcctbss  23581  2ndcomap  23584  dis2ndc  23586  1stcelcls  23587  llyeq  23596  nllyeq  23597  restnlly  23608  islly2  23610  lly1stc  23622  dislly  23623  hauspwdom  23627  finlocfin  23646  unisngl  23653  dissnlocfin  23655  locfindis  23656  comppfsc  23658  llycmpkgen2  23676  txbas  23693  eltx  23694  ptpjopn  23738  ptclsg  23741  txcnp  23746  ptcnplem  23747  ptcnp  23748  txlly  23762  pthaus  23764  txtube  23766  txhaus  23773  txlm  23774  tx1stc  23776  txkgen  23778  xkohaus  23779  xkopt  23781  xkococnlem  23785  tgqtop  23838  kqfvima  23856  kqt0lem  23862  isr0  23863  regr1lem  23865  kqreglem1  23867  kqreglem2  23868  reghmph  23919  fbssfi  23963  isfil  23973  filuni  24011  isufil  24029  isufil2  24034  fixufil  24048  uffixfr  24049  uffixsn  24051  rnelfm  24079  flimopn  24101  flimrest  24109  flimcls  24111  txflf  24132  fclsopni  24141  fclsrest  24150  fclscf  24151  fcfnei  24161  alexsublem  24170  alexsubALTlem3  24175  alexsubALT  24177  tmdgsum2  24222  symgtgp  24232  subgntr  24233  opnsubg  24234  ghmcnp  24241  tgpt0  24245  qustgpopn  24246  tsmsi  24260  tsmssubm  24269  tsmssplit  24278  isust  24330  ustn0  24347  blssps  24550  blss  24551  blssexps  24552  blssex  24553  neibl  24627  blcld  24631  metss  24634  methaus  24646  met1stc  24647  met2ndci  24648  metrest  24650  prdsxmslem2  24655  metcnp3  24666  dscopn  24699  idnghm  24869  qdensere  24895  tgioo  24922  tgqioo  24926  zdis  24943  xrge0tsms  24961  cnheibor  25083  lmmbr  25386  bcthlem4  25455  ovolicc2lem5  25649  dyadmbllem  25727  i1fd  25809  itg11  25819  itg2gt0  25888  itgeq1f  25899  itgeq1fOLD  25900  itgeq1  25901  bddmulibl  25967  ellimc2  26005  limcnlp  26006  ellimc3  26007  limcflf  26009  limciun  26022  lhop1lem  26141  ig1pdvds  26306  plycpn  26419  aannenlem2  26459  efopn  26789  xrlimcnp  27099  wilthlem2  27199  wilthlem3  27200  nodenselem8  27821  noetasuplem4  27866  noetainflem4  27870  nocvxminlem  27913  lrrecfr  28102  addsprop  28135  bdayons  28435  addonbday  28438  dfn0s2  28491  tghilberti1  28872  colline  28885  lmif  29052  islmib  29054  prlngex  29154  incistruhgr  29370  upgr1eopALT  29408  uhgrvtxedgiedgb  29427  upgredg2vtx  29432  edglnl  29434  numedglnl  29435  uhgr2edg  29499  umgrvad2edg  29504  usgredg4  29508  usgredg2vtxeuALT  29513  uspgredg2vlem  29514  ushgredgedg  29520  nbgr1vtx  29649  nbusgredgeu0  29659  nbusgrf1o0  29660  nb3grprlem1  29671  nb3grprlem2  29672  uvtx01vtx  29688  nbupgruvtxres  29698  cplgr1vlem  29720  cplgr1v  29721  vtxd0nedgb  29779  vtxduhgr0nedg  29783  1loopgrvd2  29794  1egrvtxdg0  29802  uspgrloopvtxel  29807  vtxdginducedm1lem4  29833  wlk1walk  29929  wlkp1lem1  29962  pthdivtx  30017  0enwwlksnge1  30154  usgrwwlks2on  30248  umgrwwlks2on  30249  rusgr0edg  30266  eleclclwwlkn  30368  upgr4cycl4dv4e  30477  1conngr  30486  vdn0conngrumgrv2  30488  eupth2eucrct  30509  eupth2lem1  30510  frgrncvvdeqlem7  30597  frgrncvvdeqlem9  30599  frgrwopregasn  30608  frgrwopregbsn  30609  l2p  30772  lpni  30773  issh  31501  pjoc1  31727  h1dn0  31845  spansneleqi  31862  nonbooli  31944  pjch  31987  pjnel  32019  cdjreui  32725  rexunirn  32779  rabsnel  32787  nelun  32800  iinabrex  32855  opabdm  32897  opabrn  32898  fpwrelmapffslem  33018  fpwrelmap  33019  fz1nntr  33088  xrge0tsmsd  33334  nsgqusf1olem3  33668  elrspunidl  33680  constrmon  34079  reff  34174  tpr2rico  34247  lmxrge0  34287  issiga  34447  isrnsiga  34448  isldsys  34491  isros  34503  issros  34510  ddeval1  34569  ddeval0  34570  ismbfm  34586  dya2icoseg  34612  dya2iocnrect  34616  ballotlem7  34871  bnj216  35066  bnj563  35077  bnj956  35110  bnj545  35228  bnj548  35230  bnj570  35238  bnj900  35262  bnj929  35269  bnj964  35276  bnj983  35284  bnj1001  35292  bnj1145  35326  bnj1398  35367  bnj1498  35394  fineqvnttrclselem2  35458  fineqvnttrclse  35460  fineqvinfep  35461  wevgblacfn  35494  erdszelem1  35582  kur14lem9  35605  cnllysconn  35636  cvmsss2  35665  cvmcov2  35666  cvmsiota  35668  cvmopnlem  35669  cvmliftlem15  35689  satfv1  35754  satfdmlem  35759  mclsssvlem  35953  mclsind  35961  untelirr  36099  untsucf  36101  elintfv  36156  dfon2lem4  36175  dfon2lem7  36178  dfon2lem9  36180  dfiota3  36312  funpartlem  36333  funpartfun  36334  linethru  36544  hilbert1.1  36545  rankelg  36559  elhf2  36566  neibastop2lem  36760  regsfromregtco  36938  regsfromunir1  36940  bj-zfauscl  37448  bj-cleq  37486  bj-snsetex  37487  bj-clel3gALT  37572  bj-nuliota  37581  bj-isrvec  37826  mptsnunlem  37872  isbasisrelowllem1  37889  isbasisrelowllem2  37890  relowlssretop  37897  relowlpssretop  37898  exrecfnlem  37913  finxpeq1  37920  finxpreclem5  37929  finxpreclem6  37930  nlpineqsn  37942  fvineqsneq  37946  pibt2  37951  unccur  38142  fin2so  38146  matunitlindflem1  38155  ptrecube  38159  poimirlem9  38168  poimirlem30  38189  poimir  38192  heicant  38194  mblfinlem1  38196  ftc1anc  38240  ftc2nc  38241  cover2  38254  isbnd2  38322  prdstotbnd  38333  heibor1lem  38348  grpokerinj  38432  rngoueqz  38479  isidl  38553  1idl  38565  0rngo  38566  ispridl  38573  smprngopr  38591  isfldidl  38607  isdmn3  38613  mpobi123f  38701  iineq12f  38703  mptbi12f  38705  dfsuccl4  39013  eqvrelqsel  39239  n0eldmqseq  39273  dmqseqim2  39281  suceldisj  39357  disjlem17  39441  lsateln0  39659  ispsubsp  40409  linepsubN  40416  elpcliN  40557  dvh3dim3N  42113  dochsnnz  42114  mapdindp3  42386  sn-iotalem  42882  prjspval  43227  elmzpcl  43349  diophren  43432  dford3lem2  43646  ttac  43655  pw2f1ocnv  43656  wepwsolem  43661  kelac1  43682  onexgt  43859  onexlimgt  43862  ordnexbtwnsuc  43886  oaordnr  43915  omnord1  43924  nnoeomeqom  43931  oenord1  43935  succlg  43947  oacl2g  43949  omabs2  43951  omcl2  43952  omcl3g  43953  naddwordnexlem4  44020  nlimsuc  44059  intabssd  44137  elmapintrab  44194  eliunov2  44297  gneispaceel2  44762  mnuop23d  44868  mnuunid  44879  mnurndlem1  44883  expgrowthi  44935  dvconstbi  44936  tratrb  45137  suctrALT2VD  45436  suctrALT2  45437  en3lplem1VD  45443  en3lpVD  45445  tratrbVD  45461  suctrALTcf  45522  suctrALTcfVD  45523  suctrALT3  45524  unisnALT  45526  0elaxnul  45584  pwclaxpow  45585  prclaxpr  45586  uniclaxun  45587  omssaxinf2  45589  wfaxrep  45595  restuni3  45728  supminfxr  46070  xlimxrre  46437  xlimmnfvlem1  46438  xlimpnfvlem1  46442  icccncfext  46493  stoweidlem27  46633  stoweidlem35  46641  stoweidlem46  46652  stoweidlem52  46658  ioorrnopnlem  46910  ioorrnopnxrlem  46912  issal  46920  intsaluni  46935  salgencntex  46949  smfresal  47394  tannpoly  47516  funressnfv  47669  fnbrafvb  47780  afvco2  47802  ndmaovg  47810  aovmpt4g  47827  fafv2elrnb  47861  fvelsetpreimafv  48025  elsetpreimafvbi  48029  sprsymrelf1lem  48129  paireqne  48149  fpprbasnn  48383  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  dfclnbgr6  48510  dfsclnbgr6  48512  grtri  48594  stgrvtx0  48616  stgrnbgr0  48618  isubgr3stgrlem3  48622  gpgvtx0  48707  gpgvtx1  48708  gpg3kgrtriex  48743  pgnbgreunbgrlem3  48772  pgnbgreunbgrlem6  48778  rngccatidALTV  48926  ringccatidALTV  48960  prmringnzring  48991  ldepspr  49138  mosn  49476  indthinc  50125  indthincALT  50126