Theorem eleq2 2901

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  eleq12  2902  eleq2i  2904  nelneq2  2938  dvelimdc  3005  nelne1OLD  3114  raleqf  3397  rexeqf  3398  reueq1f  3399  rmoeq1f  3400  reueq1  3407  rmoeq1  3408  raleleq  3427  rabeqf  3481  rabeqi  3482  rabeq  3483  clel3g  3654  clel4  3656  sbcbi2OLD  3832  sbcel2gv  3841  csbeq2  3888  difeq2  4093  uneq1  4132  ineq1OLD  4182  unineq  4254  nel02  4298  n0i  4299  sbnfc2  4388  disjel  4406  elif  4509  exsnrex  4618  elinsn  4646  sneqrg  4770  preq1b  4777  preq12b  4781  elpreqprb  4798  elunii  4843  elinti  4885  intss1  4891  intmin  4896  intab  4906  iuneqconst  4930  iineq2  4939  dfiin2g  4957  breq  5068  zfrepclf  5198  zfauscl  5205  sseliALT  5213  inuni  5246  sels  5334  elALT  5335  rext  5341  intid  5350  elopg  5358  opth1  5367  opthwiener  5404  xpeq1  5569  xpeq2  5576  0nelelxp  5590  opthprc  5616  ordtri1  6224  ordtri3  6227  nsuceq0  6271  suctr  6274  ordnbtwn  6281  funopg  6389  dffv2  6756  fveqdmss  6846  dffo4  6869  funopdmsn  6912  fnsnb  6928  elunirn  7010  f1oiso  7104  canth  7111  eusvobj2  7149  mpoeq123  7226  ndmovg  7331  uniuni  7484  iunpw  7493  oneqmin  7520  onuninsuci  7555  nlimsucg  7557  limomss  7585  nnlim  7593  peano5  7605  unielxp  7727  cnvf1o  7806  smoel  7997  smo11  8001  tz7.44-2  8043  oawordeulem  8180  oaordex  8184  omordi  8192  oneo  8207  oeordi  8213  oeoa  8223  oeoe  8225  nnmordi  8257  nnaordex  8264  omabs  8274  nnneo  8278  omsmolem  8280  elqsn0  8366  qsel  8376  mapsnd  8450  undifixp  8498  boxriin  8504  boxcutc  8505  fineqvlem  8732  fineqv  8733  pssnn  8736  fissuni  8829  dffi2  8887  inficl  8889  dffi3  8895  wofib  9009  zfregcl  9058  en3lplem1  9075  en3lp  9077  suc11reg  9082  inf0  9084  inf3lem2  9092  inf3lem3  9093  infeq5i  9099  axinf2  9103  dfom3  9110  elom3  9111  cantnfle  9134  oemapvali  9147  cantnflem1  9152  tc2  9184  r1sdom  9203  rankwflemb  9222  rankval3b  9255  rankunb  9279  rankuni2b  9282  cardlim  9401  cardprclem  9408  infxpenlem  9439  alephnbtwn  9497  alephordi  9500  cardaleph  9515  alephfp  9534  alephval3  9536  dfac3  9547  dfac5lem2  9550  dfac5lem4  9552  dfac2b  9556  kmlem2  9577  coflim  9683  cfsmolem  9692  fin23lem30  9764  isf34lem4  9799  axdc2lem  9870  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  zorn2lem7  9924  axdclem  9941  brdom7disj  9953  brdom6disj  9954  axpowndlem3  10021  winainflem  10115  iswun  10126  eltskg  10172  inar1  10197  elgrug  10214  inaprc  10258  eltskm  10265  addnidpi  10323  indpi  10329  nqereu  10351  elnp  10409  elnpi  10410  genpnnp  10427  ltaddpr  10456  dfnn2  11651  dfnn3  11652  dfuzi  12074  uz11  12268  elfzonlteqm1  13114  om2uzlti  13319  axdc4uz  13353  hashrabsn1  13736  hashbclem  13811  hashf1lem2  13815  hash2prb  13831  hash2prd  13834  wrdsymb0  13901  lsw0  13917  swrdwrdsymb  14024  rtrclreclem3  14419  prodeq1f  15262  rpnnen2lem1  15567  rpnnen2lem2  15568  lcmfval  15965  lcmf0val  15966  ismre  16861  isacs  16922  initoid  17265  termoid  17266  initoeu2lem1  17274  clatl  17726  mreclatBAD  17797  issubm  17968  dfgrp2e  18129  isnsg  18307  cycsubg  18351  resghm  18374  ghmeql  18381  gsmsymgreq  18560  f1otrspeq  18575  pmtrval  18579  pmtrdifellem4  18607  pmtrprfval  18615  gsumzsplit  19047  pgpfac1lem1  19196  pgpfac1lem5  19201  pgpfac1  19202  ablsimpnosubgd  19226  issubrg  19535  lmodfopnelem2  19671  islss  19706  lspsneq0  19784  lmhmeql  19827  lspdisjb  19898  lidl1el  19991  lidldvgen  20028  0ring01eq  20044  mplcoe1  20246  mplcoe5  20249  selvfval  20330  islindf4  20982  m1detdiag  21206  mdetunilem9  21229  maducoeval2  21249  madugsum  21252  chpmat1dlem  21443  istopg  21503  toprntopon  21533  fiinbas  21560  topbas  21580  ppttop  21615  pptbas  21616  epttop  21617  elcls  21681  clsndisj  21683  iscldtop  21703  neiptopnei  21740  restbas  21766  restntr  21790  pnfnei  21828  mnfnei  21829  cnpimaex  21864  lmcvg  21870  iscnp4  21871  cncnpi  21886  cnconst2  21891  cnprest  21897  cnprest2  21898  cnpdis  21901  lmss  21906  lmff  21909  cnt0  21954  ist1-3  21957  cnhaus  21962  isreg2  21985  dishaus  21990  ordthauslem  21991  cmpsublem  22007  cmpsub  22008  cmpcld  22010  hauscmplem  22014  unconn  22037  conncompid  22039  conncompss  22041  1stcfb  22053  1stcrest  22061  2ndcctbss  22063  2ndcomap  22066  dis2ndc  22068  1stcelcls  22069  llyeq  22078  nllyeq  22079  restnlly  22090  islly2  22092  lly1stc  22104  dislly  22105  hauspwdom  22109  finlocfin  22128  unisngl  22135  dissnlocfin  22137  locfindis  22138  comppfsc  22140  llycmpkgen2  22158  txbas  22175  eltx  22176  ptpjopn  22220  ptclsg  22223  txcnp  22228  ptcnplem  22229  ptcnp  22230  txlly  22244  pthaus  22246  txtube  22248  txhaus  22255  txlm  22256  tx1stc  22258  txkgen  22260  xkohaus  22261  xkopt  22263  xkococnlem  22267  tgqtop  22320  kqfvima  22338  kqt0lem  22344  isr0  22345  regr1lem  22347  kqreglem1  22349  kqreglem2  22350  reghmph  22401  fbssfi  22445  isfil  22455  filuni  22493  isufil  22511  isufil2  22516  fixufil  22530  uffixfr  22531  uffixsn  22533  rnelfm  22561  flimopn  22583  flimrest  22591  flimcls  22593  txflf  22614  fclsopni  22623  fclsrest  22632  fclscf  22633  fcfnei  22643  alexsublem  22652  alexsubALTlem3  22657  alexsubALT  22659  tmdgsum2  22704  symgtgp  22714  subgntr  22715  opnsubg  22716  ghmcnp  22723  tgpt0  22727  qustgpopn  22728  tsmsi  22742  tsmssubm  22751  tsmssplit  22760  isust  22812  ustn0  22829  blssps  23034  blss  23035  blssexps  23036  blssex  23037  neibl  23111  blcld  23115  metss  23118  methaus  23130  met1stc  23131  met2ndci  23132  metrest  23134  prdsxmslem2  23139  metcnp3  23150  dscopn  23183  idnghm  23352  qdensere  23378  tgioo  23404  tgqioo  23408  zdis  23424  xrge0tsms  23442  cnheibor  23559  lmmbr  23861  bcthlem4  23930  ovolicc2lem5  24122  dyadmbllem  24200  i1fd  24282  itg11  24292  itg2gt0  24361  itgeq1f  24372  bddmulibl  24439  ellimc2  24475  limcnlp  24476  ellimc3  24477  limcflf  24479  limciun  24492  lhop1lem  24610  ig1pdvds  24770  plycpn  24878  aannenlem2  24918  efopn  25241  xrlimcnp  25546  wilthlem2  25646  wilthlem3  25647  tghilberti1  26423  colline  26435  lmif  26571  islmib  26573  incistruhgr  26864  upgr1eopALT  26902  uhgrvtxedgiedgb  26921  upgredg2vtx  26926  edglnl  26928  numedglnl  26929  uhgr2edg  26990  umgrvad2edg  26995  usgredg4  26999  usgredg2vtxeuALT  27004  uspgredg2vlem  27005  ushgredgedg  27011  nbgr1vtx  27140  nbusgredgeu0  27150  nbusgrf1o0  27151  nb3grprlem1  27162  nb3grprlem2  27163  uvtx01vtx  27179  nbupgruvtxres  27189  cplgr1vlem  27211  cplgr1v  27212  vtxd0nedgb  27270  vtxduhgr0nedg  27274  1loopgrvd2  27285  1egrvtxdg0  27293  uspgrloopvtxel  27298  vtxdginducedm1lem4  27324  wlk1walk  27420  wlkp1lem1  27455  pthdivtx  27510  0enwwlksnge1  27642  umgrwwlks2on  27736  rusgr0edg  27752  eleclclwwlkn  27855  upgr4cycl4dv4e  27964  1conngr  27973  vdn0conngrumgrv2  27975  eupth2eucrct  27996  eupth2lem1  27997  frgrncvvdeqlem7  28084  frgrncvvdeqlem9  28086  frgrwopregasn  28095  frgrwopregbsn  28096  l2p  28256  lpni  28257  issh  28985  pjoc1  29211  h1dn0  29329  spansneleqi  29346  nonbooli  29428  pjch  29471  pjnel  29503  cdjreui  30209  rexunirn  30256  rabsnel  30263  nelun  30274  opabdm  30362  opabrn  30363  fpwrelmapffslem  30468  fpwrelmap  30469  fz1nntr  30527  xrge0tsmsd  30692  isprmidl  30955  reff  31103  tpr2rico  31155  lmxrge0  31195  indval  31272  issiga  31371  isrnsiga  31372  isldsys  31415  isros  31427  issros  31434  ddeval1  31493  ddeval0  31494  ismbfm  31510  isanmbfm  31514  dya2icoseg  31535  dya2iocnrect  31539  ballotlem7  31793  bnj216  32002  bnj563  32014  bnj956  32048  bnj545  32167  bnj548  32169  bnj570  32177  bnj900  32201  bnj929  32208  bnj964  32215  bnj983  32223  bnj1001  32231  bnj1145  32265  bnj1398  32306  bnj1498  32333  erdszelem1  32438  kur14lem9  32461  cnllysconn  32492  cvmsss2  32521  cvmcov2  32522  cvmsiota  32524  cvmopnlem  32525  cvmliftlem15  32545  satfv1  32610  satfdmlem  32615  mclsssvlem  32809  mclsind  32817  untelirr  32934  untsucf  32936  elintfv  33007  dfon2lem4  33031  dfon2lem7  33034  dfon2lem9  33036  soseq  33096  nodenselem8  33195  noetalem3  33219  nocvxminlem  33247  dfiota3  33384  funpartlem  33403  funpartfun  33404  linethru  33614  hilbert1.1  33615  rankelg  33629  elhf2  33636  neibastop2lem  33708  bj-rabeqd  34241  bj-zfauscl  34246  bj-cleq  34277  bj-snsetex  34278  bj-nuliota  34353  mptsnunlem  34622  isbasisrelowllem1  34639  isbasisrelowllem2  34640  relowlssretop  34647  relowlpssretop  34648  exrecfnlem  34663  finxpeq1  34670  finxpreclem5  34679  finxpreclem6  34680  nlpineqsn  34692  fvineqsneu  34695  fvineqsneq  34696  pibt2  34701  unccur  34890  fin2so  34894  matunitlindflem1  34903  ptrecube  34907  poimirlem9  34916  poimirlem30  34937  poimir  34940  heicant  34942  mblfinlem1  34944  ftc1anc  34990  ftc2nc  34991  cover2  35004  isbnd2  35076  prdstotbnd  35087  heibor1lem  35102  grpokerinj  35186  rngoueqz  35233  isidl  35307  1idl  35319  0rngo  35320  ispridl  35327  smprngopr  35345  isfldidl  35361  isdmn3  35367  mpobi123f  35455  iineq12f  35457  mptbi12f  35459  eqvrelqsel  35866  n0eldmqseq  35899  dmqseqim2  35906  lsateln0  36146  ispsubsp  36896  linepsubN  36903  elpcliN  37044  dvh3dim3N  38600  dochsnnz  38601  mapdindp3  38873  prjspval  39302  elmzpcl  39372  diophren  39459  dford3lem2  39673  ttac  39682  pw2f1ocnv  39683  wepwsolem  39691  kelac1  39712  intabssd  39934  elmapintrab  39985  eliunov2  40073  gneispaceel2  40543  mnuop23d  40651  mnuunid  40662  mnurndlem1  40666  expgrowthi  40714  dvconstbi  40715  tratrb  40919  suctrALT2VD  41219  suctrALT2  41220  en3lplem1VD  41226  en3lpVD  41228  tratrbVD  41244  suctrALTcf  41305  suctrALTcfVD  41306  suctrALT3  41307  unisnALT  41309  restuni3  41433  supminfxr  41789  xlimxrre  42161  xlimmnfvlem1  42162  xlimpnfvlem1  42166  icccncfext  42219  stoweidlem27  42361  stoweidlem35  42369  stoweidlem46  42380  stoweidlem52  42386  ioorrnopnlem  42638  ioorrnopnxrlem  42640  issal  42648  intsaluni  42661  salgencntex  42675  sge0f1o  42713  smfresal  43112  funressnfv  43327  fnbrafvb  43402  afvco2  43424  ndmaovg  43432  aovmpt4g  43449  fafv2elrnb  43483  fzoopth  43576  fvelsetpreimafv  43596  elsetpreimafvbi  43600  sprsymrelf1lem  43702  paireqne  43722  fpprbasnn  43943  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  issubmgm  44105  c0snmgmhm  44234  c0snmhm  44235  rngccatidALTV  44309  ringccatidALTV  44372  ldepspr  44577