Theorem eleq2 2825

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleq12  2826  eleq2i  2828  nelneq2  2861  dvelimdc  2923  raleqf  3325  rexeqfOLD  3327  rmoeq1OLD  3383  reueq1OLD  3384  rmoeq1f  3389  rabeq  3413  rabeqd  3427  rabeqf  3433  clel3g  3615  clel4g  3617  sbcbi2  3799  sbcel2gv  3807  csbeq2  3854  difeq2  4072  uneq1  4113  unineq  4240  nel02  4291  n0i  4292  sbnfc2  4391  disjel  4409  elif  4523  exsnrex  4637  elinsn  4667  sneqrg  4795  preq1b  4802  preq12b  4806  elpreqprb  4824  elunii  4868  elinti  4911  intss1  4918  intmin  4923  intab  4933  iuneqconst  4958  iineq2  4967  dfiun2g  4985  dfiin2g  4986  breq  5100  zfrepclf  5236  zfauscl  5243  sseliALT  5254  inuni  5295  selsALT  5389  rext  5396  intidg  5405  elopg  5414  opth1  5423  opthwiener  5462  xpeq1  5638  xpeq2  5645  0nelelxp  5659  opthprc  5688  ordtri1  6350  ordtri3  6353  nsuceq0  6402  suctr  6405  ordnbtwn  6412  funopg  6526  dffv2  6929  fveqdmss  7023  dffo4  7048  funopdmsn  7095  fnsnbOLD  7112  elunirn  7197  f1oiso  7297  canth  7312  eusvobj2  7350  mpoeq123  7430  ndmovg  7541  uniuni  7707  iunpw  7716  oneqmin  7745  onuninsuci  7782  nlimsucg  7784  limomss  7813  nnlim  7822  peano5  7835  unielxp  7971  cnvf1o  8053  soseq  8101  smoel  8292  smo11  8296  tz7.44-2  8338  nlim2  8417  ord1eln01  8423  ord2eln012  8424  oawordeulem  8481  oaordex  8485  omordi  8493  oneo  8508  oeordi  8515  oeoa  8525  oeoe  8527  nnmordi  8559  nnaordex  8566  nnaordex2  8567  omabs  8579  nnneo  8583  omsmolem  8585  elqsn0  8721  qsel  8733  mapsnd  8824  undifixp  8872  boxriin  8878  boxcutc  8879  pssnn  9093  fineqvlem  9166  fineqv  9167  en1eqsn  9175  fissuni  9257  dffi2  9326  inficl  9328  dffi3  9334  wofib  9450  zfregcl  9499  zfregclOLD  9500  nelaneq  9506  en3lplem1  9521  en3lp  9523  suc11reg  9528  inf0  9530  inf3lem2  9538  inf3lem3  9539  infeq5i  9545  axinf2  9549  dfom3  9556  elom3  9557  cantnfle  9580  oemapvali  9593  cantnflem1  9598  tc2  9649  r1sdom  9686  rankwflemb  9705  rankval3b  9738  rankunb  9762  rankuni2b  9765  cardlim  9884  cardprclem  9891  infxpenlem  9923  alephnbtwn  9981  alephordi  9984  cardaleph  9999  alephfp  10018  alephval3  10020  dfac3  10031  dfac5lem2  10034  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2b  10041  kmlem2  10062  coflim  10171  cfsmolem  10180  fin23lem30  10252  isf34lem4  10287  axdc2lem  10358  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  zorn2lem7  10412  axdclem  10429  brdom7disj  10441  brdom6disj  10442  axpowndlem3  10510  winainflem  10604  iswun  10615  eltskg  10661  inar1  10686  elgrug  10703  inaprc  10747  eltskm  10754  addnidpi  10812  indpi  10818  nqereu  10840  elnp  10898  elnpi  10899  genpnnp  10916  ltaddpr  10945  dfnn2  12158  dfnn3  12159  dfuzi  12583  uz11  12776  elfzonlteqm1  13657  fzoopth  13678  om2uzlti  13873  axdc4uz  13907  hashrabsn1  14297  hashbclem  14375  hashf1lem2  14379  hash2prb  14395  hash2prd  14398  hash3tpb  14418  wrdsymb0  14472  lsw0  14488  swrdwrdsymb  14586  rtrclreclem3  14983  prodeq1f  15829  prodeq1  15830  rpnnen2lem1  16139  rpnnen2lem2  16140  lcmfval  16548  lcmf0val  16549  ismre  17509  isacs  17574  initoid  17925  termoid  17926  initoeu2lem1  17938  clatl  18431  mreclatBAD  18486  issubmgm  18627  issubm  18728  dfgrp2e  18893  isnsg  19084  cycsubg  19137  resghm  19161  ghmeql  19168  gsmsymgreq  19361  f1otrspeq  19376  pmtrval  19380  pmtrdifellem4  19408  pmtrprfval  19416  gsumzsplit  19856  pgpfac1lem1  20005  pgpfac1lem5  20010  pgpfac1  20011  ablsimpnosubgd  20035  c0snmgmhm  20398  c0snmhm  20399  0ring01eq  20462  issubrg  20504  lmodfopnelem2  20850  islss  20885  lspsneq0  20963  lmhmeql  21007  lspdisjb  21081  lidl1el  21181  rngqiprngfulem2  21267  rngqipring1  21271  lidldvgen  21289  islindf4  21793  mplcoe1  21992  mplcoe5  21995  selvfval  22077  m1detdiag  22541  mdetunilem9  22564  maducoeval2  22584  madugsum  22587  chpmat1dlem  22779  istopg  22839  toprntopon  22869  fiinbas  22896  topbas  22916  ppttop  22951  pptbas  22952  epttop  22953  elcls  23017  clsndisj  23019  iscldtop  23039  neiptopnei  23076  restbas  23102  restntr  23126  pnfnei  23164  mnfnei  23165  cnpimaex  23200  lmcvg  23206  iscnp4  23207  cncnpi  23222  cnconst2  23227  cnprest  23233  cnprest2  23234  cnpdis  23237  lmss  23242  lmff  23245  cnt0  23290  ist1-3  23293  cnhaus  23298  isreg2  23321  dishaus  23326  ordthauslem  23327  cmpsublem  23343  cmpsub  23344  cmpcld  23346  hauscmplem  23350  unconn  23373  conncompid  23375  conncompss  23377  1stcfb  23389  1stcrest  23397  2ndcctbss  23399  2ndcomap  23402  dis2ndc  23404  1stcelcls  23405  llyeq  23414  nllyeq  23415  restnlly  23426  islly2  23428  lly1stc  23440  dislly  23441  hauspwdom  23445  finlocfin  23464  unisngl  23471  dissnlocfin  23473  locfindis  23474  comppfsc  23476  llycmpkgen2  23494  txbas  23511  eltx  23512  ptpjopn  23556  ptclsg  23559  txcnp  23564  ptcnplem  23565  ptcnp  23566  txlly  23580  pthaus  23582  txtube  23584  txhaus  23591  txlm  23592  tx1stc  23594  txkgen  23596  xkohaus  23597  xkopt  23599  xkococnlem  23603  tgqtop  23656  kqfvima  23674  kqt0lem  23680  isr0  23681  regr1lem  23683  kqreglem1  23685  kqreglem2  23686  reghmph  23737  fbssfi  23781  isfil  23791  filuni  23829  isufil  23847  isufil2  23852  fixufil  23866  uffixfr  23867  uffixsn  23869  rnelfm  23897  flimopn  23919  flimrest  23927  flimcls  23929  txflf  23950  fclsopni  23959  fclsrest  23968  fclscf  23969  fcfnei  23979  alexsublem  23988  alexsubALTlem3  23993  alexsubALT  23995  tmdgsum2  24040  symgtgp  24050  subgntr  24051  opnsubg  24052  ghmcnp  24059  tgpt0  24063  qustgpopn  24064  tsmsi  24078  tsmssubm  24087  tsmssplit  24096  isust  24148  ustn0  24165  blssps  24368  blss  24369  blssexps  24370  blssex  24371  neibl  24445  blcld  24449  metss  24452  methaus  24464  met1stc  24465  met2ndci  24466  metrest  24468  prdsxmslem2  24473  metcnp3  24484  dscopn  24517  idnghm  24687  qdensere  24713  tgioo  24740  tgqioo  24744  zdis  24761  xrge0tsms  24779  cnheibor  24910  lmmbr  25214  bcthlem4  25283  ovolicc2lem5  25478  dyadmbllem  25556  i1fd  25638  itg11  25648  itg2gt0  25717  itgeq1f  25728  itgeq1fOLD  25729  itgeq1  25730  bddmulibl  25796  ellimc2  25834  limcnlp  25835  ellimc3  25836  limcflf  25838  limciun  25851  lhop1lem  25974  ig1pdvds  26141  plycpn  26253  aannenlem2  26293  efopn  26623  xrlimcnp  26934  wilthlem2  27035  wilthlem3  27036  nodenselem8  27659  noetasuplem4  27704  noetainflem4  27708  nocvxminlem  27750  lrrecfr  27939  addsprop  27972  bdayons  28272  addonbday  28275  dfn0s2  28328  tghilberti1  28709  colline  28721  lmif  28857  islmib  28859  incistruhgr  29152  upgr1eopALT  29190  uhgrvtxedgiedgb  29209  upgredg2vtx  29214  edglnl  29216  numedglnl  29217  uhgr2edg  29281  umgrvad2edg  29286  usgredg4  29290  usgredg2vtxeuALT  29295  uspgredg2vlem  29296  ushgredgedg  29302  nbgr1vtx  29431  nbusgredgeu0  29441  nbusgrf1o0  29442  nb3grprlem1  29453  nb3grprlem2  29454  uvtx01vtx  29470  nbupgruvtxres  29480  cplgr1vlem  29502  cplgr1v  29503  vtxd0nedgb  29562  vtxduhgr0nedg  29566  1loopgrvd2  29577  1egrvtxdg0  29585  uspgrloopvtxel  29590  vtxdginducedm1lem4  29616  wlk1walk  29712  wlkp1lem1  29745  pthdivtx  29800  0enwwlksnge1  29937  usgrwwlks2on  30031  umgrwwlks2on  30032  rusgr0edg  30049  eleclclwwlkn  30151  upgr4cycl4dv4e  30260  1conngr  30269  vdn0conngrumgrv2  30271  eupth2eucrct  30292  eupth2lem1  30293  frgrncvvdeqlem7  30380  frgrncvvdeqlem9  30382  frgrwopregasn  30391  frgrwopregbsn  30392  l2p  30554  lpni  30555  issh  31283  pjoc1  31509  h1dn0  31627  spansneleqi  31644  nonbooli  31726  pjch  31769  pjnel  31801  cdjreui  32507  rexunirn  32566  rabsnel  32575  nelun  32588  iinabrex  32644  opabdm  32689  opabrn  32690  fpwrelmapffslem  32811  fpwrelmap  32812  fz1nntr  32882  indval  32932  xrge0tsmsd  33155  nsgqusf1olem3  33496  elrspunidl  33509  isprmidl  33519  constrmon  33901  reff  33996  tpr2rico  34069  lmxrge0  34109  issiga  34269  isrnsiga  34270  isldsys  34313  isros  34325  issros  34332  ddeval1  34391  ddeval0  34392  ismbfm  34408  dya2icoseg  34434  dya2iocnrect  34438  ballotlem7  34693  bnj216  34888  bnj563  34899  bnj956  34932  bnj545  35051  bnj548  35053  bnj570  35061  bnj900  35085  bnj929  35092  bnj964  35099  bnj983  35107  bnj1001  35115  bnj1145  35149  bnj1398  35190  bnj1498  35217  fineqvnttrclselem2  35278  fineqvnttrclse  35280  fineqvinfep  35281  wevgblacfn  35303  erdszelem1  35385  kur14lem9  35408  cnllysconn  35439  cvmsss2  35468  cvmcov2  35469  cvmsiota  35471  cvmopnlem  35472  cvmliftlem15  35492  satfv1  35557  satfdmlem  35562  mclsssvlem  35756  mclsind  35764  untelirr  35902  untsucf  35904  elintfv  35959  dfon2lem4  35978  dfon2lem7  35981  dfon2lem9  35983  dfiota3  36115  funpartlem  36136  funpartfun  36137  linethru  36347  hilbert1.1  36348  rankelg  36362  elhf2  36369  neibastop2lem  36554  exeltr  36665  regsfromregtr  36668  regsfromunir1  36670  bj-zfauscl  37125  bj-cleq  37163  bj-snsetex  37164  bj-clel3gALT  37249  bj-nuliota  37258  bj-isrvec  37499  mptsnunlem  37543  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlssretop  37568  relowlpssretop  37569  exrecfnlem  37584  finxpeq1  37591  finxpreclem5  37600  finxpreclem6  37601  nlpineqsn  37613  fvineqsneq  37617  pibt2  37622  unccur  37804  fin2so  37808  matunitlindflem1  37817  ptrecube  37821  poimirlem9  37830  poimirlem30  37851  poimir  37854  heicant  37856  mblfinlem1  37858  ftc1anc  37902  ftc2nc  37903  cover2  37916  isbnd2  37984  prdstotbnd  37995  heibor1lem  38010  grpokerinj  38094  rngoueqz  38141  isidl  38215  1idl  38227  0rngo  38228  ispridl  38235  smprngopr  38253  isfldidl  38269  isdmn3  38275  mpobi123f  38363  iineq12f  38365  mptbi12f  38367  dfsuccl4  38648  eqvrelqsel  38873  n0eldmqseq  38908  dmqseqim2  38916  disjlem17  39058  lsateln0  39255  ispsubsp  40005  linepsubN  40012  elpcliN  40153  dvh3dim3N  41709  dochsnnz  41710  mapdindp3  41982  sn-iotalem  42477  prjspval  42846  elmzpcl  42968  diophren  43055  dford3lem2  43269  ttac  43278  pw2f1ocnv  43279  wepwsolem  43284  kelac1  43305  onexgt  43482  onexlimgt  43485  ordnexbtwnsuc  43509  oaordnr  43538  omnord1  43547  nnoeomeqom  43554  oenord1  43558  succlg  43570  oacl2g  43572  omabs2  43574  omcl2  43575  omcl3g  43576  naddwordnexlem4  43643  nlimsuc  43682  intabssd  43760  elmapintrab  43817  eliunov2  43920  gneispaceel2  44385  mnuop23d  44507  mnuunid  44518  mnurndlem1  44522  expgrowthi  44574  dvconstbi  44575  tratrb  44777  suctrALT2VD  45076  suctrALT2  45077  en3lplem1VD  45083  en3lpVD  45085  tratrbVD  45101  suctrALTcf  45162  suctrALTcfVD  45163  suctrALT3  45164  unisnALT  45166  0elaxnul  45224  pwclaxpow  45225  prclaxpr  45226  uniclaxun  45227  omssaxinf2  45229  wfaxrep  45235  restuni3  45362  supminfxr  45708  xlimxrre  46075  xlimmnfvlem1  46076  xlimpnfvlem1  46080  icccncfext  46131  stoweidlem27  46271  stoweidlem35  46279  stoweidlem46  46290  stoweidlem52  46296  ioorrnopnlem  46548  ioorrnopnxrlem  46550  issal  46558  intsaluni  46573  salgencntex  46587  smfresal  47032  tannpoly  47136  funressnfv  47289  fnbrafvb  47400  afvco2  47422  ndmaovg  47430  aovmpt4g  47447  fafv2elrnb  47481  fvelsetpreimafv  47633  elsetpreimafvbi  47637  sprsymrelf1lem  47737  paireqne  47757  fpprbasnn  47975  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  dfclnbgr6  48102  dfsclnbgr6  48104  grtri  48186  stgrvtx0  48208  stgrnbgr0  48210  isubgr3stgrlem3  48214  gpgvtx0  48299  gpgvtx1  48300  gpg3kgrtriex  48335  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  rngccatidALTV  48518  ringccatidALTV  48552  ldepspr  48719  mosn  49058  indthinc  49707  indthincALT  49708