Theorem eleq2 2821

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  eleq12  2822  eleq2i  2824  nelneq2  2857  clelsb2OLD  2861  dvelimdc  2929  raleleqOLD  3339  raleqf  3348  rexeqfOLD  3350  rmoeq1OLD  3415  reueq1OLD  3416  rmoeq1f  3419  rabeq  3445  rabeqd  3459  rabeqf  3465  rabeqiOLD  3470  clel3g  3650  clel4g  3652  clel4OLD  3654  sbcbi2  3839  sbcel2gv  3849  csbeq2  3898  difeq2  4116  uneq1  4156  unineq  4277  nel02  4332  n0i  4333  sbnfc2  4436  disjel  4456  elif  4571  exsnrex  4684  elinsn  4714  sneqrg  4840  preq1b  4847  preq12b  4851  elpreqprb  4868  elunii  4913  elinti  4959  intss1  4967  intmin  4972  intab  4982  iuneqconst  5008  iineq2  5017  dfiun2g  5033  dfiin2g  5035  breq  5150  zfrepclf  5294  zfauscl  5301  sseliALT  5309  inuni  5343  selsALT  5439  rext  5448  intidg  5457  intidOLD  5458  elopg  5466  opth1  5475  opthwiener  5514  xpeq1  5690  xpeq2  5697  0nelelxp  5711  opthprc  5740  ordtri1  6397  ordtri3  6400  nsuceq0  6447  suctr  6450  ordnbtwn  6457  funopg  6582  dffv2  6986  fveqdmss  7080  dffo4  7104  funopdmsn  7150  fnsnb  7166  elunirn  7253  f1oiso  7351  canth  7365  eusvobj2  7404  mpoeq123  7484  ndmovg  7594  uniuni  7753  iunpw  7762  oneqmin  7792  onuninsuci  7833  nlimsucg  7835  limomss  7864  nnlim  7873  peano5  7888  peano5OLD  7889  unielxp  8017  cnvf1o  8102  soseq  8150  smoel  8366  smo11  8370  tz7.44-2  8413  nlim2  8496  ord1eln01  8502  ord2eln012  8503  oawordeulem  8560  oaordex  8564  omordi  8572  oneo  8587  oeordi  8593  oeoa  8603  oeoe  8605  nnmordi  8637  nnaordex  8644  omabs  8656  nnneo  8660  omsmolem  8662  elqsn0  8786  qsel  8796  mapsnd  8886  undifixp  8934  boxriin  8940  boxcutc  8941  pssnn  9174  fineqvlem  9268  fineqv  9269  pssnnOLD  9271  en1eqsn  9280  fissuni  9363  dffi2  9424  inficl  9426  dffi3  9432  wofib  9546  zfregcl  9595  en3lplem1  9613  en3lp  9615  suc11reg  9620  inf0  9622  inf3lem2  9630  inf3lem3  9631  infeq5i  9637  axinf2  9641  dfom3  9648  elom3  9649  cantnfle  9672  oemapvali  9685  cantnflem1  9690  tc2  9743  r1sdom  9775  rankwflemb  9794  rankval3b  9827  rankunb  9851  rankuni2b  9854  cardlim  9973  cardprclem  9980  infxpenlem  10014  alephnbtwn  10072  alephordi  10075  cardaleph  10090  alephfp  10109  alephval3  10111  dfac3  10122  dfac5lem2  10125  dfac5lem4  10127  dfac2b  10131  kmlem2  10152  coflim  10262  cfsmolem  10271  fin23lem30  10343  isf34lem4  10378  axdc2lem  10449  axdc3lem2  10452  axdc3lem4  10454  axdc4lem  10456  zorn2lem7  10503  axdclem  10520  brdom7disj  10532  brdom6disj  10533  axpowndlem3  10600  winainflem  10694  iswun  10705  eltskg  10751  inar1  10776  elgrug  10793  inaprc  10837  eltskm  10844  addnidpi  10902  indpi  10908  nqereu  10930  elnp  10988  elnpi  10989  genpnnp  11006  ltaddpr  11035  dfnn2  12232  dfnn3  12233  dfuzi  12660  uz11  12854  elfzonlteqm1  13715  om2uzlti  13922  axdc4uz  13956  hashrabsn1  14341  hashbclem  14418  hashf1lem2  14424  hash2prb  14440  hash2prd  14443  wrdsymb0  14506  lsw0  14522  swrdwrdsymb  14619  rtrclreclem3  15014  prodeq1f  15859  rpnnen2lem1  16164  rpnnen2lem2  16165  lcmfval  16565  lcmf0val  16566  ismre  17541  isacs  17602  initoid  17961  termoid  17962  initoeu2lem1  17974  clatl  18471  mreclatBAD  18526  issubmgm  18633  issubm  18726  dfgrp2e  18891  isnsg  19078  cycsubg  19130  resghm  19153  ghmeql  19160  gsmsymgreq  19348  f1otrspeq  19363  pmtrval  19367  pmtrdifellem4  19395  pmtrprfval  19403  gsumzsplit  19843  pgpfac1lem1  19992  pgpfac1lem5  19997  pgpfac1  19998  ablsimpnosubgd  20022  c0snmgmhm  20360  c0snmhm  20361  0ring01eq  20425  issubrg  20469  lmodfopnelem2  20741  islss  20777  lspsneq0  20855  lmhmeql  20899  lspdisjb  20973  lidl1el  21079  rngqiprngfulem2  21160  rngqipring1  21164  lidldvgen  21182  islindf4  21703  mplcoe1  21903  mplcoe5  21906  selvfval  21988  m1detdiag  22419  mdetunilem9  22442  maducoeval2  22462  madugsum  22465  chpmat1dlem  22657  istopg  22717  toprntopon  22747  fiinbas  22775  topbas  22795  ppttop  22830  pptbas  22831  epttop  22832  elcls  22897  clsndisj  22899  iscldtop  22919  neiptopnei  22956  restbas  22982  restntr  23006  pnfnei  23044  mnfnei  23045  cnpimaex  23080  lmcvg  23086  iscnp4  23087  cncnpi  23102  cnconst2  23107  cnprest  23113  cnprest2  23114  cnpdis  23117  lmss  23122  lmff  23125  cnt0  23170  ist1-3  23173  cnhaus  23178  isreg2  23201  dishaus  23206  ordthauslem  23207  cmpsublem  23223  cmpsub  23224  cmpcld  23226  hauscmplem  23230  unconn  23253  conncompid  23255  conncompss  23257  1stcfb  23269  1stcrest  23277  2ndcctbss  23279  2ndcomap  23282  dis2ndc  23284  1stcelcls  23285  llyeq  23294  nllyeq  23295  restnlly  23306  islly2  23308  lly1stc  23320  dislly  23321  hauspwdom  23325  finlocfin  23344  unisngl  23351  dissnlocfin  23353  locfindis  23354  comppfsc  23356  llycmpkgen2  23374  txbas  23391  eltx  23392  ptpjopn  23436  ptclsg  23439  txcnp  23444  ptcnplem  23445  ptcnp  23446  txlly  23460  pthaus  23462  txtube  23464  txhaus  23471  txlm  23472  tx1stc  23474  txkgen  23476  xkohaus  23477  xkopt  23479  xkococnlem  23483  tgqtop  23536  kqfvima  23554  kqt0lem  23560  isr0  23561  regr1lem  23563  kqreglem1  23565  kqreglem2  23566  reghmph  23617  fbssfi  23661  isfil  23671  filuni  23709  isufil  23727  isufil2  23732  fixufil  23746  uffixfr  23747  uffixsn  23749  rnelfm  23777  flimopn  23799  flimrest  23807  flimcls  23809  txflf  23830  fclsopni  23839  fclsrest  23848  fclscf  23849  fcfnei  23859  alexsublem  23868  alexsubALTlem3  23873  alexsubALT  23875  tmdgsum2  23920  symgtgp  23930  subgntr  23931  opnsubg  23932  ghmcnp  23939  tgpt0  23943  qustgpopn  23944  tsmsi  23958  tsmssubm  23967  tsmssplit  23976  isust  24028  ustn0  24045  blssps  24250  blss  24251  blssexps  24252  blssex  24253  neibl  24330  blcld  24334  metss  24337  methaus  24349  met1stc  24350  met2ndci  24351  metrest  24353  prdsxmslem2  24358  metcnp3  24369  dscopn  24402  idnghm  24580  qdensere  24606  tgioo  24632  tgqioo  24636  zdis  24652  xrge0tsms  24670  cnheibor  24801  lmmbr  25106  bcthlem4  25175  ovolicc2lem5  25370  dyadmbllem  25448  i1fd  25530  itg11  25540  itg2gt0  25610  itgeq1f  25621  bddmulibl  25688  ellimc2  25726  limcnlp  25727  ellimc3  25728  limcflf  25730  limciun  25743  lhop1lem  25866  ig1pdvds  26032  plycpn  26141  aannenlem2  26181  efopn  26506  xrlimcnp  26814  wilthlem2  26914  wilthlem3  26915  nodenselem8  27537  noetasuplem4  27582  noetainflem4  27586  nocvxminlem  27623  lrrecfr  27773  addsprop  27806  dfn0s2  28085  tghilberti1  28321  colline  28333  lmif  28469  islmib  28471  incistruhgr  28772  upgr1eopALT  28810  uhgrvtxedgiedgb  28829  upgredg2vtx  28834  edglnl  28836  numedglnl  28837  uhgr2edg  28898  umgrvad2edg  28903  usgredg4  28907  usgredg2vtxeuALT  28912  uspgredg2vlem  28913  ushgredgedg  28919  nbgr1vtx  29048  nbusgredgeu0  29058  nbusgrf1o0  29059  nb3grprlem1  29070  nb3grprlem2  29071  uvtx01vtx  29087  nbupgruvtxres  29097  cplgr1vlem  29119  cplgr1v  29120  vtxd0nedgb  29178  vtxduhgr0nedg  29182  1loopgrvd2  29193  1egrvtxdg0  29201  uspgrloopvtxel  29206  vtxdginducedm1lem4  29232  wlk1walk  29329  wlkp1lem1  29363  pthdivtx  29419  0enwwlksnge1  29551  umgrwwlks2on  29644  rusgr0edg  29660  eleclclwwlkn  29762  upgr4cycl4dv4e  29871  1conngr  29880  vdn0conngrumgrv2  29882  eupth2eucrct  29903  eupth2lem1  29904  frgrncvvdeqlem7  29991  frgrncvvdeqlem9  29993  frgrwopregasn  30002  frgrwopregbsn  30003  l2p  30165  lpni  30166  issh  30894  pjoc1  31120  h1dn0  31238  spansneleqi  31255  nonbooli  31337  pjch  31380  pjnel  31412  cdjreui  32118  rexunirn  32165  rabsnel  32173  nelun  32184  iinabrex  32233  opabdm  32273  opabrn  32274  fpwrelmapffslem  32390  fpwrelmap  32391  fz1nntr  32448  xrge0tsmsd  32645  nsgqusf1olem3  32966  elrspunidl  32986  isprmidl  32996  reff  33283  tpr2rico  33356  lmxrge0  33396  indval  33475  issiga  33574  isrnsiga  33575  isldsys  33618  isros  33630  issros  33637  ddeval1  33696  ddeval0  33697  ismbfm  33713  dya2icoseg  33740  dya2iocnrect  33744  ballotlem7  33998  bnj216  34207  bnj563  34218  bnj956  34251  bnj545  34370  bnj548  34372  bnj570  34380  bnj900  34404  bnj929  34411  bnj964  34418  bnj983  34426  bnj1001  34434  bnj1145  34468  bnj1398  34509  bnj1498  34536  erdszelem1  34646  kur14lem9  34669  cnllysconn  34700  cvmsss2  34729  cvmcov2  34730  cvmsiota  34732  cvmopnlem  34733  cvmliftlem15  34753  satfv1  34818  satfdmlem  34823  mclsssvlem  35017  mclsind  35025  untelirr  35147  untsucf  35149  elintfv  35206  dfon2lem4  35228  dfon2lem7  35231  dfon2lem9  35233  dfiota3  35365  funpartlem  35384  funpartfun  35385  linethru  35595  hilbert1.1  35596  rankelg  35610  elhf2  35617  neibastop2lem  35709  bj-zfauscl  36268  bj-cleq  36307  bj-snsetex  36308  bj-clel3gALT  36393  bj-nuliota  36402  bj-isrvec  36639  mptsnunlem  36683  isbasisrelowllem1  36700  isbasisrelowllem2  36701  relowlssretop  36708  relowlpssretop  36709  exrecfnlem  36724  finxpeq1  36731  finxpreclem5  36740  finxpreclem6  36741  nlpineqsn  36753  fvineqsneu  36756  fvineqsneq  36757  pibt2  36762  unccur  36935  fin2so  36939  matunitlindflem1  36948  ptrecube  36952  poimirlem9  36961  poimirlem30  36982  poimir  36985  heicant  36987  mblfinlem1  36989  ftc1anc  37033  ftc2nc  37034  cover2  37047  isbnd2  37115  prdstotbnd  37126  heibor1lem  37141  grpokerinj  37225  rngoueqz  37272  isidl  37346  1idl  37358  0rngo  37359  ispridl  37366  smprngopr  37384  isfldidl  37400  isdmn3  37406  mpobi123f  37494  iineq12f  37496  mptbi12f  37498  eqvrelqsel  37950  n0eldmqseq  37983  dmqseqim2  37991  disjlem17  38133  lsateln0  38329  ispsubsp  39080  linepsubN  39087  elpcliN  39228  dvh3dim3N  40784  dochsnnz  40785  mapdindp3  41057  sn-iotalem  41505  prjspval  41808  elmzpcl  41927  diophren  42014  dford3lem2  42229  ttac  42238  pw2f1ocnv  42239  wepwsolem  42247  kelac1  42268  onexgt  42452  onexlimgt  42455  ordnexbtwnsuc  42480  oaordnr  42509  omnord1  42518  nnoeomeqom  42525  oenord1  42529  succlg  42541  oacl2g  42543  omabs2  42545  omcl2  42546  omcl3g  42547  naddwordnexlem4  42615  nlimsuc  42655  intabssd  42733  elmapintrab  42790  eliunov2  42893  gneispaceel2  43358  mnuop23d  43488  mnuunid  43499  mnurndlem1  43503  expgrowthi  43555  dvconstbi  43556  tratrb  43760  suctrALT2VD  44060  suctrALT2  44061  en3lplem1VD  44067  en3lpVD  44069  tratrbVD  44085  suctrALTcf  44146  suctrALTcfVD  44147  suctrALT3  44148  unisnALT  44150  restuni3  44269  supminfxr  44633  xlimxrre  45006  xlimmnfvlem1  45007  xlimpnfvlem1  45011  icccncfext  45062  stoweidlem27  45202  stoweidlem35  45210  stoweidlem46  45221  stoweidlem52  45227  ioorrnopnlem  45479  ioorrnopnxrlem  45481  issal  45489  intsaluni  45504  salgencntex  45518  sge0f1o  45557  smfresal  45963  funressnfv  46212  fnbrafvb  46321  afvco2  46343  ndmaovg  46351  aovmpt4g  46368  fafv2elrnb  46402  fzoopth  46494  fvelsetpreimafv  46514  elsetpreimafvbi  46518  sprsymrelf1lem  46618  paireqne  46638  fpprbasnn  46856  nnsum4primeseven  46927  nnsum4primesevenALTV  46928  rngccatidALTV  47109  ringccatidALTV  47143  ldepspr  47316  mosn  47659  indthinc  47834  indthincALT  47835