Theorem eleq2 2827

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eleq12  2828  eleq2i  2830  nelneq2  2864  clelsb2  2867  dvelimdc  2933  raleqf  3323  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  reueq1  3335  rmoeq1  3336  raleleq  3347  rabeqf  3405  rabeqiOLD  3407  rabeq  3408  clel3g  3584  clel4g  3586  clel4OLD  3588  sbcbi2  3774  sbcel2gv  3784  csbeq2  3833  difeq2  4047  uneq1  4086  unineq  4208  nel02  4263  n0i  4264  sbnfc2  4367  disjel  4387  elif  4499  exsnrex  4613  elinsn  4643  sneqrg  4767  preq1b  4774  preq12b  4778  elpreqprb  4795  elunii  4841  elinti  4885  intss1  4891  intmin  4896  intab  4906  iuneqconst  4932  iineq2  4941  dfiin2g  4958  breq  5072  zfrepclf  5213  zfauscl  5220  sseliALT  5228  inuni  5262  sels  5351  elALT  5352  rext  5358  intid  5367  elopg  5375  opth1  5384  opthwiener  5422  xpeq1  5594  xpeq2  5601  0nelelxp  5615  opthprc  5642  ordtri1  6284  ordtri3  6287  nsuceq0  6331  suctr  6334  ordnbtwn  6341  funopg  6452  dffv2  6845  fveqdmss  6938  dffo4  6961  funopdmsn  7004  fnsnb  7020  elunirn  7106  f1oiso  7202  canth  7209  eusvobj2  7248  mpoeq123  7325  ndmovg  7433  uniuni  7590  iunpw  7599  oneqmin  7627  onuninsuci  7662  nlimsucg  7664  limomss  7692  nnlim  7701  peano5  7714  peano5OLD  7715  unielxp  7842  cnvf1o  7922  smoel  8162  smo11  8166  tz7.44-2  8209  oawordeulem  8347  oaordex  8351  omordi  8359  oneo  8374  oeordi  8380  oeoa  8390  oeoe  8392  nnmordi  8424  nnaordex  8431  omabs  8441  nnneo  8445  omsmolem  8447  elqsn0  8533  qsel  8543  mapsnd  8632  undifixp  8680  boxriin  8686  boxcutc  8687  pssnn  8913  fineqvlem  8966  fineqv  8967  pssnnOLD  8969  fissuni  9054  dffi2  9112  inficl  9114  dffi3  9120  wofib  9234  zfregcl  9283  en3lplem1  9300  en3lp  9302  suc11reg  9307  inf0  9309  inf3lem2  9317  inf3lem3  9318  infeq5i  9324  axinf2  9328  dfom3  9335  elom3  9336  cantnfle  9359  oemapvali  9372  cantnflem1  9377  tc2  9431  r1sdom  9463  rankwflemb  9482  rankval3b  9515  rankunb  9539  rankuni2b  9542  cardlim  9661  cardprclem  9668  infxpenlem  9700  alephnbtwn  9758  alephordi  9761  cardaleph  9776  alephfp  9795  alephval3  9797  dfac3  9808  dfac5lem2  9811  dfac5lem4  9813  dfac2b  9817  kmlem2  9838  coflim  9948  cfsmolem  9957  fin23lem30  10029  isf34lem4  10064  axdc2lem  10135  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  zorn2lem7  10189  axdclem  10206  brdom7disj  10218  brdom6disj  10219  axpowndlem3  10286  winainflem  10380  iswun  10391  eltskg  10437  inar1  10462  elgrug  10479  inaprc  10523  eltskm  10530  addnidpi  10588  indpi  10594  nqereu  10616  elnp  10674  elnpi  10675  genpnnp  10692  ltaddpr  10721  dfnn2  11916  dfnn3  11917  dfuzi  12341  uz11  12536  elfzonlteqm1  13391  om2uzlti  13598  axdc4uz  13632  hashrabsn1  14017  hashbclem  14092  hashf1lem2  14098  hash2prb  14114  hash2prd  14117  wrdsymb0  14180  lsw0  14196  swrdwrdsymb  14303  rtrclreclem3  14699  prodeq1f  15546  rpnnen2lem1  15851  rpnnen2lem2  15852  lcmfval  16254  lcmf0val  16255  ismre  17216  isacs  17277  initoid  17632  termoid  17633  initoeu2lem1  17645  clatl  18141  mreclatBAD  18196  issubm  18357  dfgrp2e  18520  isnsg  18698  cycsubg  18742  resghm  18765  ghmeql  18772  gsmsymgreq  18955  f1otrspeq  18970  pmtrval  18974  pmtrdifellem4  19002  pmtrprfval  19010  gsumzsplit  19443  pgpfac1lem1  19592  pgpfac1lem5  19597  pgpfac1  19598  ablsimpnosubgd  19622  issubrg  19939  lmodfopnelem2  20075  islss  20111  lspsneq0  20189  lmhmeql  20232  lspdisjb  20303  lidl1el  20402  lidldvgen  20439  0ring01eq  20455  islindf4  20955  mplcoe1  21148  mplcoe5  21151  selvfval  21237  m1detdiag  21654  mdetunilem9  21677  maducoeval2  21697  madugsum  21700  chpmat1dlem  21892  istopg  21952  toprntopon  21982  fiinbas  22010  topbas  22030  ppttop  22065  pptbas  22066  epttop  22067  elcls  22132  clsndisj  22134  iscldtop  22154  neiptopnei  22191  restbas  22217  restntr  22241  pnfnei  22279  mnfnei  22280  cnpimaex  22315  lmcvg  22321  iscnp4  22322  cncnpi  22337  cnconst2  22342  cnprest  22348  cnprest2  22349  cnpdis  22352  lmss  22357  lmff  22360  cnt0  22405  ist1-3  22408  cnhaus  22413  isreg2  22436  dishaus  22441  ordthauslem  22442  cmpsublem  22458  cmpsub  22459  cmpcld  22461  hauscmplem  22465  unconn  22488  conncompid  22490  conncompss  22492  1stcfb  22504  1stcrest  22512  2ndcctbss  22514  2ndcomap  22517  dis2ndc  22519  1stcelcls  22520  llyeq  22529  nllyeq  22530  restnlly  22541  islly2  22543  lly1stc  22555  dislly  22556  hauspwdom  22560  finlocfin  22579  unisngl  22586  dissnlocfin  22588  locfindis  22589  comppfsc  22591  llycmpkgen2  22609  txbas  22626  eltx  22627  ptpjopn  22671  ptclsg  22674  txcnp  22679  ptcnplem  22680  ptcnp  22681  txlly  22695  pthaus  22697  txtube  22699  txhaus  22706  txlm  22707  tx1stc  22709  txkgen  22711  xkohaus  22712  xkopt  22714  xkococnlem  22718  tgqtop  22771  kqfvima  22789  kqt0lem  22795  isr0  22796  regr1lem  22798  kqreglem1  22800  kqreglem2  22801  reghmph  22852  fbssfi  22896  isfil  22906  filuni  22944  isufil  22962  isufil2  22967  fixufil  22981  uffixfr  22982  uffixsn  22984  rnelfm  23012  flimopn  23034  flimrest  23042  flimcls  23044  txflf  23065  fclsopni  23074  fclsrest  23083  fclscf  23084  fcfnei  23094  alexsublem  23103  alexsubALTlem3  23108  alexsubALT  23110  tmdgsum2  23155  symgtgp  23165  subgntr  23166  opnsubg  23167  ghmcnp  23174  tgpt0  23178  qustgpopn  23179  tsmsi  23193  tsmssubm  23202  tsmssplit  23211  isust  23263  ustn0  23280  blssps  23485  blss  23486  blssexps  23487  blssex  23488  neibl  23563  blcld  23567  metss  23570  methaus  23582  met1stc  23583  met2ndci  23584  metrest  23586  prdsxmslem2  23591  metcnp3  23602  dscopn  23635  idnghm  23813  qdensere  23839  tgioo  23865  tgqioo  23869  zdis  23885  xrge0tsms  23903  cnheibor  24024  lmmbr  24327  bcthlem4  24396  ovolicc2lem5  24590  dyadmbllem  24668  i1fd  24750  itg11  24760  itg2gt0  24830  itgeq1f  24841  bddmulibl  24908  ellimc2  24946  limcnlp  24947  ellimc3  24948  limcflf  24950  limciun  24963  lhop1lem  25082  ig1pdvds  25246  plycpn  25354  aannenlem2  25394  efopn  25718  xrlimcnp  26023  wilthlem2  26123  wilthlem3  26124  tghilberti1  26902  colline  26914  lmif  27050  islmib  27052  incistruhgr  27352  upgr1eopALT  27390  uhgrvtxedgiedgb  27409  upgredg2vtx  27414  edglnl  27416  numedglnl  27417  uhgr2edg  27478  umgrvad2edg  27483  usgredg4  27487  usgredg2vtxeuALT  27492  uspgredg2vlem  27493  ushgredgedg  27499  nbgr1vtx  27628  nbusgredgeu0  27638  nbusgrf1o0  27639  nb3grprlem1  27650  nb3grprlem2  27651  uvtx01vtx  27667  nbupgruvtxres  27677  cplgr1vlem  27699  cplgr1v  27700  vtxd0nedgb  27758  vtxduhgr0nedg  27762  1loopgrvd2  27773  1egrvtxdg0  27781  uspgrloopvtxel  27786  vtxdginducedm1lem4  27812  wlk1walk  27908  wlkp1lem1  27943  pthdivtx  27998  0enwwlksnge1  28130  umgrwwlks2on  28223  rusgr0edg  28239  eleclclwwlkn  28341  upgr4cycl4dv4e  28450  1conngr  28459  vdn0conngrumgrv2  28461  eupth2eucrct  28482  eupth2lem1  28483  frgrncvvdeqlem7  28570  frgrncvvdeqlem9  28572  frgrwopregasn  28581  frgrwopregbsn  28582  l2p  28742  lpni  28743  issh  29471  pjoc1  29697  h1dn0  29815  spansneleqi  29832  nonbooli  29914  pjch  29957  pjnel  29989  cdjreui  30695  rexunirn  30741  rabsnel  30748  nelun  30760  iinabrex  30809  opabdm  30852  opabrn  30853  fpwrelmapffslem  30969  fpwrelmap  30970  fz1nntr  31027  xrge0tsmsd  31219  nsgqusf1olem3  31502  elrspunidl  31508  isprmidl  31515  reff  31691  tpr2rico  31764  lmxrge0  31804  indval  31881  issiga  31980  isrnsiga  31981  isldsys  32024  isros  32036  issros  32043  ddeval1  32102  ddeval0  32103  ismbfm  32119  isanmbfm  32123  dya2icoseg  32144  dya2iocnrect  32148  ballotlem7  32402  bnj216  32611  bnj563  32623  bnj956  32656  bnj545  32775  bnj548  32777  bnj570  32785  bnj900  32809  bnj929  32816  bnj964  32823  bnj983  32831  bnj1001  32839  bnj1145  32873  bnj1398  32914  bnj1498  32941  erdszelem1  33053  kur14lem9  33076  cnllysconn  33107  cvmsss2  33136  cvmcov2  33137  cvmsiota  33139  cvmopnlem  33140  cvmliftlem15  33160  satfv1  33225  satfdmlem  33230  mclsssvlem  33424  mclsind  33432  untelirr  33549  untsucf  33551  elintfv  33644  dfon2lem4  33668  dfon2lem7  33671  dfon2lem9  33673  soseq  33730  nodenselem8  33821  noetasuplem4  33866  noetainflem4  33870  nocvxminlem  33899  lrrecfr  34027  dfiota3  34152  funpartlem  34171  funpartfun  34172  linethru  34382  hilbert1.1  34383  rankelg  34397  elhf2  34404  neibastop2lem  34476  bj-rabeqd  35034  bj-zfauscl  35039  bj-cleq  35079  bj-snsetex  35080  bj-clel3gALT  35148  bj-nuliota  35155  bj-isrvec  35392  mptsnunlem  35436  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  relowlpssretop  35462  exrecfnlem  35477  finxpeq1  35484  finxpreclem5  35493  finxpreclem6  35494  nlpineqsn  35506  fvineqsneu  35509  fvineqsneq  35510  pibt2  35515  unccur  35687  fin2so  35691  matunitlindflem1  35700  ptrecube  35704  poimirlem9  35713  poimirlem30  35734  poimir  35737  heicant  35739  mblfinlem1  35741  ftc1anc  35785  ftc2nc  35786  cover2  35799  isbnd2  35868  prdstotbnd  35879  heibor1lem  35894  grpokerinj  35978  rngoueqz  36025  isidl  36099  1idl  36111  0rngo  36112  ispridl  36119  smprngopr  36137  isfldidl  36153  isdmn3  36159  mpobi123f  36247  iineq12f  36249  mptbi12f  36251  eqvrelqsel  36656  n0eldmqseq  36689  dmqseqim2  36696  lsateln0  36936  ispsubsp  37686  linepsubN  37693  elpcliN  37834  dvh3dim3N  39390  dochsnnz  39391  mapdindp3  39663  sn-iotalem  40117  prjspval  40363  elmzpcl  40464  diophren  40551  dford3lem2  40765  ttac  40774  pw2f1ocnv  40775  wepwsolem  40783  kelac1  40804  intabssd  41024  elmapintrab  41073  eliunov2  41176  gneispaceel2  41643  mnuop23d  41773  mnuunid  41784  mnurndlem1  41788  expgrowthi  41840  dvconstbi  41841  tratrb  42045  suctrALT2VD  42345  suctrALT2  42346  en3lplem1VD  42352  en3lpVD  42354  tratrbVD  42370  suctrALTcf  42431  suctrALTcfVD  42432  suctrALT3  42433  unisnALT  42435  restuni3  42556  supminfxr  42894  xlimxrre  43262  xlimmnfvlem1  43263  xlimpnfvlem1  43267  icccncfext  43318  stoweidlem27  43458  stoweidlem35  43466  stoweidlem46  43477  stoweidlem52  43483  ioorrnopnlem  43735  ioorrnopnxrlem  43737  issal  43745  intsaluni  43758  salgencntex  43772  sge0f1o  43810  smfresal  44209  funressnfv  44424  fnbrafvb  44533  afvco2  44555  ndmaovg  44563  aovmpt4g  44580  fafv2elrnb  44614  fzoopth  44707  fvelsetpreimafv  44727  elsetpreimafvbi  44731  sprsymrelf1lem  44831  paireqne  44851  fpprbasnn  45069  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  issubmgm  45231  c0snmgmhm  45360  c0snmhm  45361  rngccatidALTV  45435  ringccatidALTV  45498  ldepspr  45702  mosn  46046  indthinc  46221  indthincALT  46222