Theorem eleq2 2878

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eleq12  2879  eleq2i  2881  nelneq2  2915  dvelimdc  2979  raleqf  3350  rexeqf  3351  reueq1f  3352  rmoeq1f  3353  reueq1  3360  rmoeq1  3361  raleleq  3372  rabeqf  3428  rabeqiOLD  3430  rabeq  3431  clel3g  3602  clel4  3604  sbcbi2  3778  sbcel2gv  3787  csbeq2  3833  difeq2  4044  uneq1  4083  ineq1OLD  4132  unineq  4204  nel02  4248  n0i  4249  sbnfc2  4344  disjel  4364  elif  4467  exsnrex  4578  elinsn  4606  sneqrg  4730  preq1b  4737  preq12b  4741  elpreqprb  4758  elunii  4805  elinti  4847  intss1  4853  intmin  4858  intab  4868  iuneqconst  4892  iineq2  4901  dfiin2g  4919  breq  5032  zfrepclf  5162  zfauscl  5169  sseliALT  5177  inuni  5210  sels  5299  elALT  5300  rext  5306  intid  5315  elopg  5323  opth1  5332  opthwiener  5369  xpeq1  5533  xpeq2  5540  0nelelxp  5554  opthprc  5580  ordtri1  6192  ordtri3  6195  nsuceq0  6239  suctr  6242  ordnbtwn  6249  funopg  6358  dffv2  6733  fveqdmss  6823  dffo4  6846  funopdmsn  6889  fnsnb  6905  elunirn  6988  f1oiso  7083  canth  7090  eusvobj2  7128  mpoeq123  7205  ndmovg  7311  uniuni  7464  iunpw  7473  oneqmin  7500  onuninsuci  7535  nlimsucg  7537  limomss  7565  nnlim  7573  peano5  7585  unielxp  7709  cnvf1o  7789  smoel  7980  smo11  7984  tz7.44-2  8026  oawordeulem  8163  oaordex  8167  omordi  8175  oneo  8190  oeordi  8196  oeoa  8206  oeoe  8208  nnmordi  8240  nnaordex  8247  omabs  8257  nnneo  8261  omsmolem  8263  elqsn0  8349  qsel  8359  mapsnd  8433  undifixp  8481  boxriin  8487  boxcutc  8488  fineqvlem  8716  fineqv  8717  pssnn  8720  fissuni  8813  dffi2  8871  inficl  8873  dffi3  8879  wofib  8993  zfregcl  9042  en3lplem1  9059  en3lp  9061  suc11reg  9066  inf0  9068  inf3lem2  9076  inf3lem3  9077  infeq5i  9083  axinf2  9087  dfom3  9094  elom3  9095  cantnfle  9118  oemapvali  9131  cantnflem1  9136  tc2  9168  r1sdom  9187  rankwflemb  9206  rankval3b  9239  rankunb  9263  rankuni2b  9266  cardlim  9385  cardprclem  9392  infxpenlem  9424  alephnbtwn  9482  alephordi  9485  cardaleph  9500  alephfp  9519  alephval3  9521  dfac3  9532  dfac5lem2  9535  dfac5lem4  9537  dfac2b  9541  kmlem2  9562  coflim  9672  cfsmolem  9681  fin23lem30  9753  isf34lem4  9788  axdc2lem  9859  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  zorn2lem7  9913  axdclem  9930  brdom7disj  9942  brdom6disj  9943  axpowndlem3  10010  winainflem  10104  iswun  10115  eltskg  10161  inar1  10186  elgrug  10203  inaprc  10247  eltskm  10254  addnidpi  10312  indpi  10318  nqereu  10340  elnp  10398  elnpi  10399  genpnnp  10416  ltaddpr  10445  dfnn2  11638  dfnn3  11639  dfuzi  12061  uz11  12255  elfzonlteqm1  13108  om2uzlti  13313  axdc4uz  13347  hashrabsn1  13731  hashbclem  13806  hashf1lem2  13810  hash2prb  13826  hash2prd  13829  wrdsymb0  13892  lsw0  13908  swrdwrdsymb  14015  rtrclreclem3  14411  prodeq1f  15254  rpnnen2lem1  15559  rpnnen2lem2  15560  lcmfval  15955  lcmf0val  15956  ismre  16853  isacs  16914  initoid  17257  termoid  17258  initoeu2lem1  17266  clatl  17718  mreclatBAD  17789  issubm  17960  dfgrp2e  18121  isnsg  18299  cycsubg  18343  resghm  18366  ghmeql  18373  gsmsymgreq  18552  f1otrspeq  18567  pmtrval  18571  pmtrdifellem4  18599  pmtrprfval  18607  gsumzsplit  19040  pgpfac1lem1  19189  pgpfac1lem5  19194  pgpfac1  19195  ablsimpnosubgd  19219  issubrg  19528  lmodfopnelem2  19664  islss  19699  lspsneq0  19777  lmhmeql  19820  lspdisjb  19891  lidl1el  19984  lidldvgen  20021  0ring01eq  20037  islindf4  20527  mplcoe1  20705  mplcoe5  20708  selvfval  20789  m1detdiag  21202  mdetunilem9  21225  maducoeval2  21245  madugsum  21248  chpmat1dlem  21440  istopg  21500  toprntopon  21530  fiinbas  21557  topbas  21577  ppttop  21612  pptbas  21613  epttop  21614  elcls  21678  clsndisj  21680  iscldtop  21700  neiptopnei  21737  restbas  21763  restntr  21787  pnfnei  21825  mnfnei  21826  cnpimaex  21861  lmcvg  21867  iscnp4  21868  cncnpi  21883  cnconst2  21888  cnprest  21894  cnprest2  21895  cnpdis  21898  lmss  21903  lmff  21906  cnt0  21951  ist1-3  21954  cnhaus  21959  isreg2  21982  dishaus  21987  ordthauslem  21988  cmpsublem  22004  cmpsub  22005  cmpcld  22007  hauscmplem  22011  unconn  22034  conncompid  22036  conncompss  22038  1stcfb  22050  1stcrest  22058  2ndcctbss  22060  2ndcomap  22063  dis2ndc  22065  1stcelcls  22066  llyeq  22075  nllyeq  22076  restnlly  22087  islly2  22089  lly1stc  22101  dislly  22102  hauspwdom  22106  finlocfin  22125  unisngl  22132  dissnlocfin  22134  locfindis  22135  comppfsc  22137  llycmpkgen2  22155  txbas  22172  eltx  22173  ptpjopn  22217  ptclsg  22220  txcnp  22225  ptcnplem  22226  ptcnp  22227  txlly  22241  pthaus  22243  txtube  22245  txhaus  22252  txlm  22253  tx1stc  22255  txkgen  22257  xkohaus  22258  xkopt  22260  xkococnlem  22264  tgqtop  22317  kqfvima  22335  kqt0lem  22341  isr0  22342  regr1lem  22344  kqreglem1  22346  kqreglem2  22347  reghmph  22398  fbssfi  22442  isfil  22452  filuni  22490  isufil  22508  isufil2  22513  fixufil  22527  uffixfr  22528  uffixsn  22530  rnelfm  22558  flimopn  22580  flimrest  22588  flimcls  22590  txflf  22611  fclsopni  22620  fclsrest  22629  fclscf  22630  fcfnei  22640  alexsublem  22649  alexsubALTlem3  22654  alexsubALT  22656  tmdgsum2  22701  symgtgp  22711  subgntr  22712  opnsubg  22713  ghmcnp  22720  tgpt0  22724  qustgpopn  22725  tsmsi  22739  tsmssubm  22748  tsmssplit  22757  isust  22809  ustn0  22826  blssps  23031  blss  23032  blssexps  23033  blssex  23034  neibl  23108  blcld  23112  metss  23115  methaus  23127  met1stc  23128  met2ndci  23129  metrest  23131  prdsxmslem2  23136  metcnp3  23147  dscopn  23180  idnghm  23349  qdensere  23375  tgioo  23401  tgqioo  23405  zdis  23421  xrge0tsms  23439  cnheibor  23560  lmmbr  23862  bcthlem4  23931  ovolicc2lem5  24125  dyadmbllem  24203  i1fd  24285  itg11  24295  itg2gt0  24364  itgeq1f  24375  bddmulibl  24442  ellimc2  24480  limcnlp  24481  ellimc3  24482  limcflf  24484  limciun  24497  lhop1lem  24616  ig1pdvds  24777  plycpn  24885  aannenlem2  24925  efopn  25249  xrlimcnp  25554  wilthlem2  25654  wilthlem3  25655  tghilberti1  26431  colline  26443  lmif  26579  islmib  26581  incistruhgr  26872  upgr1eopALT  26910  uhgrvtxedgiedgb  26929  upgredg2vtx  26934  edglnl  26936  numedglnl  26937  uhgr2edg  26998  umgrvad2edg  27003  usgredg4  27007  usgredg2vtxeuALT  27012  uspgredg2vlem  27013  ushgredgedg  27019  nbgr1vtx  27148  nbusgredgeu0  27158  nbusgrf1o0  27159  nb3grprlem1  27170  nb3grprlem2  27171  uvtx01vtx  27187  nbupgruvtxres  27197  cplgr1vlem  27219  cplgr1v  27220  vtxd0nedgb  27278  vtxduhgr0nedg  27282  1loopgrvd2  27293  1egrvtxdg0  27301  uspgrloopvtxel  27306  vtxdginducedm1lem4  27332  wlk1walk  27428  wlkp1lem1  27463  pthdivtx  27518  0enwwlksnge1  27650  umgrwwlks2on  27743  rusgr0edg  27759  eleclclwwlkn  27861  upgr4cycl4dv4e  27970  1conngr  27979  vdn0conngrumgrv2  27981  eupth2eucrct  28002  eupth2lem1  28003  frgrncvvdeqlem7  28090  frgrncvvdeqlem9  28092  frgrwopregasn  28101  frgrwopregbsn  28102  l2p  28262  lpni  28263  issh  28991  pjoc1  29217  h1dn0  29335  spansneleqi  29352  nonbooli  29434  pjch  29477  pjnel  29509  cdjreui  30215  rexunirn  30263  rabsnel  30270  nelun  30282  iinabrex  30332  opabdm  30375  opabrn  30376  fpwrelmapffslem  30494  fpwrelmap  30495  fz1nntr  30553  xrge0tsmsd  30742  elrspunidl  31014  isprmidl  31021  reff  31192  tpr2rico  31265  lmxrge0  31305  indval  31382  issiga  31481  isrnsiga  31482  isldsys  31525  isros  31537  issros  31544  ddeval1  31603  ddeval0  31604  ismbfm  31620  isanmbfm  31624  dya2icoseg  31645  dya2iocnrect  31649  ballotlem7  31903  bnj216  32112  bnj563  32124  bnj956  32158  bnj545  32277  bnj548  32279  bnj570  32287  bnj900  32311  bnj929  32318  bnj964  32325  bnj983  32333  bnj1001  32341  bnj1145  32375  bnj1398  32416  bnj1498  32443  erdszelem1  32551  kur14lem9  32574  cnllysconn  32605  cvmsss2  32634  cvmcov2  32635  cvmsiota  32637  cvmopnlem  32638  cvmliftlem15  32658  satfv1  32723  satfdmlem  32728  mclsssvlem  32922  mclsind  32930  untelirr  33047  untsucf  33049  elintfv  33120  dfon2lem4  33144  dfon2lem7  33147  dfon2lem9  33149  soseq  33209  nodenselem8  33308  noetalem3  33332  nocvxminlem  33360  dfiota3  33497  funpartlem  33516  funpartfun  33517  linethru  33727  hilbert1.1  33728  rankelg  33742  elhf2  33749  neibastop2lem  33821  bj-rabeqd  34362  bj-zfauscl  34367  bj-cleq  34398  bj-snsetex  34399  bj-nuliota  34474  mptsnunlem  34755  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlssretop  34780  relowlpssretop  34781  exrecfnlem  34796  finxpeq1  34803  finxpreclem5  34812  finxpreclem6  34813  nlpineqsn  34825  fvineqsneu  34828  fvineqsneq  34829  pibt2  34834  unccur  35040  fin2so  35044  matunitlindflem1  35053  ptrecube  35057  poimirlem9  35066  poimirlem30  35087  poimir  35090  heicant  35092  mblfinlem1  35094  ftc1anc  35138  ftc2nc  35139  cover2  35152  isbnd2  35221  prdstotbnd  35232  heibor1lem  35247  grpokerinj  35331  rngoueqz  35378  isidl  35452  1idl  35464  0rngo  35465  ispridl  35472  smprngopr  35490  isfldidl  35506  isdmn3  35512  mpobi123f  35600  iineq12f  35602  mptbi12f  35604  eqvrelqsel  36011  n0eldmqseq  36044  dmqseqim2  36051  lsateln0  36291  ispsubsp  37041  linepsubN  37048  elpcliN  37189  dvh3dim3N  38745  dochsnnz  38746  mapdindp3  39018  prjspval  39597  elmzpcl  39667  diophren  39754  dford3lem2  39968  ttac  39977  pw2f1ocnv  39978  wepwsolem  39986  kelac1  40007  intabssd  40227  elmapintrab  40276  eliunov2  40380  gneispaceel2  40847  mnuop23d  40974  mnuunid  40985  mnurndlem1  40989  expgrowthi  41037  dvconstbi  41038  tratrb  41242  suctrALT2VD  41542  suctrALT2  41543  en3lplem1VD  41549  en3lpVD  41551  tratrbVD  41567  suctrALTcf  41628  suctrALTcfVD  41629  suctrALT3  41630  unisnALT  41632  restuni3  41753  supminfxr  42103  xlimxrre  42473  xlimmnfvlem1  42474  xlimpnfvlem1  42478  icccncfext  42529  stoweidlem27  42669  stoweidlem35  42677  stoweidlem46  42688  stoweidlem52  42694  ioorrnopnlem  42946  ioorrnopnxrlem  42948  issal  42956  intsaluni  42969  salgencntex  42983  sge0f1o  43021  smfresal  43420  funressnfv  43635  fnbrafvb  43710  afvco2  43732  ndmaovg  43740  aovmpt4g  43757  fafv2elrnb  43791  fzoopth  43884  fvelsetpreimafv  43904  elsetpreimafvbi  43908  sprsymrelf1lem  44008  paireqne  44028  fpprbasnn  44247  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  issubmgm  44409  c0snmgmhm  44538  c0snmhm  44539  rngccatidALTV  44613  ringccatidALTV  44676  ldepspr  44882