Theorem eleq2 2848

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840

This theorem is referenced by:  eleq12  2849  eleq2i  2851  nelneq2  2885  dvelimdc  2950  nelne1OLD  3059  raleqf  3331  rexeqf  3332  reueq1f  3333  rmoeq1f  3334  reueq1  3341  rmoeq1  3342  raleleq  3361  rabeqf  3398  rabeqi  3399  rabeq  3400  clel3g  3562  clel4  3564  sbcbi2OLD  3731  sbcel2gv  3740  csbeq2  3786  difeq2  3979  uneq1  4017  ineq1  4064  unineq  4136  n0i  4180  sbnfc2  4266  disjel  4283  elif  4386  exsnrex  4486  elinsn  4514  sneqrg  4638  preq1b  4645  preq12b  4649  elpreqprb  4666  elunii  4711  elinti  4752  intss1  4758  intmin  4763  intab  4773  iineq2  4805  dfiin2g  4821  breq  4925  zfrepclf  5050  zfauscl  5056  sseliALT  5064  inuni  5096  elALT  5184  rext  5190  intid  5200  elopg  5208  opth1  5217  opthwiener  5253  xpeq1  5414  xpeq2  5421  0nelelxp  5435  opthprc  5459  ordtri1  6056  ordtri3  6059  nsuceq0  6103  suctr  6106  ordnbtwn  6113  funopg  6216  dffv2  6578  fveqdmss  6665  dffo4  6686  funopdmsn  6729  fnsnb  6745  elunirn  6829  f1oiso  6921  canth  6928  eusvobj2  6963  mpoeq123  7038  ndmovg  7141  uniuni  7295  iunpw  7303  oneqmin  7330  onuninsuci  7365  nlimsucg  7367  limomss  7395  nnlim  7403  peano5  7414  unielxp  7532  cnvf1o  7607  smoel  7794  smo11  7798  tz7.44-2  7840  oawordeulem  7973  oaordex  7977  omordi  7985  oneo  8000  oeordi  8006  oeoa  8016  oeoe  8018  nnmordi  8050  nnaordex  8057  omabs  8066  nnneo  8070  omsmolem  8072  elqsn0  8158  qsel  8168  mapsnd  8240  undifixp  8287  boxriin  8293  boxcutc  8294  fineqvlem  8519  fineqv  8520  pssnn  8523  fissuni  8616  dffi2  8674  inficl  8676  dffi3  8682  wofib  8796  zfregcl  8845  en3lplem1  8861  en3lp  8863  suc11reg  8868  inf0  8870  inf3lem2  8878  inf3lem3  8879  infeq5i  8885  axinf2  8889  dfom3  8896  elom3  8897  cantnfle  8920  oemapvali  8933  cantnflem1  8938  tc2  8970  r1sdom  8989  rankwflemb  9008  rankval3b  9041  rankunb  9065  rankuni2b  9068  cardlim  9187  cardprclem  9194  infxpenlem  9225  alephnbtwn  9283  alephordi  9286  cardaleph  9301  alephfp  9320  alephval3  9322  dfac3  9333  dfac5lem2  9336  dfac5lem4  9338  dfac2b  9342  kmlem2  9363  coflim  9473  cfsmolem  9482  fin23lem30  9554  isf34lem4  9589  axdc2lem  9660  axdc3lem2  9663  axdc3lem4  9665  axdc4lem  9667  zorn2lem7  9714  axdclem  9731  brdom7disj  9743  brdom6disj  9744  axpowndlem3  9811  winainflem  9905  iswun  9916  eltskg  9962  inar1  9987  elgrug  10004  inaprc  10048  eltskm  10055  addnidpi  10113  indpi  10119  nqereu  10141  elnp  10199  elnpi  10200  genpnnp  10217  ltaddpr  10246  dfnn2  11446  dfnn3  11447  dfuzi  11879  uz11  12074  elfzonlteqm1  12921  om2uzlti  13126  axdc4uz  13160  hashrabsn1  13541  hashbclem  13613  hashf1lem2  13617  hash2prb  13631  hash2prd  13634  wrdsymb0  13702  lsw0  13718  swrdwrdsymb  13829  rtrclreclem3  14270  prodeq1f  15112  rpnnen2lem1  15417  rpnnen2lem2  15418  lcmfval  15811  lcmf0val  15812  ismre  16709  isacs  16770  initoid  17113  termoid  17114  initoeu2lem1  17122  clatl  17574  mreclatBAD  17645  issubm  17805  dfgrp2e  17907  cycsubg  18081  isnsg  18082  resghm  18135  ghmeql  18142  gsmsymgreq  18311  f1otrspeq  18326  pmtrval  18330  pmtrdifellem4  18358  pmtrprfval  18366  gsumzsplit  18790  pgpfac1lem1  18936  pgpfac1lem5  18941  pgpfac1  18942  issubrg  19248  lmodfopnelem2  19383  islss  19418  lspsneq0  19496  lmhmeql  19539  lspdisjb  19610  lidl1el  19702  lidldvgen  19739  0ring01eq  19755  mplcoe1  19949  mplcoe5  19952  islindf4  20674  m1detdiag  20900  mdetunilem9  20923  maducoeval2  20943  madugsum  20946  chpmat1dlem  21137  istopg  21197  toprntopon  21227  fiinbas  21254  topbas  21274  ppttop  21309  pptbas  21310  epttop  21311  elcls  21375  clsndisj  21377  iscldtop  21397  neiptopnei  21434  restbas  21460  restntr  21484  pnfnei  21522  mnfnei  21523  cnpimaex  21558  lmcvg  21564  iscnp4  21565  cncnpi  21580  cnconst2  21585  cnprest  21591  cnprest2  21592  cnpdis  21595  lmss  21600  lmff  21603  cnt0  21648  ist1-3  21651  cnhaus  21656  isreg2  21679  dishaus  21684  ordthauslem  21685  cmpsublem  21701  cmpsub  21702  cmpcld  21704  hauscmplem  21708  unconn  21731  conncompid  21733  conncompss  21735  1stcfb  21747  1stcrest  21755  2ndcctbss  21757  2ndcomap  21760  dis2ndc  21762  1stcelcls  21763  llyeq  21772  nllyeq  21773  restnlly  21784  islly2  21786  lly1stc  21798  dislly  21799  hauspwdom  21803  finlocfin  21822  unisngl  21829  dissnlocfin  21831  locfindis  21832  comppfsc  21834  llycmpkgen2  21852  txbas  21869  eltx  21870  ptpjopn  21914  ptclsg  21917  txcnp  21922  ptcnplem  21923  ptcnp  21924  txlly  21938  pthaus  21940  txtube  21942  txhaus  21949  txlm  21950  tx1stc  21952  txkgen  21954  xkohaus  21955  xkopt  21957  xkococnlem  21961  tgqtop  22014  kqfvima  22032  kqt0lem  22038  isr0  22039  regr1lem  22041  kqreglem1  22043  kqreglem2  22044  reghmph  22095  fbssfi  22139  isfil  22149  filuni  22187  isufil  22205  isufil2  22210  fixufil  22224  uffixfr  22225  uffixsn  22227  rnelfm  22255  flimopn  22277  flimrest  22285  flimcls  22287  txflf  22308  fclsopni  22317  fclsrest  22326  fclscf  22327  fcfnei  22337  alexsublem  22346  alexsubALTlem3  22351  alexsubALT  22353  tmdgsum2  22398  symgtgp  22403  subgntr  22408  opnsubg  22409  ghmcnp  22416  tgpt0  22420  qustgpopn  22421  tsmsi  22435  tsmssubm  22444  tsmssplit  22453  isust  22505  ustn0  22522  blssps  22727  blss  22728  blssexps  22729  blssex  22730  neibl  22804  blcld  22808  metss  22811  methaus  22823  met1stc  22824  met2ndci  22825  metrest  22827  prdsxmslem2  22832  metcnp3  22843  dscopn  22876  idnghm  23045  qdensere  23071  tgioo  23097  tgqioo  23101  zdis  23117  xrge0tsms  23135  cnheibor  23252  lmmbr  23554  bcthlem4  23623  ovolicc2lem5  23815  dyadmbllem  23893  i1fd  23975  itg11  23985  itg2gt0  24054  itgeq1f  24065  bddmulibl  24132  ellimc2  24168  limcnlp  24169  ellimc3  24170  limcflf  24172  limciun  24185  lhop1lem  24303  ig1pdvds  24463  plycpn  24571  aannenlem2  24611  efopn  24932  xrlimcnp  25238  wilthlem2  25338  wilthlem3  25339  tghilberti1  26115  colline  26127  lmif  26263  islmib  26265  incistruhgr  26557  upgr1eopALT  26595  uhgrvtxedgiedgb  26614  upgredg2vtx  26619  edglnl  26621  numedglnl  26622  uhgr2edg  26683  umgrvad2edg  26688  usgredg4  26692  usgredg2vtxeuALT  26697  uspgredg2vlem  26698  ushgredgedg  26704  nbgr1vtx  26833  nbusgredgeu0  26843  nbusgrf1o0  26844  nb3grprlem1  26855  nb3grprlem2  26856  uvtx01vtx  26872  nbupgruvtxres  26882  cplgr1vlem  26904  cplgr1v  26905  vtxd0nedgb  26963  vtxduhgr0nedg  26967  1loopgrvd2  26978  1egrvtxdg0  26986  uspgrloopvtxel  26991  vtxdginducedm1lem4  27017  wlk1walk  27113  wlkp1lem1  27151  pthdivtx  27208  0enwwlksnge1  27340  umgrwwlks2on  27453  rusgr0edg  27469  eleclclwwlkn  27590  upgr4cycl4dv4e  27704  1conngr  27713  vdn0conngrumgrv2  27715  eupth2eucrct  27737  eupth2lem1  27738  frgrncvvdeqlem7  27829  frgrncvvdeqlem9  27831  frgrwopregasn  27840  frgrwopregbsn  27841  l2p  28023  lpni  28024  issh  28754  pjoc1  28982  h1dn0  29100  spansneleqi  29117  nonbooli  29199  pjch  29242  pjnel  29274  cdjreui  29980  rexunirn  30027  rabsnel  30032  opabdm  30116  opabrn  30117  fpwrelmapffslem  30209  fpwrelmap  30210  fz1nntr  30263  xrge0tsmsd  30486  reff  30704  tpr2rico  30756  lmxrge0  30796  indval  30873  issiga  30972  isrnsigaOLD  30973  isrnsiga  30974  isldsys  31017  isros  31029  issros  31036  ddeval1  31095  ddeval0  31096  ismbfm  31112  isanmbfm  31116  dya2icoseg  31137  dya2iocnrect  31141  ballotlem7  31396  bnj216  31611  bnj563  31623  bnj956  31657  bnj545  31775  bnj548  31777  bnj570  31785  bnj900  31809  bnj929  31816  bnj964  31823  bnj983  31831  bnj1001  31838  bnj1145  31871  bnj1398  31912  bnj1498  31939  erdszelem1  31983  kur14lem9  32006  cnllysconn  32037  cvmsss2  32066  cvmcov2  32067  cvmsiota  32069  cvmopnlem  32070  cvmliftlem15  32090  mclsssvlem  32269  mclsind  32277  untelirr  32394  untsucf  32396  elintfv  32467  dfon2lem4  32491  dfon2lem7  32494  dfon2lem9  32496  soseq  32557  nodenselem8  32656  noetalem3  32680  nocvxminlem  32708  dfiota3  32845  funpartlem  32864  funpartfun  32865  linethru  33075  hilbert1.1  33076  rankelg  33090  elhf2  33097  neibastop2lem  33169  bj-rabeqd  33672  bj-zfauscl  33678  bj-cleq  33704  bj-sels  33727  bj-snsetex  33728  bj-nuliota  33796  mptsnunlem  33996  isbasisrelowllem1  34013  isbasisrelowllem2  34014  relowlssretop  34021  relowlpssretop  34022  exrecfnlem  34037  finxpeq1  34043  finxpreclem5  34052  finxpreclem6  34053  nlpineqsn  34065  fvineqsneu  34068  fvineqsneq  34069  pibt2  34074  unccur  34264  fin2so  34268  matunitlindflem1  34277  ptrecube  34281  poimirlem9  34290  poimirlem30  34311  poimir  34314  heicant  34316  mblfinlem1  34318  ftc1anc  34364  ftc2nc  34365  cover2  34379  isbnd2  34451  prdstotbnd  34462  heibor1lem  34477  grpokerinj  34561  rngoueqz  34608  isidl  34682  1idl  34694  0rngo  34695  ispridl  34702  smprngopr  34720  isfldidl  34736  isdmn3  34742  mpt2bi123f  34832  iineq12f  34834  mptbi12f  34836  nel02  34975  eqvrelqsel  35244  n0eldmqseq  35277  dmqseqim2  35284  lsateln0  35524  ispsubsp  36274  linepsubN  36281  elpcliN  36422  dvh3dim3N  37978  dochsnnz  37979  mapdindp3  38251  prjspval  38605  elmzpcl  38663  diophren  38751  dford3lem2  38965  ttac  38974  pw2f1ocnv  38975  wepwsolem  38983  kelac1  39004  elmapintrab  39243  intabssd  39277  eliunov2  39332  gneispaceel2  39802  mnuop23d  39922  mnuunid  39933  mnurndlem1  39937  ablsimpnosubgd  39985  expgrowthi  40025  dvconstbi  40026  tratrb  40233  suctrALT2VD  40533  suctrALT2  40534  en3lplem1VD  40540  en3lpVD  40542  tratrbVD  40558  suctrALTcf  40619  suctrALTcfVD  40620  suctrALT3  40621  unisnALT  40623  restuni3  40753  supminfxr  41117  xlimxrre  41489  xlimmnfvlem1  41490  xlimpnfvlem1  41494  icccncfext  41546  stoweidlem27  41689  stoweidlem35  41697  stoweidlem46  41708  stoweidlem52  41714  ioorrnopnlem  41966  ioorrnopnxrlem  41968  issal  41976  intsaluni  41989  salgencntex  42003  sge0f1o  42041  smfresal  42440  funressnfv  42629  fnbrafvb  42705  afvco2  42727  ndmaovg  42735  aovmpt4g  42752  fafv2elrnb  42786  fzoopth  42879  sprsymrelf1lem  42961  paireqne  42981  fpprbasnn  43202  nnsum4primeseven  43273  nnsum4primesevenALTV  43274  issubmgm  43364  c0snmgmhm  43489  c0snmhm  43490  rngccatidALTV  43564  ringccatidALTV  43627  ldepspr  43835