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 205   = wceq 1540   ∈ wcel 2105

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728  df-clel 2814

This theorem is referenced by:  eleq12  2826  eleq2i  2828  nelneq2  2862  clelsb2OLD  2866  dvelimdc  2931  raleleq  3313  raleqf  3324  rexeqf  3325  rmoeq1  3387  reueq1  3388  rmoeq1f  3391  reueq1f  3392  rabeq  3416  rabeqf  3433  rabeqiOLD  3437  clel3g  3600  clel4g  3602  clel4OLD  3604  sbcbi2  3787  sbcel2gv  3797  csbeq2  3846  difeq2  4061  uneq1  4100  unineq  4221  nel02  4276  n0i  4277  sbnfc2  4380  disjel  4400  elif  4513  exsnrex  4625  elinsn  4655  sneqrg  4781  preq1b  4788  preq12b  4792  elpreqprb  4809  elunii  4854  elinti  4900  intss1  4906  intmin  4911  intab  4921  iuneqconst  4947  iineq2  4956  dfiun2g  4972  dfiin2g  4974  breq  5088  zfrepclf  5232  zfauscl  5239  sseliALT  5247  inuni  5281  sels  5374  elALT  5376  rext  5382  intid  5391  elopg  5399  opth1  5408  opthwiener  5446  xpeq1  5621  xpeq2  5628  0nelelxp  5642  opthprc  5669  ordtri1  6321  ordtri3  6324  nsuceq0  6370  suctr  6373  ordnbtwn  6380  funopg  6504  dffv2  6902  fveqdmss  6995  dffo4  7018  funopdmsn  7061  fnsnb  7077  elunirn  7163  f1oiso  7261  canth  7270  eusvobj2  7309  mpoeq123  7388  ndmovg  7496  uniuni  7653  iunpw  7662  oneqmin  7691  onuninsuci  7732  nlimsucg  7734  limomss  7763  nnlim  7772  peano5  7786  peano5OLD  7787  unielxp  7915  cnvf1o  7997  soseq  8024  smoel  8239  smo11  8243  tz7.44-2  8286  nlim2  8369  ord1eln01  8375  ord2eln012  8376  oawordeulem  8434  oaordex  8438  omordi  8446  oneo  8461  oeordi  8467  oeoa  8477  oeoe  8479  nnmordi  8511  nnaordex  8518  omabs  8530  nnneo  8534  omsmolem  8536  elqsn0  8624  qsel  8634  mapsnd  8723  undifixp  8771  boxriin  8777  boxcutc  8778  pssnn  9011  fineqvlem  9105  fineqv  9106  pssnnOLD  9108  en1eqsn  9117  fissuni  9200  dffi2  9258  inficl  9260  dffi3  9266  wofib  9380  zfregcl  9429  en3lplem1  9447  en3lp  9449  suc11reg  9454  inf0  9456  inf3lem2  9464  inf3lem3  9465  infeq5i  9471  axinf2  9475  dfom3  9482  elom3  9483  cantnfle  9506  oemapvali  9519  cantnflem1  9524  tc2  9577  r1sdom  9609  rankwflemb  9628  rankval3b  9661  rankunb  9685  rankuni2b  9688  cardlim  9807  cardprclem  9814  infxpenlem  9848  alephnbtwn  9906  alephordi  9909  cardaleph  9924  alephfp  9943  alephval3  9945  dfac3  9956  dfac5lem2  9959  dfac5lem4  9961  dfac2b  9965  kmlem2  9986  coflim  10096  cfsmolem  10105  fin23lem30  10177  isf34lem4  10212  axdc2lem  10283  axdc3lem2  10286  axdc3lem4  10288  axdc4lem  10290  zorn2lem7  10337  axdclem  10354  brdom7disj  10366  brdom6disj  10367  axpowndlem3  10434  winainflem  10528  iswun  10539  eltskg  10585  inar1  10610  elgrug  10627  inaprc  10671  eltskm  10678  addnidpi  10736  indpi  10742  nqereu  10764  elnp  10822  elnpi  10823  genpnnp  10840  ltaddpr  10869  dfnn2  12065  dfnn3  12066  dfuzi  12490  uz11  12686  elfzonlteqm1  13542  om2uzlti  13749  axdc4uz  13783  hashrabsn1  14167  hashbclem  14242  hashf1lem2  14248  hash2prb  14264  hash2prd  14267  wrdsymb0  14330  lsw0  14346  swrdwrdsymb  14451  rtrclreclem3  14847  prodeq1f  15694  rpnnen2lem1  15999  rpnnen2lem2  16000  lcmfval  16400  lcmf0val  16401  ismre  17373  isacs  17434  initoid  17790  termoid  17791  initoeu2lem1  17803  clatl  18300  mreclatBAD  18355  issubm  18516  dfgrp2e  18678  isnsg  18856  cycsubg  18900  resghm  18923  ghmeql  18930  gsmsymgreq  19113  f1otrspeq  19128  pmtrval  19132  pmtrdifellem4  19160  pmtrprfval  19168  gsumzsplit  19600  pgpfac1lem1  19749  pgpfac1lem5  19754  pgpfac1  19755  ablsimpnosubgd  19779  issubrg  20103  lmodfopnelem2  20240  islss  20276  lspsneq0  20354  lmhmeql  20397  lspdisjb  20468  lidl1el  20569  lidldvgen  20606  0ring01eq  20622  islindf4  21125  mplcoe1  21318  mplcoe5  21321  selvfval  21407  m1detdiag  21826  mdetunilem9  21849  maducoeval2  21869  madugsum  21872  chpmat1dlem  22064  istopg  22124  toprntopon  22154  fiinbas  22182  topbas  22202  ppttop  22237  pptbas  22238  epttop  22239  elcls  22304  clsndisj  22306  iscldtop  22326  neiptopnei  22363  restbas  22389  restntr  22413  pnfnei  22451  mnfnei  22452  cnpimaex  22487  lmcvg  22493  iscnp4  22494  cncnpi  22509  cnconst2  22514  cnprest  22520  cnprest2  22521  cnpdis  22524  lmss  22529  lmff  22532  cnt0  22577  ist1-3  22580  cnhaus  22585  isreg2  22608  dishaus  22613  ordthauslem  22614  cmpsublem  22630  cmpsub  22631  cmpcld  22633  hauscmplem  22637  unconn  22660  conncompid  22662  conncompss  22664  1stcfb  22676  1stcrest  22684  2ndcctbss  22686  2ndcomap  22689  dis2ndc  22691  1stcelcls  22692  llyeq  22701  nllyeq  22702  restnlly  22713  islly2  22715  lly1stc  22727  dislly  22728  hauspwdom  22732  finlocfin  22751  unisngl  22758  dissnlocfin  22760  locfindis  22761  comppfsc  22763  llycmpkgen2  22781  txbas  22798  eltx  22799  ptpjopn  22843  ptclsg  22846  txcnp  22851  ptcnplem  22852  ptcnp  22853  txlly  22867  pthaus  22869  txtube  22871  txhaus  22878  txlm  22879  tx1stc  22881  txkgen  22883  xkohaus  22884  xkopt  22886  xkococnlem  22890  tgqtop  22943  kqfvima  22961  kqt0lem  22967  isr0  22968  regr1lem  22970  kqreglem1  22972  kqreglem2  22973  reghmph  23024  fbssfi  23068  isfil  23078  filuni  23116  isufil  23134  isufil2  23139  fixufil  23153  uffixfr  23154  uffixsn  23156  rnelfm  23184  flimopn  23206  flimrest  23214  flimcls  23216  txflf  23237  fclsopni  23246  fclsrest  23255  fclscf  23256  fcfnei  23266  alexsublem  23275  alexsubALTlem3  23280  alexsubALT  23282  tmdgsum2  23327  symgtgp  23337  subgntr  23338  opnsubg  23339  ghmcnp  23346  tgpt0  23350  qustgpopn  23351  tsmsi  23365  tsmssubm  23374  tsmssplit  23383  isust  23435  ustn0  23452  blssps  23657  blss  23658  blssexps  23659  blssex  23660  neibl  23737  blcld  23741  metss  23744  methaus  23756  met1stc  23757  met2ndci  23758  metrest  23760  prdsxmslem2  23765  metcnp3  23776  dscopn  23809  idnghm  23987  qdensere  24013  tgioo  24039  tgqioo  24043  zdis  24059  xrge0tsms  24077  cnheibor  24198  lmmbr  24502  bcthlem4  24571  ovolicc2lem5  24765  dyadmbllem  24843  i1fd  24925  itg11  24935  itg2gt0  25005  itgeq1f  25016  bddmulibl  25083  ellimc2  25121  limcnlp  25122  ellimc3  25123  limcflf  25125  limciun  25138  lhop1lem  25257  ig1pdvds  25421  plycpn  25529  aannenlem2  25569  efopn  25893  xrlimcnp  26198  wilthlem2  26298  wilthlem3  26299  nodenselem8  26919  tghilberti1  27131  colline  27143  lmif  27279  islmib  27281  incistruhgr  27582  upgr1eopALT  27620  uhgrvtxedgiedgb  27639  upgredg2vtx  27644  edglnl  27646  numedglnl  27647  uhgr2edg  27708  umgrvad2edg  27713  usgredg4  27717  usgredg2vtxeuALT  27722  uspgredg2vlem  27723  ushgredgedg  27729  nbgr1vtx  27858  nbusgredgeu0  27868  nbusgrf1o0  27869  nb3grprlem1  27880  nb3grprlem2  27881  uvtx01vtx  27897  nbupgruvtxres  27907  cplgr1vlem  27929  cplgr1v  27930  vtxd0nedgb  27988  vtxduhgr0nedg  27992  1loopgrvd2  28003  1egrvtxdg0  28011  uspgrloopvtxel  28016  vtxdginducedm1lem4  28042  wlk1walk  28139  wlkp1lem1  28173  pthdivtx  28229  0enwwlksnge1  28361  umgrwwlks2on  28454  rusgr0edg  28470  eleclclwwlkn  28572  upgr4cycl4dv4e  28681  1conngr  28690  vdn0conngrumgrv2  28692  eupth2eucrct  28713  eupth2lem1  28714  frgrncvvdeqlem7  28801  frgrncvvdeqlem9  28803  frgrwopregasn  28812  frgrwopregbsn  28813  l2p  28973  lpni  28974  issh  29702  pjoc1  29928  h1dn0  30046  spansneleqi  30063  nonbooli  30145  pjch  30188  pjnel  30220  cdjreui  30926  rexunirn  30972  rabsnel  30979  nelun  30991  iinabrex  31039  opabdm  31082  opabrn  31083  fpwrelmapffslem  31198  fpwrelmap  31199  fz1nntr  31256  xrge0tsmsd  31448  nsgqusf1olem3  31735  elrspunidl  31741  isprmidl  31748  reff  31925  tpr2rico  31998  lmxrge0  32038  indval  32117  issiga  32216  isrnsiga  32217  isldsys  32260  isros  32272  issros  32279  ddeval1  32338  ddeval0  32339  ismbfm  32355  isanmbfm  32359  dya2icoseg  32380  dya2iocnrect  32384  ballotlem7  32638  bnj216  32847  bnj563  32858  bnj956  32891  bnj545  33010  bnj548  33012  bnj570  33020  bnj900  33044  bnj929  33051  bnj964  33058  bnj983  33066  bnj1001  33074  bnj1145  33108  bnj1398  33149  bnj1498  33176  erdszelem1  33288  kur14lem9  33311  cnllysconn  33342  cvmsss2  33371  cvmcov2  33372  cvmsiota  33374  cvmopnlem  33375  cvmliftlem15  33395  satfv1  33460  satfdmlem  33465  mclsssvlem  33659  mclsind  33667  untelirr  33784  untsucf  33786  elintfv  33866  dfon2lem4  33889  dfon2lem7  33892  dfon2lem9  33894  noetasuplem4  34009  noetainflem4  34013  nocvxminlem  34042  lrrecfr  34170  dfiota3  34295  funpartlem  34314  funpartfun  34315  linethru  34525  hilbert1.1  34526  rankelg  34540  elhf2  34547  neibastop2lem  34619  bj-rabeqd  35176  bj-zfauscl  35181  bj-cleq  35220  bj-snsetex  35221  bj-clel3gALT  35298  bj-nuliota  35305  bj-isrvec  35542  mptsnunlem  35586  isbasisrelowllem1  35603  isbasisrelowllem2  35604  relowlssretop  35611  relowlpssretop  35612  exrecfnlem  35627  finxpeq1  35634  finxpreclem5  35643  finxpreclem6  35644  nlpineqsn  35656  fvineqsneu  35659  fvineqsneq  35660  pibt2  35665  unccur  35837  fin2so  35841  matunitlindflem1  35850  ptrecube  35854  poimirlem9  35863  poimirlem30  35884  poimir  35887  heicant  35889  mblfinlem1  35891  ftc1anc  35935  ftc2nc  35936  cover2  35949  isbnd2  36018  prdstotbnd  36029  heibor1lem  36044  grpokerinj  36128  rngoueqz  36175  isidl  36249  1idl  36261  0rngo  36262  ispridl  36269  smprngopr  36287  isfldidl  36303  isdmn3  36309  mpobi123f  36397  iineq12f  36399  mptbi12f  36401  eqvrelqsel  36855  n0eldmqseq  36888  dmqseqim2  36896  disjlem17  37038  lsateln0  37234  ispsubsp  37985  linepsubN  37992  elpcliN  38133  dvh3dim3N  39689  dochsnnz  39690  mapdindp3  39962  sn-iotalem  40419  prjspval  40663  prjcrv0  40691  elmzpcl  40769  diophren  40856  dford3lem2  41071  ttac  41080  pw2f1ocnv  41081  wepwsolem  41089  kelac1  41110  oacl2g  41270  nlimsuc  41287  intabssd  41365  elmapintrab  41423  eliunov2  41526  gneispaceel2  41993  mnuop23d  42123  mnuunid  42134  mnurndlem1  42138  expgrowthi  42190  dvconstbi  42191  tratrb  42395  suctrALT2VD  42695  suctrALT2  42696  en3lplem1VD  42702  en3lpVD  42704  tratrbVD  42720  suctrALTcf  42781  suctrALTcfVD  42782  suctrALT3  42783  unisnALT  42785  restuni3  42907  supminfxr  43258  xlimxrre  43627  xlimmnfvlem1  43628  xlimpnfvlem1  43632  icccncfext  43683  stoweidlem27  43823  stoweidlem35  43831  stoweidlem46  43842  stoweidlem52  43848  ioorrnopnlem  44100  ioorrnopnxrlem  44102  issal  44110  intsaluni  44123  salgencntex  44137  sge0f1o  44176  smfresal  44582  funressnfv  44807  fnbrafvb  44916  afvco2  44938  ndmaovg  44946  aovmpt4g  44963  fafv2elrnb  44997  fzoopth  45089  fvelsetpreimafv  45109  elsetpreimafvbi  45113  sprsymrelf1lem  45213  paireqne  45233  fpprbasnn  45451  nnsum4primeseven  45522  nnsum4primesevenALTV  45523  issubmgm  45613  c0snmgmhm  45742  c0snmhm  45743  rngccatidALTV  45817  ringccatidALTV  45880  ldepspr  46084  mosn  46428  indthinc  46603  indthincALT  46604