Theorem eleq2 2677

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  eleq12  2678  eleq2i  2680  nelneq2  2713  dvelimdc  2772  nelne1  2878  raleqf  3111  rexeqf  3112  reueq1f  3113  rmoeq1f  3114  raleleq  3133  rabeqf  3165  clel3g  3310  clel4  3312  sbcbi2  3451  sbcel2gv  3463  csbeq2  3503  difeq2  3684  uneq1  3722  ineq1  3769  unineq  3836  n0i  3879  sbnfc2  3959  disjel  3975  elif  4078  exsnrex  4168  sneqrg  4310  preq1b  4317  preqr1OLD  4320  preq12b  4322  prel12  4323  elpreqprb  4335  elunii  4377  eluniab  4383  ssuniOLD  4396  elinti  4420  elintab  4422  intss1  4427  intmin  4432  intab  4442  iineq2  4474  dfiin2g  4489  breq  4585  zfrepclf  4705  axsep2  4710  zfauscl  4711  sseliALT  4719  inuni  4753  elALT  4837  rext  4843  intid  4853  elopg  4861  opth1  4870  opthwiener  4901  xpeq1  5052  xpeq2  5053  0nelelxp  5069  opthprc  5089  ordtri1  5673  ordtri3  5676  ordtri3OLD  5677  nsuceq0  5722  suctr  5725  suctrOLD  5726  ordnbtwn  5733  ordnbtwnOLD  5734  funopg  5836  dffv2  6181  fveqdmss  6262  dffo4  6283  fnsnb  6337  elunirn  6413  f1oiso  6501  canth  6508  eusvobj2  6542  mpt2eq123  6612  ndmovg  6715  snnex  6862  uniuni  6865  iunpw  6870  oneqmin  6897  onuninsuci  6932  nlimsucg  6934  limomss  6962  nnlim  6970  peano5  6981  unielxp  7095  cnvf1o  7163  smoel  7344  smo11  7348  tz7.44-2  7390  oawordeulem  7521  oaordex  7525  omordi  7533  oneo  7548  oeordi  7554  oeoa  7564  oeoe  7566  nnmordi  7598  nnaordex  7605  omabs  7614  nnneo  7618  omsmolem  7620  elqsn0  7703  qsel  7713  mapsn  7785  undifixp  7830  boxriin  7836  boxcutc  7837  fineqvlem  8059  fineqv  8060  pssnn  8063  fissuni  8154  dffi2  8212  inficl  8214  dffi3  8220  wofib  8333  zfregcl  8382  zfregclOLD  8384  en3lplem1  8394  en3lp  8396  suc11reg  8399  inf0  8401  inf3lem2  8409  inf3lem3  8410  infeq5i  8416  axinf2  8420  dfom3  8427  elom3  8428  cantnfle  8451  oemapvali  8464  cantnflem1c  8467  cantnflem1  8469  tc2  8501  r1sdom  8520  rankwflemb  8539  rankval3b  8572  rankunb  8596  rankuni2b  8599  tcrank  8630  cardlim  8681  cardprclem  8688  infxpenlem  8719  alephnbtwn  8777  alephordi  8780  cardaleph  8795  alephfp  8814  alephval3  8816  aceq1  8823  aceq2  8825  dfac3  8827  dfac5lem2  8830  dfac5lem4  8832  dfac2  8836  kmlem2  8856  kmlem4  8858  coflim  8966  cfsmolem  8975  fin23lem30  9047  isf32lem2  9059  isf34lem4  9082  axdc2lem  9153  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  zorn2lem7  9207  axdclem  9224  brdom7disj  9234  brdom6disj  9235  axpowndlem3  9300  winainflem  9394  iswun  9405  eltskg  9451  inar1  9476  elgrug  9493  inaprc  9537  eltskm  9544  addnidpi  9602  indpi  9608  nqereu  9630  elnp  9688  elnpi  9689  genpnnp  9706  ltaddpr  9735  dfnn2  10910  dfnn3  10911  dfuzi  11344  uz11  11586  elfzonlteqm1  12410  om2uzlti  12611  axdc4uz  12645  hashrabsn1  13024  hashbclem  13093  hashf1lem2  13097  hash2prb  13111  hash2prd  13114  fundmge2nop0  13129  wrdsymb0  13194  lsw0  13205  rtrclreclem3  13648  prodeq1f  14477  rpnnen2lem1  14782  rpnnen2lem2  14783  sadcp1  15015  lcmfval  15172  lcmf0val  15173  ismre  16073  isacs  16135  initoid  16478  termoid  16479  initoeu2lem1  16487  clatl  16939  mreclatBAD  17010  issubm  17170  dfgrp2e  17271  cycsubg  17445  isnsg  17446  subgacs  17452  nsgacs  17453  resghm  17499  ghmeql  17506  gsmsymgreq  17675  f1otrspeq  17690  pmtrval  17694  pmtrdifellem4  17722  pmtrprfval  17730  gsumzsplit  18150  pgpfac1lem1  18296  pgpfac1lem5  18301  pgpfac1  18302  issubrg  18603  lmodfopnelem2  18723  islss  18756  lssacs  18788  lspsneq0  18833  lmhmeql  18876  lspdisjb  18947  lidl1el  19039  lidldvgen  19076  0ring01eq  19092  mplcoe1  19286  mplcoe5  19289  islindf4  19996  m1detdiag  20222  mdetunilem9  20245  maducoeval2  20265  madugsum  20268  chpmat1dlem  20459  istopg  20525  fiinbas  20567  topbas  20587  ppttop  20621  pptbas  20622  epttop  20623  elcls  20687  clsndisj  20689  elcls3  20697  iscldtop  20709  neiptopnei  20746  restbas  20772  restntr  20796  pnfnei  20834  mnfnei  20835  cnpimaex  20870  lmcvg  20876  iscnp4  20877  cncnpi  20892  cnconst2  20897  cnprest  20903  cnprest2  20904  cnpdis  20907  lmss  20912  lmff  20915  cnt0  20960  ist1-3  20963  cnhaus  20968  isreg2  20991  dishaus  20996  ordthauslem  20997  cmpsublem  21012  cmpsub  21013  cmpcld  21015  hauscmplem  21019  uncon  21042  concompid  21044  concompcon  21045  concompss  21046  1stcfb  21058  1stcrest  21066  2ndcctbss  21068  2ndcomap  21071  dis2ndc  21073  1stcelcls  21074  llyeq  21083  nllyeq  21084  restnlly  21095  restlly  21096  islly2  21097  lly1stc  21109  dislly  21110  hauspwdom  21114  finlocfin  21133  unisngl  21140  dissnlocfin  21142  locfindis  21143  comppfsc  21145  llycmpkgen2  21163  txbas  21180  eltx  21181  ptpjopn  21225  ptclsg  21228  dfac14lem  21230  txcnp  21233  ptcnplem  21234  ptcnp  21235  txlly  21249  pthaus  21251  txtube  21253  txhaus  21260  txlm  21261  tx1stc  21263  txkgen  21265  xkohaus  21266  xkopt  21268  xkococnlem  21272  tgqtop  21325  kqfvima  21343  kqt0lem  21349  isr0  21350  r0cld  21351  regr1lem  21352  kqreglem1  21354  kqreglem2  21355  reghmph  21406  fbssfi  21451  isfil  21461  filuni  21499  isufil  21517  isufil2  21522  uffix  21535  fixufil  21536  uffixfr  21537  uffixsn  21539  rnelfm  21567  flimopn  21589  flimrest  21597  flimcls  21599  flftg  21610  txflf  21620  fclsopni  21629  fclsrest  21638  fclscf  21639  fcfnei  21649  alexsublem  21658  alexsubALTlem3  21663  alexsubALT  21665  tmdgsum2  21710  symgtgp  21715  subgntr  21720  opnsubg  21721  tgpconcompeqg  21725  ghmcnp  21728  tgpt0  21732  qustgpopn  21733  tsmsi  21747  tsmssubm  21756  tsmssplit  21765  isust  21817  ustn0  21834  blssps  22039  blss  22040  blssexps  22041  blssex  22042  neibl  22116  blcld  22120  metss  22123  methaus  22135  met1stc  22136  met2ndci  22137  metrest  22139  prdsxmslem2  22144  metcnp3  22155  dscopn  22188  idnghm  22357  qdensere  22383  tgioo  22407  tgqioo  22411  zdis  22427  xrge0tsms  22445  cnheibor  22562  lmmbr  22864  bcthlem4  22932  ovolicc2lem5  23096  dyadmbllem  23173  i1fd  23254  itg11  23264  itg2gt0  23333  itgeq1f  23344  bddmulibl  23411  ellimc2  23447  limcnlp  23448  ellimc3  23449  limcflf  23451  limciun  23464  lhop1lem  23580  ig1pdvds  23740  plycpn  23848  aannenlem2  23888  efopn  24204  xrlimcnp  24495  wilthlem2  24595  wilthlem3  24596  wilth  24597  tghilberti1  25332  tghilberti2  25333  colline  25344  lmif  25477  islmib  25479  incistruhgr  25746  upgr1eopALT  25783  uhgrvtxedgiedgb  25810  upgredg2vtx  25814  usgra2edg  25911  usgraedg4  25916  nbgraf1olem1  25970  nbgraf1olem3  25972  nb3graprlem1  25980  nb3graprlem2  25981  uvtx01vtx  26020  uvtxnbgravtx  26023  2trllemF  26079  wlkntrl  26092  constr1trl  26118  eleclclwwlkn  26360  vdgr1a  26433  vdusgra0nedg  26435  usgravd0nedg  26445  eupath2lem1  26504  vdn0frgrav2  26550  vdgn0frgrav2  26551  frgrancvvdeqlem4  26560  frgrancvvdeqlem7  26563  frgrancvvdeqlemA  26564  frgrancvvdeqlemC  26566  frgrawopreg1  26577  frgrawopreg2  26578  lpni  26722  issh  27449  pjoc1  27677  h1dn0  27795  spansneleqi  27812  nonbooli  27894  pjch  27937  pjnel  27969  cdjreui  28675  rexunirn  28715  rabsnel  28726  opabdm  28803  opabrn  28804  fpwrelmapffslem  28895  fpwrelmap  28896  fz1nntr  28948  xrge0tsmsd  29116  reff  29234  tpr2rico  29286  lmxrge0  29326  indval  29403  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503  isldsys  29546  isros  29558  issros  29565  ddeval1  29624  ddeval0  29625  ddemeas  29626  ismbfm  29641  isanmbfm  29645  dya2icoseg  29666  dya2iocnrect  29670  ballotlem7  29924  bnj145OLD  30049  bnj216  30054  bnj563  30067  bnj956  30101  bnj545  30219  bnj548  30221  bnj570  30229  bnj900  30253  bnj929  30260  bnj964  30267  bnj983  30275  bnj1001  30282  bnj1145  30315  bnj1398  30356  bnj1498  30383  erdszelem1  30427  kur14lem9  30450  cnllyscon  30481  cvmcov  30499  cvmsss2  30510  cvmcov2  30511  cvmseu  30512  cvmsiota  30513  cvmopnlem  30514  cvmliftlem15  30534  mclsssvlem  30713  mclsind  30721  untelirr  30839  untsucf  30841  dfon2lem4  30935  dfon2lem7  30938  dfon2lem9  30940  soseq  30995  frrlem4  31027  frrlem5e  31032  frrlem11  31036  nodenselem8  31087  nocvxminlem  31089  nofulllem5  31105  dfiota3  31200  funpartlem  31219  funpartfun  31220  linethru  31430  hilbert1.1  31431  hilbert1.2  31432  rankelg  31445  elhf2  31452  fneint  31513  neibastop2lem  31525  bj-axc14nf  32031  bj-rabeqd  32108  bj-cleq  32142  bj-snsetex  32144  bj-nuliota  32210  bj-toprntopon  32244  bj-xnex  32245  mptsnunlem  32361  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  relowlpssretop  32388  finxpeq1  32399  finxpreclem5  32408  finxpreclem6  32409  unccur  32562  fin2so  32566  matunitlindflem1  32575  ptrecube  32579  poimirlem9  32588  poimirlem30  32609  poimir  32612  heicant  32614  mblfinlem1  32616  ftc1anc  32663  ftc2nc  32664  cover2  32678  isbnd2  32752  prdstotbnd  32763  heibor1lem  32778  grpokerinj  32862  rngoueqz  32909  isidl  32983  1idl  32995  0rngo  32996  ispridl  33003  smprngopr  33021  isfldidl  33037  isdmn3  33043  mpt2bi123f  33141  iineq12f  33143  mptbi12f  33145  lsateln0  33300  ispsubsp  34049  linepsubN  34056  elpcliN  34197  dvh3dim3N  35756  dochsnnz  35757  mapdindp3  36029  elmzpcl  36307  diophren  36395  dford3lem2  36612  ttac  36621  pw2f1ocnv  36622  wepwsolem  36630  kelac1  36651  sdrgacs  36790  elintabg  36899  elmapintrab  36901  intabssd  36935  eliunov2  36990  gneispaceel2  37462  expgrowthi  37554  dvconstbi  37555  tratrb  37767  suctrALT2VD  38093  suctrALT2  38094  en3lplem1VD  38100  en3lpVD  38102  tratrbVD  38119  suctrALTcf  38180  suctrALTcfVD  38181  suctrALT3  38182  unisnALT  38184  elunif  38198  fnchoice  38211  restuni3  38333  mapsnd  38383  icccncfext  38773  stoweidlem27  38920  stoweidlem35  38928  stoweidlem46  38939  stoweidlem52  38945  ioorrnopnlem  39200  ioorrnopnxrlem  39202  issal  39210  intsaluni  39223  salgencntex  39237  sge0f1o  39275  smfresal  39673  funressnfv  39857  fnbrafvb  39883  afvco2  39905  ndmaovg  39913  aovmpt4g  39930  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  fzoopth  40360  uhgr2edg  40435  umgrvad2edg  40440  umgr2edgneu  40441  usgredg4  40444  usgredg2vtxeuALT  40449  uspgredg2vlem  40450  uspgredg2v  40451  ushgredgedga  40456  usgredgaleordALT  40461  nbgr1vtx  40580  nbusgredgeu0  40596  nbusgrf1o0  40597  nbusgrf1o  40599  nb3grprlem1  40608  nb3grprlem2  40609  uvtxa01vtx0  40623  nbupgruvtxres  40634  cplgr1vlem  40651  cplgr1v  40652  vtxd0nedgb  40703  vtxdushgrfvedglem  40704  vtxduhgr0nedg  40707  1loopgrvd2  40718  1egrvtxdg0  40727  uspgrloopvtxel  40732  1wlk1walk  40843  1wlkp1lem1  40882  pthdivtx  40935  0enwwlksnge1  41060  umgrwwlks2on  41161  rusgr0edg  41176  eleclclwwlksn  41260  upgr4cycl4dv4e  41352  1conngr  41361  vdn0conngrumgrv2  41363  eupth2eucrct  41385  eupth2lem1  41386  frgrncvvdeqlem4  41472  frgrncvvdeqlem7  41475  frgrncvvdeqlemA  41476  frgrncvvdeqlemC  41478  frgrwopreg1  41487  frgrwopreg2  41488  issubmgm  41579  c0snmgmhm  41704  c0snmhm  41705  rngccatidALTV  41781  ringccatidALTV  41844  ldepspr  42056