Theorem eleq2 2817

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eleq12  2818  eleq2i  2820  nelneq2  2853  dvelimdc  2916  raleqf  3326  rexeqfOLD  3328  rmoeq1OLD  3386  reueq1OLD  3387  rmoeq1f  3392  rabeq  3417  rabeqd  3431  rabeqf  3437  clel3g  3624  clel4g  3626  sbcbi2  3809  sbcel2gv  3817  csbeq2  3864  difeq2  4079  uneq1  4120  unineq  4247  nel02  4298  n0i  4299  sbnfc2  4398  disjel  4416  elif  4528  exsnrex  4640  elinsn  4670  sneqrg  4799  preq1b  4806  preq12b  4810  elpreqprb  4828  elunii  4872  elinti  4915  intss1  4923  intmin  4928  intab  4938  iuneqconst  4963  iineq2  4972  dfiun2g  4990  dfiin2g  4991  breq  5104  zfrepclf  5241  zfauscl  5248  sseliALT  5259  inuni  5300  selsALT  5394  rext  5403  intidg  5412  intidOLD  5413  elopg  5421  opth1  5430  opthwiener  5469  xpeq1  5645  xpeq2  5652  0nelelxp  5666  opthprc  5695  ordtri1  6353  ordtri3  6356  nsuceq0  6405  suctr  6408  ordnbtwn  6415  funopg  6534  dffv2  6938  fveqdmss  7032  dffo4  7057  funopdmsn  7104  fnsnbOLD  7122  elunirn  7207  f1oiso  7308  canth  7323  eusvobj2  7361  mpoeq123  7441  ndmovg  7552  uniuni  7718  iunpw  7727  oneqmin  7756  onuninsuci  7796  nlimsucg  7798  limomss  7827  nnlim  7836  peano5  7849  unielxp  7985  cnvf1o  8067  soseq  8115  smoel  8306  smo11  8310  tz7.44-2  8352  nlim2  8431  ord1eln01  8437  ord2eln012  8438  oawordeulem  8495  oaordex  8499  omordi  8507  oneo  8522  oeordi  8528  oeoa  8538  oeoe  8540  nnmordi  8572  nnaordex  8579  nnaordex2  8580  omabs  8592  nnneo  8596  omsmolem  8598  elqsn0  8734  qsel  8746  mapsnd  8836  undifixp  8884  boxriin  8890  boxcutc  8891  pssnn  9109  fineqvlem  9185  fineqv  9186  en1eqsn  9195  fissuni  9284  dffi2  9350  inficl  9352  dffi3  9358  wofib  9474  zfregcl  9523  en3lplem1  9541  en3lp  9543  suc11reg  9548  inf0  9550  inf3lem2  9558  inf3lem3  9559  infeq5i  9565  axinf2  9569  dfom3  9576  elom3  9577  cantnfle  9600  oemapvali  9613  cantnflem1  9618  tc2  9671  r1sdom  9703  rankwflemb  9722  rankval3b  9755  rankunb  9779  rankuni2b  9782  cardlim  9901  cardprclem  9908  infxpenlem  9942  alephnbtwn  10000  alephordi  10003  cardaleph  10018  alephfp  10037  alephval3  10039  dfac3  10050  dfac5lem2  10053  dfac5lem4  10055  dfac5lem4OLD  10057  dfac2b  10060  kmlem2  10081  coflim  10190  cfsmolem  10199  fin23lem30  10271  isf34lem4  10306  axdc2lem  10377  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  zorn2lem7  10431  axdclem  10448  brdom7disj  10460  brdom6disj  10461  axpowndlem3  10528  winainflem  10622  iswun  10633  eltskg  10679  inar1  10704  elgrug  10721  inaprc  10765  eltskm  10772  addnidpi  10830  indpi  10836  nqereu  10858  elnp  10916  elnpi  10917  genpnnp  10934  ltaddpr  10963  dfnn2  12175  dfnn3  12176  dfuzi  12601  uz11  12794  elfzonlteqm1  13678  fzoopth  13699  om2uzlti  13891  axdc4uz  13925  hashrabsn1  14315  hashbclem  14393  hashf1lem2  14397  hash2prb  14413  hash2prd  14416  hash3tpb  14436  wrdsymb0  14490  lsw0  14506  swrdwrdsymb  14603  rtrclreclem3  15002  prodeq1f  15848  prodeq1  15849  rpnnen2lem1  16158  rpnnen2lem2  16159  lcmfval  16567  lcmf0val  16568  ismre  17527  isacs  17588  initoid  17939  termoid  17940  initoeu2lem1  17952  clatl  18443  mreclatBAD  18498  issubmgm  18605  issubm  18706  dfgrp2e  18871  isnsg  19063  cycsubg  19116  resghm  19140  ghmeql  19147  gsmsymgreq  19338  f1otrspeq  19353  pmtrval  19357  pmtrdifellem4  19385  pmtrprfval  19393  gsumzsplit  19833  pgpfac1lem1  19982  pgpfac1lem5  19987  pgpfac1  19988  ablsimpnosubgd  20012  c0snmgmhm  20347  c0snmhm  20348  0ring01eq  20414  issubrg  20456  lmodfopnelem2  20781  islss  20816  lspsneq0  20894  lmhmeql  20938  lspdisjb  21012  lidl1el  21112  rngqiprngfulem2  21198  rngqipring1  21202  lidldvgen  21220  islindf4  21723  mplcoe1  21920  mplcoe5  21923  selvfval  21997  m1detdiag  22460  mdetunilem9  22483  maducoeval2  22503  madugsum  22506  chpmat1dlem  22698  istopg  22758  toprntopon  22788  fiinbas  22815  topbas  22835  ppttop  22870  pptbas  22871  epttop  22872  elcls  22936  clsndisj  22938  iscldtop  22958  neiptopnei  22995  restbas  23021  restntr  23045  pnfnei  23083  mnfnei  23084  cnpimaex  23119  lmcvg  23125  iscnp4  23126  cncnpi  23141  cnconst2  23146  cnprest  23152  cnprest2  23153  cnpdis  23156  lmss  23161  lmff  23164  cnt0  23209  ist1-3  23212  cnhaus  23217  isreg2  23240  dishaus  23245  ordthauslem  23246  cmpsublem  23262  cmpsub  23263  cmpcld  23265  hauscmplem  23269  unconn  23292  conncompid  23294  conncompss  23296  1stcfb  23308  1stcrest  23316  2ndcctbss  23318  2ndcomap  23321  dis2ndc  23323  1stcelcls  23324  llyeq  23333  nllyeq  23334  restnlly  23345  islly2  23347  lly1stc  23359  dislly  23360  hauspwdom  23364  finlocfin  23383  unisngl  23390  dissnlocfin  23392  locfindis  23393  comppfsc  23395  llycmpkgen2  23413  txbas  23430  eltx  23431  ptpjopn  23475  ptclsg  23478  txcnp  23483  ptcnplem  23484  ptcnp  23485  txlly  23499  pthaus  23501  txtube  23503  txhaus  23510  txlm  23511  tx1stc  23513  txkgen  23515  xkohaus  23516  xkopt  23518  xkococnlem  23522  tgqtop  23575  kqfvima  23593  kqt0lem  23599  isr0  23600  regr1lem  23602  kqreglem1  23604  kqreglem2  23605  reghmph  23656  fbssfi  23700  isfil  23710  filuni  23748  isufil  23766  isufil2  23771  fixufil  23785  uffixfr  23786  uffixsn  23788  rnelfm  23816  flimopn  23838  flimrest  23846  flimcls  23848  txflf  23869  fclsopni  23878  fclsrest  23887  fclscf  23888  fcfnei  23898  alexsublem  23907  alexsubALTlem3  23912  alexsubALT  23914  tmdgsum2  23959  symgtgp  23969  subgntr  23970  opnsubg  23971  ghmcnp  23978  tgpt0  23982  qustgpopn  23983  tsmsi  23997  tsmssubm  24006  tsmssplit  24015  isust  24067  ustn0  24084  blssps  24288  blss  24289  blssexps  24290  blssex  24291  neibl  24365  blcld  24369  metss  24372  methaus  24384  met1stc  24385  met2ndci  24386  metrest  24388  prdsxmslem2  24393  metcnp3  24404  dscopn  24437  idnghm  24607  qdensere  24633  tgioo  24660  tgqioo  24664  zdis  24681  xrge0tsms  24699  cnheibor  24830  lmmbr  25134  bcthlem4  25203  ovolicc2lem5  25398  dyadmbllem  25476  i1fd  25558  itg11  25568  itg2gt0  25637  itgeq1f  25648  itgeq1fOLD  25649  itgeq1  25650  bddmulibl  25716  ellimc2  25754  limcnlp  25755  ellimc3  25756  limcflf  25758  limciun  25771  lhop1lem  25894  ig1pdvds  26061  plycpn  26173  aannenlem2  26213  efopn  26543  xrlimcnp  26854  wilthlem2  26955  wilthlem3  26956  nodenselem8  27579  noetasuplem4  27624  noetainflem4  27628  nocvxminlem  27665  lrrecfr  27826  addsprop  27859  bdayon  28149  dfn0s2  28200  tghilberti1  28540  colline  28552  lmif  28688  islmib  28690  incistruhgr  28982  upgr1eopALT  29020  uhgrvtxedgiedgb  29039  upgredg2vtx  29044  edglnl  29046  numedglnl  29047  uhgr2edg  29111  umgrvad2edg  29116  usgredg4  29120  usgredg2vtxeuALT  29125  uspgredg2vlem  29126  ushgredgedg  29132  nbgr1vtx  29261  nbusgredgeu0  29271  nbusgrf1o0  29272  nb3grprlem1  29283  nb3grprlem2  29284  uvtx01vtx  29300  nbupgruvtxres  29310  cplgr1vlem  29332  cplgr1v  29333  vtxd0nedgb  29392  vtxduhgr0nedg  29396  1loopgrvd2  29407  1egrvtxdg0  29415  uspgrloopvtxel  29420  vtxdginducedm1lem4  29446  wlk1walk  29542  wlkp1lem1  29575  pthdivtx  29630  0enwwlksnge1  29767  umgrwwlks2on  29860  rusgr0edg  29876  eleclclwwlkn  29978  upgr4cycl4dv4e  30087  1conngr  30096  vdn0conngrumgrv2  30098  eupth2eucrct  30119  eupth2lem1  30120  frgrncvvdeqlem7  30207  frgrncvvdeqlem9  30209  frgrwopregasn  30218  frgrwopregbsn  30219  l2p  30381  lpni  30382  issh  31110  pjoc1  31336  h1dn0  31454  spansneleqi  31471  nonbooli  31553  pjch  31596  pjnel  31628  cdjreui  32334  rexunirn  32394  rabsnel  32402  nelun  32415  iinabrex  32471  opabdm  32512  opabrn  32513  fpwrelmapffslem  32628  fpwrelmap  32629  fz1nntr  32700  indval  32749  xrge0tsmsd  32975  nsgqusf1olem3  33359  elrspunidl  33372  isprmidl  33382  constrmon  33707  reff  33802  tpr2rico  33875  lmxrge0  33915  issiga  34075  isrnsiga  34076  isldsys  34119  isros  34131  issros  34138  ddeval1  34197  ddeval0  34198  ismbfm  34214  dya2icoseg  34241  dya2iocnrect  34245  ballotlem7  34500  bnj216  34695  bnj563  34706  bnj956  34739  bnj545  34858  bnj548  34860  bnj570  34868  bnj900  34892  bnj929  34899  bnj964  34906  bnj983  34914  bnj1001  34922  bnj1145  34956  bnj1398  34997  bnj1498  35024  wevgblacfn  35069  erdszelem1  35151  kur14lem9  35174  cnllysconn  35205  cvmsss2  35234  cvmcov2  35235  cvmsiota  35237  cvmopnlem  35238  cvmliftlem15  35258  satfv1  35323  satfdmlem  35328  mclsssvlem  35522  mclsind  35530  untelirr  35668  untsucf  35670  elintfv  35725  dfon2lem4  35747  dfon2lem7  35750  dfon2lem9  35752  dfiota3  35884  funpartlem  35903  funpartfun  35904  linethru  36114  hilbert1.1  36115  rankelg  36129  elhf2  36136  neibastop2lem  36321  bj-zfauscl  36885  bj-cleq  36923  bj-snsetex  36924  bj-clel3gALT  37009  bj-nuliota  37018  bj-isrvec  37255  mptsnunlem  37299  isbasisrelowllem1  37316  isbasisrelowllem2  37317  relowlssretop  37324  relowlpssretop  37325  exrecfnlem  37340  finxpeq1  37347  finxpreclem5  37356  finxpreclem6  37357  nlpineqsn  37369  fvineqsneq  37373  pibt2  37378  unccur  37570  fin2so  37574  matunitlindflem1  37583  ptrecube  37587  poimirlem9  37596  poimirlem30  37617  poimir  37620  heicant  37622  mblfinlem1  37624  ftc1anc  37668  ftc2nc  37669  cover2  37682  isbnd2  37750  prdstotbnd  37761  heibor1lem  37776  grpokerinj  37860  rngoueqz  37907  isidl  37981  1idl  37993  0rngo  37994  ispridl  38001  smprngopr  38019  isfldidl  38035  isdmn3  38041  mpobi123f  38129  iineq12f  38131  mptbi12f  38133  eqvrelqsel  38580  n0eldmqseq  38614  dmqseqim2  38622  disjlem17  38764  lsateln0  38961  ispsubsp  39712  linepsubN  39719  elpcliN  39860  dvh3dim3N  41416  dochsnnz  41417  mapdindp3  41689  sn-iotalem  42182  prjspval  42564  elmzpcl  42687  diophren  42774  dford3lem2  42989  ttac  42998  pw2f1ocnv  42999  wepwsolem  43004  kelac1  43025  onexgt  43202  onexlimgt  43205  ordnexbtwnsuc  43229  oaordnr  43258  omnord1  43267  nnoeomeqom  43274  oenord1  43278  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  omcl3g  43296  naddwordnexlem4  43363  nlimsuc  43403  intabssd  43481  elmapintrab  43538  eliunov2  43641  gneispaceel2  44106  mnuop23d  44228  mnuunid  44239  mnurndlem1  44243  expgrowthi  44295  dvconstbi  44296  tratrb  44499  suctrALT2VD  44798  suctrALT2  44799  en3lplem1VD  44805  en3lpVD  44807  tratrbVD  44823  suctrALTcf  44884  suctrALTcfVD  44885  suctrALT3  44886  unisnALT  44888  0elaxnul  44946  pwclaxpow  44947  prclaxpr  44948  uniclaxun  44949  omssaxinf2  44951  wfaxrep  44957  restuni3  45085  supminfxr  45433  xlimxrre  45802  xlimmnfvlem1  45803  xlimpnfvlem1  45807  icccncfext  45858  stoweidlem27  45998  stoweidlem35  46006  stoweidlem46  46017  stoweidlem52  46023  ioorrnopnlem  46275  ioorrnopnxrlem  46277  issal  46285  intsaluni  46300  salgencntex  46314  smfresal  46759  tannpoly  46864  funressnfv  47017  fnbrafvb  47128  afvco2  47150  ndmaovg  47158  aovmpt4g  47175  fafv2elrnb  47209  fvelsetpreimafv  47361  elsetpreimafvbi  47365  sprsymrelf1lem  47465  paireqne  47485  fpprbasnn  47703  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  dfclnbgr6  47829  dfsclnbgr6  47831  grtri  47912  stgrvtx0  47934  stgrnbgr0  47936  isubgr3stgrlem3  47940  gpgvtx0  48017  gpgvtx1  48018  gpg3kgrtriex  48053  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087  rngccatidALTV  48233  ringccatidALTV  48267  ldepspr  48435  mosn  48774  indthinc  49424  indthincALT  49425