Theorem eleq2 2849

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eleq2d 2846	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  eleq12  2850  eleq2i  2852  nelneq2  2885  dvelimdc  2946  raleqf  3341  rmoeq1f  3402  rabeq  3426  rabeqd  3439  rabeqf  3445  clel3g  3615  clel4g  3617  sbcel2gv  3805  csbeq2  3852  difeq2  4068  uneq1  4108  unineq  4234  nel02  4285  sbnfc2  4397  disjel  4410  elif  4526  exsnrex  4641  elinsn  4671  sneqrg  4799  preq1b  4806  preq12b  4810  elpreqprb  4828  elunii  4872  elinti  4916  intss1  4923  intmin  4928  intab  4938  iuneqconst  4963  iineq2  4972  dfiun2g  4988  breq  5105  zfrepclf  5246  sepg  5253  zfausclOLD  5255  sseliALT  5266  vneqv  5273  inuni  5314  selsALT  5416  rext  5423  intidg  5432  elopg  5442  opth1  5451  opthwiener  5491  xpeq1  5669  xpeq2  5676  0nelelxp  5690  opthprc  5719  ordtri1  6391  ordtri3  6394  nsuceq0  6443  suctr  6446  ordnbtwn  6453  funopg  6568  dffv2  6974  fveqdmss  7072  dffo4  7097  funopdmsn  7148  fnsnbOLD  7165  elunirn  7249  f1oiso  7353  canth  7368  eusvobj2  7406  mpoeq123  7486  ndmovg  7598  uniuni  7762  iunpw  7771  oneqmin  7800  onuninsuci  7837  nlimsucg  7839  limomss  7868  nnlim  7877  peano5  7891  unielxp  8025  cnvf1o  8109  soseq  8158  smoel  8350  smo11  8354  tz7.44-2  8397  nlim2  8480  ord1eln01  8486  ord2eln012  8487  oawordeulem  8544  oaordex  8548  omordi  8556  oneo  8571  oeordi  8578  oeoa  8588  oeoe  8590  nnmordi  8622  nnaordex  8629  nnaordex2  8630  omabs  8642  nnneo  8646  omsmolem  8648  elqsn0  8787  qsel  8799  mapsnd  8896  undifixp  8944  boxriin  8950  boxcutc  8951  pssnn  9166  fineqvlem  9239  fineqv  9240  en1eqsn  9248  fissuni  9327  dffi2  9396  inficl  9398  dffi3  9404  wofib  9520  zfregcl  9569  zfregclOLD  9570  nelaneq  9577  nelaneqOLD  9578  en3lplem1  9594  en3lp  9596  suc11reg  9601  inf0  9603  inf3lem2  9611  inf3lem3  9612  infeq5i  9618  axinf2  9622  dfom3  9629  elom3  9630  cantnfle  9653  oemapvali  9666  cantnflem1  9671  tc2  9722  r1sdom  9759  rankwflemb  9778  rankval3b  9811  rankunb  9835  rankuni2b  9838  karden  9901  cardlim  9980  cardprclem  9987  infxpenlem  10019  alephnbtwn  10077  alephordi  10080  cardaleph  10095  alephfp  10114  alephval3  10116  dfac3  10127  dfac5lem2  10130  dfac5lem4  10132  dfac2b  10136  kmlem2  10157  coflim  10266  cfsmolem  10275  fin23lem30  10347  isf34lem4  10382  axdc2lem  10453  axdc3lem2  10456  axdc3lem4  10458  axdc4lem  10460  zorn2lem7  10507  axdclem  10524  brdom7disj  10537  brdom6disj  10538  axpowndlem3  10611  winainflem  10705  iswun  10716  eltskg  10762  inar1  10787  elgrug  10804  inaprc  10848  eltskm  10855  addnidpi  10913  indpi  10919  nqereu  10941  elnp  10999  elnpi  11000  genpnnp  11017  ltaddpr  11046  indval  12248  dfnn2  12273  dfnn3  12274  dfuzi  12715  uz11  12915  elfzonlteqm1  13800  fzoopth  13821  om2uzlti  14017  axdc4uz  14051  hashrabsn1  14441  hashbclem  14520  hashf1lem2  14524  hash2prb  14540  hash2prd  14543  hash3tpb  14563  wrdsymb0  14617  lsw0  14633  swrdwrdsymb  14735  rtrclreclem3  15136  prodeq1f  15998  prodeq1  15999  rpnnen2lem1  16305  rpnnen2lem2  16306  lcmfval  16714  lcmf0val  16715  ismre  17677  isacs  17742  initoid  18093  termoid  18094  initoeu2lem1  18106  clatl  18599  mreclatBAD  18654  issubmgm  18807  issubm  18914  dfgrp2e  19090  isnsg  19281  cycsubg  19339  resghm  19362  ghmeql  19369  gsmsymgreq  19562  f1otrspeq  19577  pmtrval  19581  pmtrdifellem4  19609  pmtrprfval  19617  gsumzsplit  20057  pgpfac1lem1  20206  pgpfac1lem5  20211  pgpfac1  20212  ablsimpnosubgd  20236  c0snmgmhm  20606  c0snmhm  20607  0ring01eq  20693  issubrg  20736  lmodfopnelem2  21086  islss  21121  lspsneq0  21199  lmhmeql  21242  lspdisjb  21316  lidl1el  21417  rngqiprngfulem2  21518  rngqipring1  21522  isprmidl  21529  lidldvgen  21568  islindf4  22054  mplcoe1  22256  mplcoe5  22259  selvfval  22338  m1detdiag  22822  mdetunilem9  22845  maducoeval2  22865  madugsum  22868  matunitlindflem1  22904  chpmat1dlem  23063  istopg  23123  toprntopon  23153  fiinbas  23180  topbas  23200  ppttop  23235  pptbas  23236  epttop  23237  elcls  23301  clsndisj  23303  iscldtop  23323  neiptopnei  23360  restbas  23386  restntr  23410  pnfnei  23448  mnfnei  23449  cnpimaex  23484  lmcvg  23490  iscnp4  23491  cncnpi  23506  cnconst2  23511  cnprest  23517  cnprest2  23518  cnpdis  23521  lmss  23526  lmff  23529  cnt0  23574  ist1-3  23577  cnhaus  23582  isreg2  23605  dishaus  23610  ordthauslem  23611  cmpsublem  23627  cmpsub  23628  cmpcld  23630  hauscmplem  23634  unconn  23657  conncompid  23659  conncompss  23661  1stcfb  23673  1stcrest  23681  2ndcctbss  23684  2ndcomap  23687  dis2ndc  23689  1stcelcls  23690  llyeq  23699  nllyeq  23700  restnlly  23711  islly2  23713  lly1stc  23725  dislly  23726  hauspwdom  23730  finlocfin  23749  unisngl  23756  dissnlocfin  23758  locfindis  23759  comppfsc  23761  llycmpkgen2  23779  txbas  23796  eltx  23797  ptpjopn  23841  ptclsg  23844  txcnp  23849  ptcnplem  23850  ptcnp  23851  txlly  23865  pthaus  23867  txtube  23869  txhaus  23876  txlm  23877  tx1stc  23879  txkgen  23881  xkohaus  23882  xkopt  23884  xkococnlem  23888  tgqtop  23941  kqfvima  23959  kqt0lem  23965  isr0  23966  regr1lem  23968  kqreglem1  23970  kqreglem2  23971  reghmph  24022  fbssfi  24066  isfil  24076  filuni  24114  isufil  24132  isufil2  24137  fixufil  24151  uffixfr  24152  uffixsn  24154  rnelfm  24182  flimopn  24204  flimrest  24212  flimcls  24214  txflf  24235  fclsopni  24244  fclsrest  24253  fclscf  24254  fcfnei  24264  alexsublem  24273  alexsubALTlem3  24278  alexsubALT  24280  tmdgsum2  24325  symgtgp  24335  subgntr  24336  opnsubg  24337  ghmcnp  24344  tgpt0  24348  qustgpopn  24349  tsmsi  24363  tsmssubm  24372  tsmssplit  24381  isust  24433  ustn0  24450  blssps  24653  blss  24654  blssexps  24655  blssex  24656  neibl  24730  blcld  24734  metss  24737  methaus  24749  met1stc  24750  met2ndci  24751  metrest  24753  prdsxmslem2  24758  metcnp3  24769  dscopn  24802  idnghm  24972  qdensere  24998  tgioo  25025  tgqioo  25029  zdis  25046  xrge0tsms  25064  cnheibor  25186  lmmbr  25489  bcthlem4  25558  ovolicc2lem5  25752  dyadmbllem  25830  i1fd  25912  itg11  25922  itg2gt0  25991  itgeq1f  26002  itgeq1  26003  bddmulibl  26069  ellimc2  26107  limcnlp  26108  ellimc3  26109  limcflf  26111  limciun  26124  lhop1lem  26243  ig1pdvds  26408  plycpn  26522  aannenlem2  26568  efopn  26898  xrlimcnp  27208  wilthlem2  27308  wilthlem3  27309  nodenselem8  27930  noetasuplem4  27975  noetainflem4  27979  nocvxminlem  28022  lrrecfr  28211  addsprop  28244  bdayons  28544  addonbday  28547  dfn0s2  28600  tghilberti1  28987  colline  29000  lmif  29172  islmib  29174  prlngex  29311  prlngeq  29317  incistruhgr  29539  upgr1eopALT  29577  uhgrvtxedgiedgb  29596  upgredg2vtx  29601  edglnl  29603  numedglnl  29604  uhgr2edg  29671  umgrvad2edg  29676  usgredg4  29680  usgredg2vtxeuALT  29685  uspgredg2vlem  29686  ushgredgedg  29692  nbgr1vtx  29821  nbusgredgeu0  29831  nbusgrf1o0  29832  nb3grprlem1  29843  nb3grprlem2  29844  uvtx01vtx  29860  nbupgruvtxres  29870  cplgr1vlem  29892  cplgr1v  29893  vtxd0nedgb  29951  vtxduhgr0nedg  29955  1loopgrvd2  29966  1egrvtxdg0  29974  uspgrloopvtxel  29979  vtxdginducedm1lem4  30005  wlk1walk  30101  wlkp1lem1  30134  pthdivtx  30194  0enwwlksnge1  30335  usgrwwlks2on  30429  umgrwwlks2on  30430  rusgr0edg  30447  eleclclwwlkn  30549  upgr4cycl4dv4e  30668  1conngr  30677  vdn0conngrumgrv2  30679  eupth2eucrct  30700  eupth2lem1  30701  frgrncvvdeqlem7  30788  frgrncvvdeqlem9  30790  frgrwopregasn  30799  frgrwopregbsn  30800  l2p  30963  lpni  30964  issh  31692  pjoc1  31918  h1dn0  32036  spansneleqi  32053  nonbooli  32135  pjch  32178  pjnel  32210  cdjreui  32916  rexunirn  32970  rabsnel  32978  nelun  32991  iinabrex  33045  opabdm  33087  opabrn  33088  fpwrelmapffslem  33206  fpwrelmap  33207  fz1nntr  33276  xrge0tsmsd  33516  nsgqusf1olem3  33847  elrspunidl  33859  constrmon  34257  reff  34352  tpr2rico  34425  lmxrge0  34465  issiga  34625  isrnsiga  34626  isldsys  34670  isros  34682  issros  34689  ddeval1  34748  ddeval0  34749  ismbfm  34765  dya2icoseg  34791  dya2iocnrect  34795  ballotlem7  35050  bnj216  35245  bnj563  35256  bnj956  35289  bnj545  35407  bnj548  35409  bnj570  35417  bnj900  35441  bnj929  35448  bnj964  35455  bnj983  35463  bnj1001  35471  bnj1145  35505  bnj1398  35546  bnj1498  35573  fineqvnttrclselem2  35651  fineqvnttrclse  35653  fineqvinfep  35654  wevgblacfn  35711  erdszelem1  35773  kur14lem9  35796  cnllysconn  35827  cvmsss2  35856  cvmcov2  35857  cvmsiota  35859  cvmopnlem  35860  cvmliftlem15  35880  satfv1  35945  satfdmlem  35950  mclsssvlem  36144  mclsind  36152  untelirr  36290  untsucf  36292  elintfv  36347  dfon2lem4  36366  dfon2lem7  36369  dfon2lem9  36371  dfiota3  36503  funpartlem  36524  funpartfun  36525  linethru  36736  hilbert1.1  36737  rankelg  36751  elhf2  36758  ltnadd  36801  neibastop2lem  36982  regsfromregtco  37160  regsfromunir1  37162  bj-sepg  37670  bj-cleq  37709  bj-snsetex  37710  bj-clel3gALT  37795  bj-nuliota  37804  bj-isrvec  38049  mptsnunlem  38095  isbasisrelowllem1  38112  isbasisrelowllem2  38113  relowlssretop  38120  relowlpssretop  38121  exrecfnlem  38136  finxpeq1  38143  finxpreclem5  38152  finxpreclem6  38153  nlpineqsn  38165  fvineqsneq  38169  pibt2  38174  unccur  38360  fin2so  38364  ptrecube  38372  poimirlem9  38381  poimirlem30  38402  poimir  38405  heicant  38407  mblfinlem1  38409  ftc1anc  38453  ftc2nc  38454  cover2  38468  isbnd2  38536  prdstotbnd  38547  heibor1lem  38562  grpokerinj  38646  rngoueqz  38693  isidl  38767  1idl  38779  0rngo  38780  ispridl  38787  smprngopr  38805  isfldidl  38821  isdmn3  38827  mpobi123f  38913  iineq12f  38915  mptbi12f  38917  dfsuccl4  39225  eqvrelqsel  39451  n0eldmqseq  39485  dmqseqim2  39493  suceldisj  39569  disjlem17  39653  lsateln0  39871  ispsubsp  40621  linepsubN  40628  elpcliN  40769  dvh3dim3N  42325  dochsnnz  42326  mapdindp3  42598  sn-iotalem  43094  prjspval  43452  elmzpcl  43574  diophren  43657  dford3lem2  43871  ttac  43880  pw2f1ocnv  43881  wepwsolem  43886  kelac1  43907  onexgt  44084  onexlimgt  44087  ordnexbtwnsuc  44111  oaordnr  44140  omnord1  44149  nnoeomeqom  44156  oenord1  44160  succlg  44172  oacl2g  44174  omabs2  44176  omcl2  44177  omcl3g  44178  naddwordnexlem4  44245  nlimsuc  44284  intabssd  44362  elmapintrab  44419  eliunov2  44522  gneispaceel2  44987  mnuop23d  45093  mnuunid  45104  mnurndlem1  45108  expgrowthi  45160  dvconstbi  45161  tratrb  45362  suctrALT2VD  45661  suctrALT2  45662  en3lplem1VD  45668  en3lpVD  45670  tratrbVD  45686  suctrALTcf  45747  suctrALTcfVD  45748  suctrALT3  45749  unisnALT  45751  0elaxnul  45809  pwclaxpow  45810  prclaxpr  45811  uniclaxun  45812  omssaxinf2  45814  wfaxrep  45820  restuni3  45953  supminfxr  46295  xlimxrre  46662  xlimmnfvlem1  46663  xlimpnfvlem1  46667  icccncfext  46718  stoweidlem27  46858  stoweidlem35  46866  stoweidlem46  46877  stoweidlem52  46883  ioorrnopnlem  47135  ioorrnopnxrlem  47137  issal  47145  intsaluni  47160  salgencntex  47174  smfresal  47619  tannpoly  47761  funressnfv  47934  fnbrafvb  48045  afvco2  48067  ndmaovg  48075  aovmpt4g  48092  fafv2elrnb  48126  fvelsetpreimafv  48290  elsetpreimafvbi  48294  sprsymrelf1lem  48394  paireqne  48414  fpprbasnn  48648  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  dfclnbgr6  48775  dfsclnbgr6  48777  grtri  48859  stgrvtx0  48881  stgrnbgr0  48883  isubgr3stgrlem3  48887  gpgvtx0  48972  gpgvtx1  48973  gpg3kgrtriex  49008  pgnbgreunbgrlem3  49037  pgnbgreunbgrlem6  49043  rngccatidALTV  49190  ringccatidALTV  49224  prmringnzring  49255  isidom3  49263  ldepspr  49406  mosn  49744  indthinc  50391  indthincALT  50392