Theorem eleq2 2826

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleq12  2827  eleq2i  2829  nelneq2  2862  dvelimdc  2924  raleqf  3319  rmoeq1f  3380  rabeq  3404  rabeqd  3418  rabeqf  3424  clel3g  3604  clel4g  3606  sbcel2gv  3796  csbeq2  3843  difeq2  4061  uneq1  4102  unineq  4229  nel02  4280  sbnfc2  4380  disjel  4398  elif  4511  exsnrex  4625  elinsn  4655  sneqrg  4783  preq1b  4790  preq12b  4794  elpreqprb  4812  elunii  4856  elinti  4899  intss1  4906  intmin  4911  intab  4921  iuneqconst  4946  iineq2  4955  dfiun2g  4973  breq  5088  zfrepclf  5227  zfauscl  5234  sseliALT  5245  inuni  5288  selsALT  5389  rext  5396  intidg  5405  elopg  5415  opth1  5424  opthwiener  5463  xpeq1  5639  xpeq2  5646  0nelelxp  5660  opthprc  5689  ordtri1  6351  ordtri3  6354  nsuceq0  6403  suctr  6406  ordnbtwn  6413  funopg  6527  dffv2  6930  fveqdmss  7025  dffo4  7050  funopdmsn  7098  fnsnbOLD  7115  elunirn  7200  f1oiso  7300  canth  7315  eusvobj2  7353  mpoeq123  7433  ndmovg  7544  uniuni  7710  iunpw  7719  oneqmin  7748  onuninsuci  7785  nlimsucg  7787  limomss  7816  nnlim  7825  peano5  7838  unielxp  7974  cnvf1o  8055  soseq  8103  smoel  8294  smo11  8298  tz7.44-2  8340  nlim2  8419  ord1eln01  8425  ord2eln012  8426  oawordeulem  8483  oaordex  8487  omordi  8495  oneo  8510  oeordi  8517  oeoa  8527  oeoe  8529  nnmordi  8561  nnaordex  8568  nnaordex2  8569  omabs  8581  nnneo  8585  omsmolem  8587  elqsn0  8725  qsel  8737  mapsnd  8828  undifixp  8876  boxriin  8882  boxcutc  8883  pssnn  9097  fineqvlem  9170  fineqv  9171  en1eqsn  9179  fissuni  9261  dffi2  9330  inficl  9332  dffi3  9338  wofib  9454  zfregcl  9503  zfregclOLD  9504  nelaneq  9510  nelaneqOLD  9511  en3lplem1  9527  en3lp  9529  suc11reg  9534  inf0  9536  inf3lem2  9544  inf3lem3  9545  infeq5i  9551  axinf2  9555  dfom3  9562  elom3  9563  cantnfle  9586  oemapvali  9599  cantnflem1  9604  tc2  9655  r1sdom  9692  rankwflemb  9711  rankval3b  9744  rankunb  9768  rankuni2b  9771  cardlim  9890  cardprclem  9897  infxpenlem  9929  alephnbtwn  9987  alephordi  9990  cardaleph  10005  alephfp  10024  alephval3  10026  dfac3  10037  dfac5lem2  10040  dfac5lem4  10042  dfac5lem4OLD  10044  dfac2b  10047  kmlem2  10068  coflim  10177  cfsmolem  10186  fin23lem30  10258  isf34lem4  10293  axdc2lem  10364  axdc3lem2  10367  axdc3lem4  10369  axdc4lem  10371  zorn2lem7  10418  axdclem  10435  brdom7disj  10447  brdom6disj  10448  axpowndlem3  10516  winainflem  10610  iswun  10621  eltskg  10667  inar1  10692  elgrug  10709  inaprc  10753  eltskm  10760  addnidpi  10818  indpi  10824  nqereu  10846  elnp  10904  elnpi  10905  genpnnp  10922  ltaddpr  10951  indval  12156  dfnn2  12181  dfnn3  12182  dfuzi  12614  uz11  12807  elfzonlteqm1  13690  fzoopth  13711  om2uzlti  13906  axdc4uz  13940  hashrabsn1  14330  hashbclem  14408  hashf1lem2  14412  hash2prb  14428  hash2prd  14431  hash3tpb  14451  wrdsymb0  14505  lsw0  14521  swrdwrdsymb  14619  rtrclreclem3  15016  prodeq1f  15865  prodeq1  15866  rpnnen2lem1  16175  rpnnen2lem2  16176  lcmfval  16584  lcmf0val  16585  ismre  17546  isacs  17611  initoid  17962  termoid  17963  initoeu2lem1  17975  clatl  18468  mreclatBAD  18523  issubmgm  18664  issubm  18765  dfgrp2e  18933  isnsg  19124  cycsubg  19177  resghm  19201  ghmeql  19208  gsmsymgreq  19401  f1otrspeq  19416  pmtrval  19420  pmtrdifellem4  19448  pmtrprfval  19456  gsumzsplit  19896  pgpfac1lem1  20045  pgpfac1lem5  20050  pgpfac1  20051  ablsimpnosubgd  20075  c0snmgmhm  20436  c0snmhm  20437  0ring01eq  20500  issubrg  20542  lmodfopnelem2  20888  islss  20923  lspsneq0  21001  lmhmeql  21045  lspdisjb  21119  lidl1el  21219  rngqiprngfulem2  21305  rngqipring1  21309  lidldvgen  21327  islindf4  21831  mplcoe1  22028  mplcoe5  22031  selvfval  22113  m1detdiag  22575  mdetunilem9  22598  maducoeval2  22618  madugsum  22621  chpmat1dlem  22813  istopg  22873  toprntopon  22903  fiinbas  22930  topbas  22950  ppttop  22985  pptbas  22986  epttop  22987  elcls  23051  clsndisj  23053  iscldtop  23073  neiptopnei  23110  restbas  23136  restntr  23160  pnfnei  23198  mnfnei  23199  cnpimaex  23234  lmcvg  23240  iscnp4  23241  cncnpi  23256  cnconst2  23261  cnprest  23267  cnprest2  23268  cnpdis  23271  lmss  23276  lmff  23279  cnt0  23324  ist1-3  23327  cnhaus  23332  isreg2  23355  dishaus  23360  ordthauslem  23361  cmpsublem  23377  cmpsub  23378  cmpcld  23380  hauscmplem  23384  unconn  23407  conncompid  23409  conncompss  23411  1stcfb  23423  1stcrest  23431  2ndcctbss  23433  2ndcomap  23436  dis2ndc  23438  1stcelcls  23439  llyeq  23448  nllyeq  23449  restnlly  23460  islly2  23462  lly1stc  23474  dislly  23475  hauspwdom  23479  finlocfin  23498  unisngl  23505  dissnlocfin  23507  locfindis  23508  comppfsc  23510  llycmpkgen2  23528  txbas  23545  eltx  23546  ptpjopn  23590  ptclsg  23593  txcnp  23598  ptcnplem  23599  ptcnp  23600  txlly  23614  pthaus  23616  txtube  23618  txhaus  23625  txlm  23626  tx1stc  23628  txkgen  23630  xkohaus  23631  xkopt  23633  xkococnlem  23637  tgqtop  23690  kqfvima  23708  kqt0lem  23714  isr0  23715  regr1lem  23717  kqreglem1  23719  kqreglem2  23720  reghmph  23771  fbssfi  23815  isfil  23825  filuni  23863  isufil  23881  isufil2  23886  fixufil  23900  uffixfr  23901  uffixsn  23903  rnelfm  23931  flimopn  23953  flimrest  23961  flimcls  23963  txflf  23984  fclsopni  23993  fclsrest  24002  fclscf  24003  fcfnei  24013  alexsublem  24022  alexsubALTlem3  24027  alexsubALT  24029  tmdgsum2  24074  symgtgp  24084  subgntr  24085  opnsubg  24086  ghmcnp  24093  tgpt0  24097  qustgpopn  24098  tsmsi  24112  tsmssubm  24121  tsmssplit  24130  isust  24182  ustn0  24199  blssps  24402  blss  24403  blssexps  24404  blssex  24405  neibl  24479  blcld  24483  metss  24486  methaus  24498  met1stc  24499  met2ndci  24500  metrest  24502  prdsxmslem2  24507  metcnp3  24518  dscopn  24551  idnghm  24721  qdensere  24747  tgioo  24774  tgqioo  24778  zdis  24795  xrge0tsms  24813  cnheibor  24935  lmmbr  25238  bcthlem4  25307  ovolicc2lem5  25501  dyadmbllem  25579  i1fd  25661  itg11  25671  itg2gt0  25740  itgeq1f  25751  itgeq1fOLD  25752  itgeq1  25753  bddmulibl  25819  ellimc2  25857  limcnlp  25858  ellimc3  25859  limcflf  25861  limciun  25874  lhop1lem  25993  ig1pdvds  26158  plycpn  26269  aannenlem2  26309  efopn  26638  xrlimcnp  26948  wilthlem2  27049  wilthlem3  27050  nodenselem8  27672  noetasuplem4  27717  noetainflem4  27721  nocvxminlem  27763  lrrecfr  27952  addsprop  27985  bdayons  28285  addonbday  28288  dfn0s2  28341  tghilberti1  28722  colline  28734  lmif  28870  islmib  28872  incistruhgr  29165  upgr1eopALT  29203  uhgrvtxedgiedgb  29222  upgredg2vtx  29227  edglnl  29229  numedglnl  29230  uhgr2edg  29294  umgrvad2edg  29299  usgredg4  29303  usgredg2vtxeuALT  29308  uspgredg2vlem  29309  ushgredgedg  29315  nbgr1vtx  29444  nbusgredgeu0  29454  nbusgrf1o0  29455  nb3grprlem1  29466  nb3grprlem2  29467  uvtx01vtx  29483  nbupgruvtxres  29493  cplgr1vlem  29515  cplgr1v  29516  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  32657  opabdm  32702  opabrn  32703  fpwrelmapffslem  32823  fpwrelmap  32824  fz1nntr  32893  xrge0tsmsd  33152  nsgqusf1olem3  33493  elrspunidl  33506  isprmidl  33516  constrmon  33907  reff  34002  tpr2rico  34075  lmxrge0  34115  issiga  34275  isrnsiga  34276  isldsys  34319  isros  34331  issros  34338  ddeval1  34397  ddeval0  34398  ismbfm  34414  dya2icoseg  34440  dya2iocnrect  34444  ballotlem7  34699  bnj216  34894  bnj563  34905  bnj956  34938  bnj545  35056  bnj548  35058  bnj570  35066  bnj900  35090  bnj929  35097  bnj964  35104  bnj983  35112  bnj1001  35120  bnj1145  35154  bnj1398  35195  bnj1498  35222  fineqvnttrclselem2  35285  fineqvnttrclse  35287  fineqvinfep  35288  wevgblacfn  35310  erdszelem1  35392  kur14lem9  35415  cnllysconn  35446  cvmsss2  35475  cvmcov2  35476  cvmsiota  35478  cvmopnlem  35479  cvmliftlem15  35499  satfv1  35564  satfdmlem  35569  mclsssvlem  35763  mclsind  35771  untelirr  35909  untsucf  35911  elintfv  35966  dfon2lem4  35985  dfon2lem7  35988  dfon2lem9  35990  dfiota3  36122  funpartlem  36143  funpartfun  36144  linethru  36354  hilbert1.1  36355  rankelg  36369  elhf2  36376  neibastop2lem  36561  regsfromregtco  36739  regsfromunir1  36741  bj-zfauscl  37250  bj-cleq  37288  bj-snsetex  37289  bj-clel3gALT  37374  bj-nuliota  37383  bj-isrvec  37627  mptsnunlem  37671  isbasisrelowllem1  37688  isbasisrelowllem2  37689  relowlssretop  37696  relowlpssretop  37697  exrecfnlem  37712  finxpeq1  37719  finxpreclem5  37728  finxpreclem6  37729  nlpineqsn  37741  fvineqsneq  37745  pibt2  37750  unccur  37941  fin2so  37945  matunitlindflem1  37954  ptrecube  37958  poimirlem9  37967  poimirlem30  37988  poimir  37991  heicant  37993  mblfinlem1  37995  ftc1anc  38039  ftc2nc  38040  cover2  38053  isbnd2  38121  prdstotbnd  38132  heibor1lem  38147  grpokerinj  38231  rngoueqz  38278  isidl  38352  1idl  38364  0rngo  38365  ispridl  38372  smprngopr  38390  isfldidl  38406  isdmn3  38412  mpobi123f  38500  iineq12f  38502  mptbi12f  38504  dfsuccl4  38812  eqvrelqsel  39038  n0eldmqseq  39072  dmqseqim2  39080  suceldisj  39156  disjlem17  39240  lsateln0  39458  ispsubsp  40208  linepsubN  40215  elpcliN  40356  dvh3dim3N  41912  dochsnnz  41913  mapdindp3  42185  sn-iotalem  42679  prjspval  43053  elmzpcl  43175  diophren  43262  dford3lem2  43476  ttac  43485  pw2f1ocnv  43486  wepwsolem  43491  kelac1  43512  onexgt  43689  onexlimgt  43692  ordnexbtwnsuc  43716  oaordnr  43745  omnord1  43754  nnoeomeqom  43761  oenord1  43765  succlg  43777  oacl2g  43779  omabs2  43781  omcl2  43782  omcl3g  43783  naddwordnexlem4  43850  nlimsuc  43889  intabssd  43967  elmapintrab  44024  eliunov2  44127  gneispaceel2  44592  mnuop23d  44714  mnuunid  44725  mnurndlem1  44729  expgrowthi  44781  dvconstbi  44782  tratrb  44984  suctrALT2VD  45283  suctrALT2  45284  en3lplem1VD  45290  en3lpVD  45292  tratrbVD  45308  suctrALTcf  45369  suctrALTcfVD  45370  suctrALT3  45371  unisnALT  45373  0elaxnul  45431  pwclaxpow  45432  prclaxpr  45433  uniclaxun  45434  omssaxinf2  45436  wfaxrep  45442  restuni3  45569  supminfxr  45913  xlimxrre  46280  xlimmnfvlem1  46281  xlimpnfvlem1  46285  icccncfext  46336  stoweidlem27  46476  stoweidlem35  46484  stoweidlem46  46495  stoweidlem52  46501  ioorrnopnlem  46753  ioorrnopnxrlem  46755  issal  46763  intsaluni  46778  salgencntex  46792  smfresal  47237  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