Theorem eleq2 2817

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eleq12  2818  eleq2i  2820  nelneq2  2853  dvelimdc  2916  raleqf  3326  rexeqfOLD  3328  rmoeq1OLD  3386  reueq1OLD  3387  rmoeq1f  3392  rabeq  3417  rabeqd  3431  rabeqf  3437  clel3g  3624  clel4g  3626  sbcbi2  3809  sbcel2gv  3817  csbeq2  3864  difeq2  4079  uneq1  4120  unineq  4247  nel02  4298  n0i  4299  sbnfc2  4398  disjel  4416  elif  4528  exsnrex  4640  elinsn  4670  sneqrg  4799  preq1b  4806  preq12b  4810  elpreqprb  4828  elunii  4872  elinti  4915  intss1  4923  intmin  4928  intab  4938  iuneqconst  4963  iineq2  4972  dfiun2g  4990  dfiin2g  4991  breq  5104  zfrepclf  5241  zfauscl  5248  sseliALT  5259  inuni  5300  selsALT  5394  rext  5403  intidg  5412  intidOLD  5413  elopg  5421  opth1  5430  opthwiener  5469  xpeq1  5645  xpeq2  5652  0nelelxp  5666  opthprc  5695  ordtri1  6353  ordtri3  6356  nsuceq0  6405  suctr  6408  ordnbtwn  6415  funopg  6534  dffv2  6938  fveqdmss  7032  dffo4  7057  funopdmsn  7104  fnsnbOLD  7122  elunirn  7207  f1oiso  7308  canth  7323  eusvobj2  7361  mpoeq123  7441  ndmovg  7552  uniuni  7718  iunpw  7727  oneqmin  7756  onuninsuci  7796  nlimsucg  7798  limomss  7827  nnlim  7836  peano5  7849  unielxp  7985  cnvf1o  8067  soseq  8115  smoel  8306  smo11  8310  tz7.44-2  8352  nlim2  8431  ord1eln01  8437  ord2eln012  8438  oawordeulem  8495  oaordex  8499  omordi  8507  oneo  8522  oeordi  8528  oeoa  8538  oeoe  8540  nnmordi  8572  nnaordex  8579  nnaordex2  8580  omabs  8592  nnneo  8596  omsmolem  8598  elqsn0  8734  qsel  8746  mapsnd  8836  undifixp  8884  boxriin  8890  boxcutc  8891  pssnn  9109  fineqvlem  9185  fineqv  9186  en1eqsn  9195  fissuni  9284  dffi2  9350  inficl  9352  dffi3  9358  wofib  9474  zfregcl  9523  en3lplem1  9541  en3lp  9543  suc11reg  9548  inf0  9550  inf3lem2  9558  inf3lem3  9559  infeq5i  9565  axinf2  9569  dfom3  9576  elom3  9577  cantnfle  9600  oemapvali  9613  cantnflem1  9618  tc2  9671  r1sdom  9703  rankwflemb  9722  rankval3b  9755  rankunb  9779  rankuni2b  9782  cardlim  9901  cardprclem  9908  infxpenlem  9942  alephnbtwn  10000  alephordi  10003  cardaleph  10018  alephfp  10037  alephval3  10039  dfac3  10050  dfac5lem2  10053  dfac5lem4  10055  dfac5lem4OLD  10057  dfac2b  10060  kmlem2  10081  coflim  10190  cfsmolem  10199  fin23lem30  10271  isf34lem4  10306  axdc2lem  10377  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  zorn2lem7  10431  axdclem  10448  brdom7disj  10460  brdom6disj  10461  axpowndlem3  10528  winainflem  10622  iswun  10633  eltskg  10679  inar1  10704  elgrug  10721  inaprc  10765  eltskm  10772  addnidpi  10830  indpi  10836  nqereu  10858  elnp  10916  elnpi  10917  genpnnp  10934  ltaddpr  10963  dfnn2  12175  dfnn3  12176  dfuzi  12601  uz11  12794  elfzonlteqm1  13678  fzoopth  13699  om2uzlti  13891  axdc4uz  13925  hashrabsn1  14315  hashbclem  14393  hashf1lem2  14397  hash2prb  14413  hash2prd  14416  hash3tpb  14436  wrdsymb0  14490  lsw0  14506  swrdwrdsymb  14603  rtrclreclem3  15002  prodeq1f  15848  prodeq1  15849  rpnnen2lem1  16158  rpnnen2lem2  16159  lcmfval  16567  lcmf0val  16568  ismre  17527  isacs  17592  initoid  17943  termoid  17944  initoeu2lem1  17956  clatl  18449  mreclatBAD  18504  issubmgm  18611  issubm  18712  dfgrp2e  18877  isnsg  19069  cycsubg  19122  resghm  19146  ghmeql  19153  gsmsymgreq  19346  f1otrspeq  19361  pmtrval  19365  pmtrdifellem4  19393  pmtrprfval  19401  gsumzsplit  19841  pgpfac1lem1  19990  pgpfac1lem5  19995  pgpfac1  19996  ablsimpnosubgd  20020  c0snmgmhm  20382  c0snmhm  20383  0ring01eq  20449  issubrg  20491  lmodfopnelem2  20837  islss  20872  lspsneq0  20950  lmhmeql  20994  lspdisjb  21068  lidl1el  21168  rngqiprngfulem2  21254  rngqipring1  21258  lidldvgen  21276  islindf4  21780  mplcoe1  21977  mplcoe5  21980  selvfval  22054  m1detdiag  22517  mdetunilem9  22540  maducoeval2  22560  madugsum  22563  chpmat1dlem  22755  istopg  22815  toprntopon  22845  fiinbas  22872  topbas  22892  ppttop  22927  pptbas  22928  epttop  22929  elcls  22993  clsndisj  22995  iscldtop  23015  neiptopnei  23052  restbas  23078  restntr  23102  pnfnei  23140  mnfnei  23141  cnpimaex  23176  lmcvg  23182  iscnp4  23183  cncnpi  23198  cnconst2  23203  cnprest  23209  cnprest2  23210  cnpdis  23213  lmss  23218  lmff  23221  cnt0  23266  ist1-3  23269  cnhaus  23274  isreg2  23297  dishaus  23302  ordthauslem  23303  cmpsublem  23319  cmpsub  23320  cmpcld  23322  hauscmplem  23326  unconn  23349  conncompid  23351  conncompss  23353  1stcfb  23365  1stcrest  23373  2ndcctbss  23375  2ndcomap  23378  dis2ndc  23380  1stcelcls  23381  llyeq  23390  nllyeq  23391  restnlly  23402  islly2  23404  lly1stc  23416  dislly  23417  hauspwdom  23421  finlocfin  23440  unisngl  23447  dissnlocfin  23449  locfindis  23450  comppfsc  23452  llycmpkgen2  23470  txbas  23487  eltx  23488  ptpjopn  23532  ptclsg  23535  txcnp  23540  ptcnplem  23541  ptcnp  23542  txlly  23556  pthaus  23558  txtube  23560  txhaus  23567  txlm  23568  tx1stc  23570  txkgen  23572  xkohaus  23573  xkopt  23575  xkococnlem  23579  tgqtop  23632  kqfvima  23650  kqt0lem  23656  isr0  23657  regr1lem  23659  kqreglem1  23661  kqreglem2  23662  reghmph  23713  fbssfi  23757  isfil  23767  filuni  23805  isufil  23823  isufil2  23828  fixufil  23842  uffixfr  23843  uffixsn  23845  rnelfm  23873  flimopn  23895  flimrest  23903  flimcls  23905  txflf  23926  fclsopni  23935  fclsrest  23944  fclscf  23945  fcfnei  23955  alexsublem  23964  alexsubALTlem3  23969  alexsubALT  23971  tmdgsum2  24016  symgtgp  24026  subgntr  24027  opnsubg  24028  ghmcnp  24035  tgpt0  24039  qustgpopn  24040  tsmsi  24054  tsmssubm  24063  tsmssplit  24072  isust  24124  ustn0  24141  blssps  24345  blss  24346  blssexps  24347  blssex  24348  neibl  24422  blcld  24426  metss  24429  methaus  24441  met1stc  24442  met2ndci  24443  metrest  24445  prdsxmslem2  24450  metcnp3  24461  dscopn  24494  idnghm  24664  qdensere  24690  tgioo  24717  tgqioo  24721  zdis  24738  xrge0tsms  24756  cnheibor  24887  lmmbr  25191  bcthlem4  25260  ovolicc2lem5  25455  dyadmbllem  25533  i1fd  25615  itg11  25625  itg2gt0  25694  itgeq1f  25705  itgeq1fOLD  25706  itgeq1  25707  bddmulibl  25773  ellimc2  25811  limcnlp  25812  ellimc3  25813  limcflf  25815  limciun  25828  lhop1lem  25951  ig1pdvds  26118  plycpn  26230  aannenlem2  26270  efopn  26600  xrlimcnp  26911  wilthlem2  27012  wilthlem3  27013  nodenselem8  27636  noetasuplem4  27681  noetainflem4  27685  nocvxminlem  27723  lrrecfr  27890  addsprop  27923  bdayon  28213  dfn0s2  28264  tghilberti1  28617  colline  28629  lmif  28765  islmib  28767  incistruhgr  29059  upgr1eopALT  29097  uhgrvtxedgiedgb  29116  upgredg2vtx  29121  edglnl  29123  numedglnl  29124  uhgr2edg  29188  umgrvad2edg  29193  usgredg4  29197  usgredg2vtxeuALT  29202  uspgredg2vlem  29203  ushgredgedg  29209  nbgr1vtx  29338  nbusgredgeu0  29348  nbusgrf1o0  29349  nb3grprlem1  29360  nb3grprlem2  29361  uvtx01vtx  29377  nbupgruvtxres  29387  cplgr1vlem  29409  cplgr1v  29410  vtxd0nedgb  29469  vtxduhgr0nedg  29473  1loopgrvd2  29484  1egrvtxdg0  29492  uspgrloopvtxel  29497  vtxdginducedm1lem4  29523  wlk1walk  29619  wlkp1lem1  29652  pthdivtx  29707  0enwwlksnge1  29844  umgrwwlks2on  29937  rusgr0edg  29953  eleclclwwlkn  30055  upgr4cycl4dv4e  30164  1conngr  30173  vdn0conngrumgrv2  30175  eupth2eucrct  30196  eupth2lem1  30197  frgrncvvdeqlem7  30284  frgrncvvdeqlem9  30286  frgrwopregasn  30295  frgrwopregbsn  30296  l2p  30458  lpni  30459  issh  31187  pjoc1  31413  h1dn0  31531  spansneleqi  31548  nonbooli  31630  pjch  31673  pjnel  31705  cdjreui  32411  rexunirn  32471  rabsnel  32479  nelun  32492  iinabrex  32548  opabdm  32589  opabrn  32590  fpwrelmapffslem  32705  fpwrelmap  32706  fz1nntr  32777  indval  32826  xrge0tsmsd  33045  nsgqusf1olem3  33379  elrspunidl  33392  isprmidl  33402  constrmon  33727  reff  33822  tpr2rico  33895  lmxrge0  33935  issiga  34095  isrnsiga  34096  isldsys  34139  isros  34151  issros  34158  ddeval1  34217  ddeval0  34218  ismbfm  34234  dya2icoseg  34261  dya2iocnrect  34265  ballotlem7  34520  bnj216  34715  bnj563  34726  bnj956  34759  bnj545  34878  bnj548  34880  bnj570  34888  bnj900  34912  bnj929  34919  bnj964  34926  bnj983  34934  bnj1001  34942  bnj1145  34976  bnj1398  35017  bnj1498  35044  wevgblacfn  35089  erdszelem1  35171  kur14lem9  35194  cnllysconn  35225  cvmsss2  35254  cvmcov2  35255  cvmsiota  35257  cvmopnlem  35258  cvmliftlem15  35278  satfv1  35343  satfdmlem  35348  mclsssvlem  35542  mclsind  35550  untelirr  35688  untsucf  35690  elintfv  35745  dfon2lem4  35767  dfon2lem7  35770  dfon2lem9  35772  dfiota3  35904  funpartlem  35923  funpartfun  35924  linethru  36134  hilbert1.1  36135  rankelg  36149  elhf2  36156  neibastop2lem  36341  bj-zfauscl  36905  bj-cleq  36943  bj-snsetex  36944  bj-clel3gALT  37029  bj-nuliota  37038  bj-isrvec  37275  mptsnunlem  37319  isbasisrelowllem1  37336  isbasisrelowllem2  37337  relowlssretop  37344  relowlpssretop  37345  exrecfnlem  37360  finxpeq1  37367  finxpreclem5  37376  finxpreclem6  37377  nlpineqsn  37389  fvineqsneq  37393  pibt2  37398  unccur  37590  fin2so  37594  matunitlindflem1  37603  ptrecube  37607  poimirlem9  37616  poimirlem30  37637  poimir  37640  heicant  37642  mblfinlem1  37644  ftc1anc  37688  ftc2nc  37689  cover2  37702  isbnd2  37770  prdstotbnd  37781  heibor1lem  37796  grpokerinj  37880  rngoueqz  37927  isidl  38001  1idl  38013  0rngo  38014  ispridl  38021  smprngopr  38039  isfldidl  38055  isdmn3  38061  mpobi123f  38149  iineq12f  38151  mptbi12f  38153  eqvrelqsel  38600  n0eldmqseq  38634  dmqseqim2  38642  disjlem17  38784  lsateln0  38981  ispsubsp  39732  linepsubN  39739  elpcliN  39880  dvh3dim3N  41436  dochsnnz  41437  mapdindp3  41709  sn-iotalem  42202  prjspval  42584  elmzpcl  42707  diophren  42794  dford3lem2  43009  ttac  43018  pw2f1ocnv  43019  wepwsolem  43024  kelac1  43045  onexgt  43222  onexlimgt  43225  ordnexbtwnsuc  43249  oaordnr  43278  omnord1  43287  nnoeomeqom  43294  oenord1  43298  succlg  43310  oacl2g  43312  omabs2  43314  omcl2  43315  omcl3g  43316  naddwordnexlem4  43383  nlimsuc  43423  intabssd  43501  elmapintrab  43558  eliunov2  43661  gneispaceel2  44126  mnuop23d  44248  mnuunid  44259  mnurndlem1  44263  expgrowthi  44315  dvconstbi  44316  tratrb  44519  suctrALT2VD  44818  suctrALT2  44819  en3lplem1VD  44825  en3lpVD  44827  tratrbVD  44843  suctrALTcf  44904  suctrALTcfVD  44905  suctrALT3  44906  unisnALT  44908  0elaxnul  44966  pwclaxpow  44967  prclaxpr  44968  uniclaxun  44969  omssaxinf2  44971  wfaxrep  44977  restuni3  45105  supminfxr  45453  xlimxrre  45822  xlimmnfvlem1  45823  xlimpnfvlem1  45827  icccncfext  45878  stoweidlem27  46018  stoweidlem35  46026  stoweidlem46  46037  stoweidlem52  46043  ioorrnopnlem  46295  ioorrnopnxrlem  46297  issal  46305  intsaluni  46320  salgencntex  46334  smfresal  46779  tannpoly  46884  funressnfv  47037  fnbrafvb  47148  afvco2  47170  ndmaovg  47178  aovmpt4g  47195  fafv2elrnb  47229  fvelsetpreimafv  47381  elsetpreimafvbi  47385  sprsymrelf1lem  47485  paireqne  47505  fpprbasnn  47723  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  dfclnbgr6  47849  dfsclnbgr6  47851  grtri  47932  stgrvtx0  47954  stgrnbgr0  47956  isubgr3stgrlem3  47960  gpgvtx0  48037  gpgvtx1  48038  gpg3kgrtriex  48073  pgnbgreunbgrlem3  48101  pgnbgreunbgrlem6  48107  rngccatidALTV  48253  ringccatidALTV  48287  ldepspr  48455  mosn  48794  indthinc  49444  indthincALT  49445