Theorem eleq2 2833

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleq12  2834  eleq2i  2836  nelneq2  2869  clelsb2OLD  2873  dvelimdc  2936  raleqf  3361  rexeqfOLD  3363  rmoeq1OLD  3427  reueq1OLD  3428  rmoeq1f  3431  rabeq  3458  rabeqd  3473  rabeqf  3480  clel3g  3674  clel4g  3676  sbcbi2  3867  sbcel2gv  3876  csbeq2  3926  difeq2  4143  uneq1  4184  unineq  4307  nel02  4362  n0i  4363  sbnfc2  4462  disjel  4480  elif  4591  exsnrex  4704  elinsn  4735  sneqrg  4864  preq1b  4871  preq12b  4875  elpreqprb  4892  elunii  4936  elinti  4979  intss1  4987  intmin  4992  intab  5002  iuneqconst  5026  iineq2  5035  dfiun2g  5053  dfiin2g  5055  breq  5168  zfrepclf  5312  zfauscl  5319  sseliALT  5327  inuni  5368  selsALT  5459  rext  5468  intidg  5477  intidOLD  5478  elopg  5486  opth1  5495  opthwiener  5533  xpeq1  5714  xpeq2  5721  0nelelxp  5735  opthprc  5764  ordtri1  6428  ordtri3  6431  nsuceq0  6478  suctr  6481  ordnbtwn  6488  funopg  6612  dffv2  7017  fveqdmss  7112  dffo4  7137  funopdmsn  7184  fnsnb  7200  elunirn  7288  f1oiso  7387  canth  7401  eusvobj2  7440  mpoeq123  7522  ndmovg  7633  uniuni  7797  iunpw  7806  oneqmin  7836  onuninsuci  7877  nlimsucg  7879  limomss  7908  nnlim  7917  peano5  7932  peano5OLD  7933  unielxp  8068  cnvf1o  8152  soseq  8200  smoel  8416  smo11  8420  tz7.44-2  8463  nlim2  8546  ord1eln01  8552  ord2eln012  8553  oawordeulem  8610  oaordex  8614  omordi  8622  oneo  8637  oeordi  8643  oeoa  8653  oeoe  8655  nnmordi  8687  nnaordex  8694  nnaordex2  8695  omabs  8707  nnneo  8711  omsmolem  8713  elqsn0  8844  qsel  8854  mapsnd  8944  undifixp  8992  boxriin  8998  boxcutc  8999  pssnn  9234  fineqvlem  9325  fineqv  9326  en1eqsn  9336  fissuni  9427  dffi2  9492  inficl  9494  dffi3  9500  wofib  9614  zfregcl  9663  en3lplem1  9681  en3lp  9683  suc11reg  9688  inf0  9690  inf3lem2  9698  inf3lem3  9699  infeq5i  9705  axinf2  9709  dfom3  9716  elom3  9717  cantnfle  9740  oemapvali  9753  cantnflem1  9758  tc2  9811  r1sdom  9843  rankwflemb  9862  rankval3b  9895  rankunb  9919  rankuni2b  9922  cardlim  10041  cardprclem  10048  infxpenlem  10082  alephnbtwn  10140  alephordi  10143  cardaleph  10158  alephfp  10177  alephval3  10179  dfac3  10190  dfac5lem2  10193  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  kmlem2  10221  coflim  10330  cfsmolem  10339  fin23lem30  10411  isf34lem4  10446  axdc2lem  10517  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  zorn2lem7  10571  axdclem  10588  brdom7disj  10600  brdom6disj  10601  axpowndlem3  10668  winainflem  10762  iswun  10773  eltskg  10819  inar1  10844  elgrug  10861  inaprc  10905  eltskm  10912  addnidpi  10970  indpi  10976  nqereu  10998  elnp  11056  elnpi  11057  genpnnp  11074  ltaddpr  11103  dfnn2  12306  dfnn3  12307  dfuzi  12734  uz11  12928  elfzonlteqm1  13792  fzoopth  13812  om2uzlti  14001  axdc4uz  14035  hashrabsn1  14423  hashbclem  14501  hashf1lem2  14505  hash2prb  14521  hash2prd  14524  hash3tpb  14544  wrdsymb0  14597  lsw0  14613  swrdwrdsymb  14710  rtrclreclem3  15109  prodeq1f  15954  prodeq1  15955  rpnnen2lem1  16262  rpnnen2lem2  16263  lcmfval  16668  lcmf0val  16669  ismre  17648  isacs  17709  initoid  18068  termoid  18069  initoeu2lem1  18081  clatl  18578  mreclatBAD  18633  issubmgm  18740  issubm  18838  dfgrp2e  19003  isnsg  19195  cycsubg  19248  resghm  19272  ghmeql  19279  gsmsymgreq  19474  f1otrspeq  19489  pmtrval  19493  pmtrdifellem4  19521  pmtrprfval  19529  gsumzsplit  19969  pgpfac1lem1  20118  pgpfac1lem5  20123  pgpfac1  20124  ablsimpnosubgd  20148  c0snmgmhm  20488  c0snmhm  20489  0ring01eq  20555  issubrg  20599  lmodfopnelem2  20919  islss  20955  lspsneq0  21033  lmhmeql  21077  lspdisjb  21151  lidl1el  21259  rngqiprngfulem2  21345  rngqipring1  21349  lidldvgen  21367  islindf4  21881  mplcoe1  22078  mplcoe5  22081  selvfval  22161  m1detdiag  22624  mdetunilem9  22647  maducoeval2  22667  madugsum  22670  chpmat1dlem  22862  istopg  22922  toprntopon  22952  fiinbas  22980  topbas  23000  ppttop  23035  pptbas  23036  epttop  23037  elcls  23102  clsndisj  23104  iscldtop  23124  neiptopnei  23161  restbas  23187  restntr  23211  pnfnei  23249  mnfnei  23250  cnpimaex  23285  lmcvg  23291  iscnp4  23292  cncnpi  23307  cnconst2  23312  cnprest  23318  cnprest2  23319  cnpdis  23322  lmss  23327  lmff  23330  cnt0  23375  ist1-3  23378  cnhaus  23383  isreg2  23406  dishaus  23411  ordthauslem  23412  cmpsublem  23428  cmpsub  23429  cmpcld  23431  hauscmplem  23435  unconn  23458  conncompid  23460  conncompss  23462  1stcfb  23474  1stcrest  23482  2ndcctbss  23484  2ndcomap  23487  dis2ndc  23489  1stcelcls  23490  llyeq  23499  nllyeq  23500  restnlly  23511  islly2  23513  lly1stc  23525  dislly  23526  hauspwdom  23530  finlocfin  23549  unisngl  23556  dissnlocfin  23558  locfindis  23559  comppfsc  23561  llycmpkgen2  23579  txbas  23596  eltx  23597  ptpjopn  23641  ptclsg  23644  txcnp  23649  ptcnplem  23650  ptcnp  23651  txlly  23665  pthaus  23667  txtube  23669  txhaus  23676  txlm  23677  tx1stc  23679  txkgen  23681  xkohaus  23682  xkopt  23684  xkococnlem  23688  tgqtop  23741  kqfvima  23759  kqt0lem  23765  isr0  23766  regr1lem  23768  kqreglem1  23770  kqreglem2  23771  reghmph  23822  fbssfi  23866  isfil  23876  filuni  23914  isufil  23932  isufil2  23937  fixufil  23951  uffixfr  23952  uffixsn  23954  rnelfm  23982  flimopn  24004  flimrest  24012  flimcls  24014  txflf  24035  fclsopni  24044  fclsrest  24053  fclscf  24054  fcfnei  24064  alexsublem  24073  alexsubALTlem3  24078  alexsubALT  24080  tmdgsum2  24125  symgtgp  24135  subgntr  24136  opnsubg  24137  ghmcnp  24144  tgpt0  24148  qustgpopn  24149  tsmsi  24163  tsmssubm  24172  tsmssplit  24181  isust  24233  ustn0  24250  blssps  24455  blss  24456  blssexps  24457  blssex  24458  neibl  24535  blcld  24539  metss  24542  methaus  24554  met1stc  24555  met2ndci  24556  metrest  24558  prdsxmslem2  24563  metcnp3  24574  dscopn  24607  idnghm  24785  qdensere  24811  tgioo  24837  tgqioo  24841  zdis  24857  xrge0tsms  24875  cnheibor  25006  lmmbr  25311  bcthlem4  25380  ovolicc2lem5  25575  dyadmbllem  25653  i1fd  25735  itg11  25745  itg2gt0  25815  itgeq1f  25826  itgeq1fOLD  25827  itgeq1  25828  bddmulibl  25894  ellimc2  25932  limcnlp  25933  ellimc3  25934  limcflf  25936  limciun  25949  lhop1lem  26072  ig1pdvds  26239  plycpn  26349  aannenlem2  26389  efopn  26718  xrlimcnp  27029  wilthlem2  27130  wilthlem3  27131  nodenselem8  27754  noetasuplem4  27799  noetainflem4  27803  nocvxminlem  27840  lrrecfr  27994  addsprop  28027  dfn0s2  28354  tghilberti1  28663  colline  28675  lmif  28811  islmib  28813  incistruhgr  29114  upgr1eopALT  29152  uhgrvtxedgiedgb  29171  upgredg2vtx  29176  edglnl  29178  numedglnl  29179  uhgr2edg  29243  umgrvad2edg  29248  usgredg4  29252  usgredg2vtxeuALT  29257  uspgredg2vlem  29258  ushgredgedg  29264  nbgr1vtx  29393  nbusgredgeu0  29403  nbusgrf1o0  29404  nb3grprlem1  29415  nb3grprlem2  29416  uvtx01vtx  29432  nbupgruvtxres  29442  cplgr1vlem  29464  cplgr1v  29465  vtxd0nedgb  29524  vtxduhgr0nedg  29528  1loopgrvd2  29539  1egrvtxdg0  29547  uspgrloopvtxel  29552  vtxdginducedm1lem4  29578  wlk1walk  29675  wlkp1lem1  29709  pthdivtx  29765  0enwwlksnge1  29897  umgrwwlks2on  29990  rusgr0edg  30006  eleclclwwlkn  30108  upgr4cycl4dv4e  30217  1conngr  30226  vdn0conngrumgrv2  30228  eupth2eucrct  30249  eupth2lem1  30250  frgrncvvdeqlem7  30337  frgrncvvdeqlem9  30339  frgrwopregasn  30348  frgrwopregbsn  30349  l2p  30511  lpni  30512  issh  31240  pjoc1  31466  h1dn0  31584  spansneleqi  31601  nonbooli  31683  pjch  31726  pjnel  31758  cdjreui  32464  rexunirn  32520  rabsnel  32528  nelun  32542  iinabrex  32591  opabdm  32633  opabrn  32634  fpwrelmapffslem  32746  fpwrelmap  32747  fz1nntr  32809  xrge0tsmsd  33041  nsgqusf1olem3  33408  elrspunidl  33421  isprmidl  33431  constrmon  33734  reff  33785  tpr2rico  33858  lmxrge0  33898  indval  33977  issiga  34076  isrnsiga  34077  isldsys  34120  isros  34132  issros  34139  ddeval1  34198  ddeval0  34199  ismbfm  34215  dya2icoseg  34242  dya2iocnrect  34246  ballotlem7  34500  bnj216  34708  bnj563  34719  bnj956  34752  bnj545  34871  bnj548  34873  bnj570  34881  bnj900  34905  bnj929  34912  bnj964  34919  bnj983  34927  bnj1001  34935  bnj1145  34969  bnj1398  35010  bnj1498  35037  wevgblacfn  35076  erdszelem1  35159  kur14lem9  35182  cnllysconn  35213  cvmsss2  35242  cvmcov2  35243  cvmsiota  35245  cvmopnlem  35246  cvmliftlem15  35266  satfv1  35331  satfdmlem  35336  mclsssvlem  35530  mclsind  35538  untelirr  35670  untsucf  35672  elintfv  35728  dfon2lem4  35750  dfon2lem7  35753  dfon2lem9  35755  dfiota3  35887  funpartlem  35906  funpartfun  35907  linethru  36117  hilbert1.1  36118  rankelg  36132  elhf2  36139  neibastop2lem  36326  bj-zfauscl  36890  bj-cleq  36928  bj-snsetex  36929  bj-clel3gALT  37014  bj-nuliota  37023  bj-isrvec  37260  mptsnunlem  37304  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  relowlpssretop  37330  exrecfnlem  37345  finxpeq1  37352  finxpreclem5  37361  finxpreclem6  37362  nlpineqsn  37374  fvineqsneq  37378  pibt2  37383  unccur  37563  fin2so  37567  matunitlindflem1  37576  ptrecube  37580  poimirlem9  37589  poimirlem30  37610  poimir  37613  heicant  37615  mblfinlem1  37617  ftc1anc  37661  ftc2nc  37662  cover2  37675  isbnd2  37743  prdstotbnd  37754  heibor1lem  37769  grpokerinj  37853  rngoueqz  37900  isidl  37974  1idl  37986  0rngo  37987  ispridl  37994  smprngopr  38012  isfldidl  38028  isdmn3  38034  mpobi123f  38122  iineq12f  38124  mptbi12f  38126  eqvrelqsel  38572  n0eldmqseq  38605  dmqseqim2  38613  disjlem17  38755  lsateln0  38951  ispsubsp  39702  linepsubN  39709  elpcliN  39850  dvh3dim3N  41406  dochsnnz  41407  mapdindp3  41679  sn-iotalem  42214  prjspval  42558  elmzpcl  42682  diophren  42769  dford3lem2  42984  ttac  42993  pw2f1ocnv  42994  wepwsolem  42999  kelac1  43020  onexgt  43201  onexlimgt  43204  ordnexbtwnsuc  43229  oaordnr  43258  omnord1  43267  nnoeomeqom  43274  oenord1  43278  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  omcl3g  43296  naddwordnexlem4  43363  nlimsuc  43403  intabssd  43481  elmapintrab  43538  eliunov2  43641  gneispaceel2  44106  mnuop23d  44235  mnuunid  44246  mnurndlem1  44250  expgrowthi  44302  dvconstbi  44303  tratrb  44507  suctrALT2VD  44807  suctrALT2  44808  en3lplem1VD  44814  en3lpVD  44816  tratrbVD  44832  suctrALTcf  44893  suctrALTcfVD  44894  suctrALT3  44895  unisnALT  44897  restuni3  45020  supminfxr  45379  xlimxrre  45752  xlimmnfvlem1  45753  xlimpnfvlem1  45757  icccncfext  45808  stoweidlem27  45948  stoweidlem35  45956  stoweidlem46  45967  stoweidlem52  45973  ioorrnopnlem  46225  ioorrnopnxrlem  46227  issal  46235  intsaluni  46250  salgencntex  46264  sge0f1o  46303  smfresal  46709  funressnfv  46958  fnbrafvb  47069  afvco2  47091  ndmaovg  47099  aovmpt4g  47116  fafv2elrnb  47150  fvelsetpreimafv  47261  elsetpreimafvbi  47265  sprsymrelf1lem  47365  paireqne  47385  fpprbasnn  47603  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  dfclnbgr6  47728  dfsclnbgr6  47730  grtri  47791  rngccatidALTV  47995  ringccatidALTV  48029  ldepspr  48202  mosn  48544  indthinc  48719  indthincALT  48720