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  3318  rexeqfOLD  3320  rmoeq1OLD  3378  reueq1OLD  3379  rmoeq1f  3384  rabeq  3409  rabeqd  3423  rabeqf  3429  clel3g  3616  clel4g  3618  sbcbi2  3801  sbcel2gv  3809  csbeq2  3856  difeq2  4071  uneq1  4112  unineq  4239  nel02  4290  n0i  4291  sbnfc2  4390  disjel  4408  elif  4520  exsnrex  4632  elinsn  4662  sneqrg  4790  preq1b  4797  preq12b  4801  elpreqprb  4819  elunii  4863  elinti  4905  intss1  4913  intmin  4918  intab  4928  iuneqconst  4953  iineq2  4962  dfiun2g  4980  dfiin2g  4981  breq  5094  zfrepclf  5230  zfauscl  5237  sseliALT  5248  inuni  5289  selsALT  5383  rext  5391  intidg  5400  intidOLD  5401  elopg  5409  opth1  5418  opthwiener  5457  xpeq1  5633  xpeq2  5640  0nelelxp  5654  opthprc  5683  ordtri1  6340  ordtri3  6343  nsuceq0  6392  suctr  6395  ordnbtwn  6402  funopg  6516  dffv2  6918  fveqdmss  7012  dffo4  7037  funopdmsn  7084  fnsnbOLD  7102  elunirn  7187  f1oiso  7288  canth  7303  eusvobj2  7341  mpoeq123  7421  ndmovg  7532  uniuni  7698  iunpw  7707  oneqmin  7736  onuninsuci  7773  nlimsucg  7775  limomss  7804  nnlim  7813  peano5  7826  unielxp  7962  cnvf1o  8044  soseq  8092  smoel  8283  smo11  8287  tz7.44-2  8329  nlim2  8408  ord1eln01  8414  ord2eln012  8415  oawordeulem  8472  oaordex  8476  omordi  8484  oneo  8499  oeordi  8505  oeoa  8515  oeoe  8517  nnmordi  8549  nnaordex  8556  nnaordex2  8557  omabs  8569  nnneo  8573  omsmolem  8575  elqsn0  8711  qsel  8723  mapsnd  8813  undifixp  8861  boxriin  8867  boxcutc  8868  pssnn  9082  fineqvlem  9155  fineqv  9156  en1eqsn  9164  fissuni  9247  dffi2  9313  inficl  9315  dffi3  9321  wofib  9437  zfregcl  9486  zfregclOLD  9487  nelaneq  9493  en3lplem1  9508  en3lp  9510  suc11reg  9515  inf0  9517  inf3lem2  9525  inf3lem3  9526  infeq5i  9532  axinf2  9536  dfom3  9543  elom3  9544  cantnfle  9567  oemapvali  9580  cantnflem1  9585  tc2  9638  r1sdom  9670  rankwflemb  9689  rankval3b  9722  rankunb  9746  rankuni2b  9749  cardlim  9868  cardprclem  9875  infxpenlem  9907  alephnbtwn  9965  alephordi  9968  cardaleph  9983  alephfp  10002  alephval3  10004  dfac3  10015  dfac5lem2  10018  dfac5lem4  10020  dfac5lem4OLD  10022  dfac2b  10025  kmlem2  10046  coflim  10155  cfsmolem  10164  fin23lem30  10236  isf34lem4  10271  axdc2lem  10342  axdc3lem2  10345  axdc3lem4  10347  axdc4lem  10349  zorn2lem7  10396  axdclem  10413  brdom7disj  10425  brdom6disj  10426  axpowndlem3  10493  winainflem  10587  iswun  10598  eltskg  10644  inar1  10669  elgrug  10686  inaprc  10730  eltskm  10737  addnidpi  10795  indpi  10801  nqereu  10823  elnp  10881  elnpi  10882  genpnnp  10899  ltaddpr  10928  dfnn2  12141  dfnn3  12142  dfuzi  12567  uz11  12760  elfzonlteqm1  13644  fzoopth  13665  om2uzlti  13857  axdc4uz  13891  hashrabsn1  14281  hashbclem  14359  hashf1lem2  14363  hash2prb  14379  hash2prd  14382  hash3tpb  14402  wrdsymb0  14456  lsw0  14472  swrdwrdsymb  14569  rtrclreclem3  14967  prodeq1f  15813  prodeq1  15814  rpnnen2lem1  16123  rpnnen2lem2  16124  lcmfval  16532  lcmf0val  16533  ismre  17492  isacs  17557  initoid  17908  termoid  17909  initoeu2lem1  17921  clatl  18414  mreclatBAD  18469  issubmgm  18576  issubm  18677  dfgrp2e  18842  isnsg  19034  cycsubg  19087  resghm  19111  ghmeql  19118  gsmsymgreq  19311  f1otrspeq  19326  pmtrval  19330  pmtrdifellem4  19358  pmtrprfval  19366  gsumzsplit  19806  pgpfac1lem1  19955  pgpfac1lem5  19960  pgpfac1  19961  ablsimpnosubgd  19985  c0snmgmhm  20347  c0snmhm  20348  0ring01eq  20414  issubrg  20456  lmodfopnelem2  20802  islss  20837  lspsneq0  20915  lmhmeql  20959  lspdisjb  21033  lidl1el  21133  rngqiprngfulem2  21219  rngqipring1  21223  lidldvgen  21241  islindf4  21745  mplcoe1  21942  mplcoe5  21945  selvfval  22019  m1detdiag  22482  mdetunilem9  22505  maducoeval2  22525  madugsum  22528  chpmat1dlem  22720  istopg  22780  toprntopon  22810  fiinbas  22837  topbas  22857  ppttop  22892  pptbas  22893  epttop  22894  elcls  22958  clsndisj  22960  iscldtop  22980  neiptopnei  23017  restbas  23043  restntr  23067  pnfnei  23105  mnfnei  23106  cnpimaex  23141  lmcvg  23147  iscnp4  23148  cncnpi  23163  cnconst2  23168  cnprest  23174  cnprest2  23175  cnpdis  23178  lmss  23183  lmff  23186  cnt0  23231  ist1-3  23234  cnhaus  23239  isreg2  23262  dishaus  23267  ordthauslem  23268  cmpsublem  23284  cmpsub  23285  cmpcld  23287  hauscmplem  23291  unconn  23314  conncompid  23316  conncompss  23318  1stcfb  23330  1stcrest  23338  2ndcctbss  23340  2ndcomap  23343  dis2ndc  23345  1stcelcls  23346  llyeq  23355  nllyeq  23356  restnlly  23367  islly2  23369  lly1stc  23381  dislly  23382  hauspwdom  23386  finlocfin  23405  unisngl  23412  dissnlocfin  23414  locfindis  23415  comppfsc  23417  llycmpkgen2  23435  txbas  23452  eltx  23453  ptpjopn  23497  ptclsg  23500  txcnp  23505  ptcnplem  23506  ptcnp  23507  txlly  23521  pthaus  23523  txtube  23525  txhaus  23532  txlm  23533  tx1stc  23535  txkgen  23537  xkohaus  23538  xkopt  23540  xkococnlem  23544  tgqtop  23597  kqfvima  23615  kqt0lem  23621  isr0  23622  regr1lem  23624  kqreglem1  23626  kqreglem2  23627  reghmph  23678  fbssfi  23722  isfil  23732  filuni  23770  isufil  23788  isufil2  23793  fixufil  23807  uffixfr  23808  uffixsn  23810  rnelfm  23838  flimopn  23860  flimrest  23868  flimcls  23870  txflf  23891  fclsopni  23900  fclsrest  23909  fclscf  23910  fcfnei  23920  alexsublem  23929  alexsubALTlem3  23934  alexsubALT  23936  tmdgsum2  23981  symgtgp  23991  subgntr  23992  opnsubg  23993  ghmcnp  24000  tgpt0  24004  qustgpopn  24005  tsmsi  24019  tsmssubm  24028  tsmssplit  24037  isust  24089  ustn0  24106  blssps  24310  blss  24311  blssexps  24312  blssex  24313  neibl  24387  blcld  24391  metss  24394  methaus  24406  met1stc  24407  met2ndci  24408  metrest  24410  prdsxmslem2  24415  metcnp3  24426  dscopn  24459  idnghm  24629  qdensere  24655  tgioo  24682  tgqioo  24686  zdis  24703  xrge0tsms  24721  cnheibor  24852  lmmbr  25156  bcthlem4  25225  ovolicc2lem5  25420  dyadmbllem  25498  i1fd  25580  itg11  25590  itg2gt0  25659  itgeq1f  25670  itgeq1fOLD  25671  itgeq1  25672  bddmulibl  25738  ellimc2  25776  limcnlp  25777  ellimc3  25778  limcflf  25780  limciun  25793  lhop1lem  25916  ig1pdvds  26083  plycpn  26195  aannenlem2  26235  efopn  26565  xrlimcnp  26876  wilthlem2  26977  wilthlem3  26978  nodenselem8  27601  noetasuplem4  27646  noetainflem4  27650  nocvxminlem  27688  lrrecfr  27855  addsprop  27888  bdayon  28178  dfn0s2  28229  tghilberti1  28582  colline  28594  lmif  28730  islmib  28732  incistruhgr  29024  upgr1eopALT  29062  uhgrvtxedgiedgb  29081  upgredg2vtx  29086  edglnl  29088  numedglnl  29089  uhgr2edg  29153  umgrvad2edg  29158  usgredg4  29162  usgredg2vtxeuALT  29167  uspgredg2vlem  29168  ushgredgedg  29174  nbgr1vtx  29303  nbusgredgeu0  29313  nbusgrf1o0  29314  nb3grprlem1  29325  nb3grprlem2  29326  uvtx01vtx  29342  nbupgruvtxres  29352  cplgr1vlem  29374  cplgr1v  29375  vtxd0nedgb  29434  vtxduhgr0nedg  29438  1loopgrvd2  29449  1egrvtxdg0  29457  uspgrloopvtxel  29462  vtxdginducedm1lem4  29488  wlk1walk  29584  wlkp1lem1  29617  pthdivtx  29672  0enwwlksnge1  29809  umgrwwlks2on  29902  rusgr0edg  29918  eleclclwwlkn  30020  upgr4cycl4dv4e  30129  1conngr  30138  vdn0conngrumgrv2  30140  eupth2eucrct  30161  eupth2lem1  30162  frgrncvvdeqlem7  30249  frgrncvvdeqlem9  30251  frgrwopregasn  30260  frgrwopregbsn  30261  l2p  30423  lpni  30424  issh  31152  pjoc1  31378  h1dn0  31496  spansneleqi  31513  nonbooli  31595  pjch  31638  pjnel  31670  cdjreui  32376  rexunirn  32436  rabsnel  32444  nelun  32457  iinabrex  32513  opabdm  32556  opabrn  32557  fpwrelmapffslem  32675  fpwrelmap  32676  fz1nntr  32747  indval  32796  xrge0tsmsd  33015  nsgqusf1olem3  33352  elrspunidl  33365  isprmidl  33375  constrmon  33711  reff  33806  tpr2rico  33879  lmxrge0  33919  issiga  34079  isrnsiga  34080  isldsys  34123  isros  34135  issros  34142  ddeval1  34201  ddeval0  34202  ismbfm  34218  dya2icoseg  34245  dya2iocnrect  34249  ballotlem7  34504  bnj216  34699  bnj563  34710  bnj956  34743  bnj545  34862  bnj548  34864  bnj570  34872  bnj900  34896  bnj929  34903  bnj964  34910  bnj983  34918  bnj1001  34926  bnj1145  34960  bnj1398  35001  bnj1498  35028  wevgblacfn  35082  erdszelem1  35164  kur14lem9  35187  cnllysconn  35218  cvmsss2  35247  cvmcov2  35248  cvmsiota  35250  cvmopnlem  35251  cvmliftlem15  35271  satfv1  35336  satfdmlem  35341  mclsssvlem  35535  mclsind  35543  untelirr  35681  untsucf  35683  elintfv  35738  dfon2lem4  35760  dfon2lem7  35763  dfon2lem9  35765  dfiota3  35897  funpartlem  35916  funpartfun  35917  linethru  36127  hilbert1.1  36128  rankelg  36142  elhf2  36149  neibastop2lem  36334  bj-zfauscl  36898  bj-cleq  36936  bj-snsetex  36937  bj-clel3gALT  37022  bj-nuliota  37031  bj-isrvec  37268  mptsnunlem  37312  isbasisrelowllem1  37329  isbasisrelowllem2  37330  relowlssretop  37337  relowlpssretop  37338  exrecfnlem  37353  finxpeq1  37360  finxpreclem5  37369  finxpreclem6  37370  nlpineqsn  37382  fvineqsneq  37386  pibt2  37391  unccur  37583  fin2so  37587  matunitlindflem1  37596  ptrecube  37600  poimirlem9  37609  poimirlem30  37630  poimir  37633  heicant  37635  mblfinlem1  37637  ftc1anc  37681  ftc2nc  37682  cover2  37695  isbnd2  37763  prdstotbnd  37774  heibor1lem  37789  grpokerinj  37873  rngoueqz  37920  isidl  37994  1idl  38006  0rngo  38007  ispridl  38014  smprngopr  38032  isfldidl  38048  isdmn3  38054  mpobi123f  38142  iineq12f  38144  mptbi12f  38146  eqvrelqsel  38593  n0eldmqseq  38627  dmqseqim2  38635  disjlem17  38777  lsateln0  38974  ispsubsp  39724  linepsubN  39731  elpcliN  39872  dvh3dim3N  41428  dochsnnz  41429  mapdindp3  41701  sn-iotalem  42194  prjspval  42576  elmzpcl  42699  diophren  42786  dford3lem2  43000  ttac  43009  pw2f1ocnv  43010  wepwsolem  43015  kelac1  43036  onexgt  43213  onexlimgt  43216  ordnexbtwnsuc  43240  oaordnr  43269  omnord1  43278  nnoeomeqom  43285  oenord1  43289  succlg  43301  oacl2g  43303  omabs2  43305  omcl2  43306  omcl3g  43307  naddwordnexlem4  43374  nlimsuc  43414  intabssd  43492  elmapintrab  43549  eliunov2  43652  gneispaceel2  44117  mnuop23d  44239  mnuunid  44250  mnurndlem1  44254  expgrowthi  44306  dvconstbi  44307  tratrb  44510  suctrALT2VD  44809  suctrALT2  44810  en3lplem1VD  44816  en3lpVD  44818  tratrbVD  44834  suctrALTcf  44895  suctrALTcfVD  44896  suctrALT3  44897  unisnALT  44899  0elaxnul  44957  pwclaxpow  44958  prclaxpr  44959  uniclaxun  44960  omssaxinf2  44962  wfaxrep  44968  restuni3  45096  supminfxr  45443  xlimxrre  45812  xlimmnfvlem1  45813  xlimpnfvlem1  45817  icccncfext  45868  stoweidlem27  46008  stoweidlem35  46016  stoweidlem46  46027  stoweidlem52  46033  ioorrnopnlem  46285  ioorrnopnxrlem  46287  issal  46295  intsaluni  46310  salgencntex  46324  smfresal  46769  tannpoly  46874  funressnfv  47027  fnbrafvb  47138  afvco2  47160  ndmaovg  47168  aovmpt4g  47185  fafv2elrnb  47219  fvelsetpreimafv  47371  elsetpreimafvbi  47375  sprsymrelf1lem  47475  paireqne  47495  fpprbasnn  47713  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  dfclnbgr6  47840  dfsclnbgr6  47842  grtri  47924  stgrvtx0  47946  stgrnbgr0  47948  isubgr3stgrlem3  47952  gpgvtx0  48037  gpgvtx1  48038  gpg3kgrtriex  48073  pgnbgreunbgrlem3  48102  pgnbgreunbgrlem6  48108  rngccatidALTV  48256  ringccatidALTV  48290  ldepspr  48458  mosn  48797  indthinc  49447  indthincALT  49448