Theorem eleq2 2818

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 2815	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 2702

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

This theorem is referenced by:  eleq12  2819  eleq2i  2821  nelneq2  2854  dvelimdc  2917  raleqf  3331  rexeqfOLD  3333  rmoeq1OLD  3392  reueq1OLD  3393  rmoeq1f  3398  rabeq  3423  rabeqd  3437  rabeqf  3443  clel3g  3630  clel4g  3632  sbcbi2  3815  sbcel2gv  3823  csbeq2  3870  difeq2  4086  uneq1  4127  unineq  4254  nel02  4305  n0i  4306  sbnfc2  4405  disjel  4423  elif  4535  exsnrex  4647  elinsn  4677  sneqrg  4806  preq1b  4813  preq12b  4817  elpreqprb  4835  elunii  4879  elinti  4922  intss1  4930  intmin  4935  intab  4945  iuneqconst  4970  iineq2  4979  dfiun2g  4997  dfiin2g  4999  breq  5112  zfrepclf  5249  zfauscl  5256  sseliALT  5267  inuni  5308  selsALT  5402  rext  5411  intidg  5420  intidOLD  5421  elopg  5429  opth1  5438  opthwiener  5477  xpeq1  5655  xpeq2  5662  0nelelxp  5676  opthprc  5705  ordtri1  6368  ordtri3  6371  nsuceq0  6420  suctr  6423  ordnbtwn  6430  funopg  6553  dffv2  6959  fveqdmss  7053  dffo4  7078  funopdmsn  7125  fnsnbOLD  7143  elunirn  7228  f1oiso  7329  canth  7344  eusvobj2  7382  mpoeq123  7464  ndmovg  7575  uniuni  7741  iunpw  7750  oneqmin  7779  onuninsuci  7819  nlimsucg  7821  limomss  7850  nnlim  7859  peano5  7872  unielxp  8009  cnvf1o  8093  soseq  8141  smoel  8332  smo11  8336  tz7.44-2  8378  nlim2  8457  ord1eln01  8463  ord2eln012  8464  oawordeulem  8521  oaordex  8525  omordi  8533  oneo  8548  oeordi  8554  oeoa  8564  oeoe  8566  nnmordi  8598  nnaordex  8605  nnaordex2  8606  omabs  8618  nnneo  8622  omsmolem  8624  elqsn0  8760  qsel  8772  mapsnd  8862  undifixp  8910  boxriin  8916  boxcutc  8917  pssnn  9138  fineqvlem  9216  fineqv  9217  en1eqsn  9226  fissuni  9315  dffi2  9381  inficl  9383  dffi3  9389  wofib  9505  zfregcl  9554  en3lplem1  9572  en3lp  9574  suc11reg  9579  inf0  9581  inf3lem2  9589  inf3lem3  9590  infeq5i  9596  axinf2  9600  dfom3  9607  elom3  9608  cantnfle  9631  oemapvali  9644  cantnflem1  9649  tc2  9702  r1sdom  9734  rankwflemb  9753  rankval3b  9786  rankunb  9810  rankuni2b  9813  cardlim  9932  cardprclem  9939  infxpenlem  9973  alephnbtwn  10031  alephordi  10034  cardaleph  10049  alephfp  10068  alephval3  10070  dfac3  10081  dfac5lem2  10084  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2b  10091  kmlem2  10112  coflim  10221  cfsmolem  10230  fin23lem30  10302  isf34lem4  10337  axdc2lem  10408  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  zorn2lem7  10462  axdclem  10479  brdom7disj  10491  brdom6disj  10492  axpowndlem3  10559  winainflem  10653  iswun  10664  eltskg  10710  inar1  10735  elgrug  10752  inaprc  10796  eltskm  10803  addnidpi  10861  indpi  10867  nqereu  10889  elnp  10947  elnpi  10948  genpnnp  10965  ltaddpr  10994  dfnn2  12206  dfnn3  12207  dfuzi  12632  uz11  12825  elfzonlteqm1  13709  fzoopth  13730  om2uzlti  13922  axdc4uz  13956  hashrabsn1  14346  hashbclem  14424  hashf1lem2  14428  hash2prb  14444  hash2prd  14447  hash3tpb  14467  wrdsymb0  14521  lsw0  14537  swrdwrdsymb  14634  rtrclreclem3  15033  prodeq1f  15879  prodeq1  15880  rpnnen2lem1  16189  rpnnen2lem2  16190  lcmfval  16598  lcmf0val  16599  ismre  17558  isacs  17619  initoid  17970  termoid  17971  initoeu2lem1  17983  clatl  18474  mreclatBAD  18529  issubmgm  18636  issubm  18737  dfgrp2e  18902  isnsg  19094  cycsubg  19147  resghm  19171  ghmeql  19178  gsmsymgreq  19369  f1otrspeq  19384  pmtrval  19388  pmtrdifellem4  19416  pmtrprfval  19424  gsumzsplit  19864  pgpfac1lem1  20013  pgpfac1lem5  20018  pgpfac1  20019  ablsimpnosubgd  20043  c0snmgmhm  20378  c0snmhm  20379  0ring01eq  20445  issubrg  20487  lmodfopnelem2  20812  islss  20847  lspsneq0  20925  lmhmeql  20969  lspdisjb  21043  lidl1el  21143  rngqiprngfulem2  21229  rngqipring1  21233  lidldvgen  21251  islindf4  21754  mplcoe1  21951  mplcoe5  21954  selvfval  22028  m1detdiag  22491  mdetunilem9  22514  maducoeval2  22534  madugsum  22537  chpmat1dlem  22729  istopg  22789  toprntopon  22819  fiinbas  22846  topbas  22866  ppttop  22901  pptbas  22902  epttop  22903  elcls  22967  clsndisj  22969  iscldtop  22989  neiptopnei  23026  restbas  23052  restntr  23076  pnfnei  23114  mnfnei  23115  cnpimaex  23150  lmcvg  23156  iscnp4  23157  cncnpi  23172  cnconst2  23177  cnprest  23183  cnprest2  23184  cnpdis  23187  lmss  23192  lmff  23195  cnt0  23240  ist1-3  23243  cnhaus  23248  isreg2  23271  dishaus  23276  ordthauslem  23277  cmpsublem  23293  cmpsub  23294  cmpcld  23296  hauscmplem  23300  unconn  23323  conncompid  23325  conncompss  23327  1stcfb  23339  1stcrest  23347  2ndcctbss  23349  2ndcomap  23352  dis2ndc  23354  1stcelcls  23355  llyeq  23364  nllyeq  23365  restnlly  23376  islly2  23378  lly1stc  23390  dislly  23391  hauspwdom  23395  finlocfin  23414  unisngl  23421  dissnlocfin  23423  locfindis  23424  comppfsc  23426  llycmpkgen2  23444  txbas  23461  eltx  23462  ptpjopn  23506  ptclsg  23509  txcnp  23514  ptcnplem  23515  ptcnp  23516  txlly  23530  pthaus  23532  txtube  23534  txhaus  23541  txlm  23542  tx1stc  23544  txkgen  23546  xkohaus  23547  xkopt  23549  xkococnlem  23553  tgqtop  23606  kqfvima  23624  kqt0lem  23630  isr0  23631  regr1lem  23633  kqreglem1  23635  kqreglem2  23636  reghmph  23687  fbssfi  23731  isfil  23741  filuni  23779  isufil  23797  isufil2  23802  fixufil  23816  uffixfr  23817  uffixsn  23819  rnelfm  23847  flimopn  23869  flimrest  23877  flimcls  23879  txflf  23900  fclsopni  23909  fclsrest  23918  fclscf  23919  fcfnei  23929  alexsublem  23938  alexsubALTlem3  23943  alexsubALT  23945  tmdgsum2  23990  symgtgp  24000  subgntr  24001  opnsubg  24002  ghmcnp  24009  tgpt0  24013  qustgpopn  24014  tsmsi  24028  tsmssubm  24037  tsmssplit  24046  isust  24098  ustn0  24115  blssps  24319  blss  24320  blssexps  24321  blssex  24322  neibl  24396  blcld  24400  metss  24403  methaus  24415  met1stc  24416  met2ndci  24417  metrest  24419  prdsxmslem2  24424  metcnp3  24435  dscopn  24468  idnghm  24638  qdensere  24664  tgioo  24691  tgqioo  24695  zdis  24712  xrge0tsms  24730  cnheibor  24861  lmmbr  25165  bcthlem4  25234  ovolicc2lem5  25429  dyadmbllem  25507  i1fd  25589  itg11  25599  itg2gt0  25668  itgeq1f  25679  itgeq1fOLD  25680  itgeq1  25681  bddmulibl  25747  ellimc2  25785  limcnlp  25786  ellimc3  25787  limcflf  25789  limciun  25802  lhop1lem  25925  ig1pdvds  26092  plycpn  26204  aannenlem2  26244  efopn  26574  xrlimcnp  26885  wilthlem2  26986  wilthlem3  26987  nodenselem8  27610  noetasuplem4  27655  noetainflem4  27659  nocvxminlem  27696  lrrecfr  27857  addsprop  27890  bdayon  28180  dfn0s2  28231  tghilberti1  28571  colline  28583  lmif  28719  islmib  28721  incistruhgr  29013  upgr1eopALT  29051  uhgrvtxedgiedgb  29070  upgredg2vtx  29075  edglnl  29077  numedglnl  29078  uhgr2edg  29142  umgrvad2edg  29147  usgredg4  29151  usgredg2vtxeuALT  29156  uspgredg2vlem  29157  ushgredgedg  29163  nbgr1vtx  29292  nbusgredgeu0  29302  nbusgrf1o0  29303  nb3grprlem1  29314  nb3grprlem2  29315  uvtx01vtx  29331  nbupgruvtxres  29341  cplgr1vlem  29363  cplgr1v  29364  vtxd0nedgb  29423  vtxduhgr0nedg  29427  1loopgrvd2  29438  1egrvtxdg0  29446  uspgrloopvtxel  29451  vtxdginducedm1lem4  29477  wlk1walk  29574  wlkp1lem1  29608  pthdivtx  29664  0enwwlksnge1  29801  umgrwwlks2on  29894  rusgr0edg  29910  eleclclwwlkn  30012  upgr4cycl4dv4e  30121  1conngr  30130  vdn0conngrumgrv2  30132  eupth2eucrct  30153  eupth2lem1  30154  frgrncvvdeqlem7  30241  frgrncvvdeqlem9  30243  frgrwopregasn  30252  frgrwopregbsn  30253  l2p  30415  lpni  30416  issh  31144  pjoc1  31370  h1dn0  31488  spansneleqi  31505  nonbooli  31587  pjch  31630  pjnel  31662  cdjreui  32368  rexunirn  32428  rabsnel  32436  nelun  32449  iinabrex  32505  opabdm  32546  opabrn  32547  fpwrelmapffslem  32662  fpwrelmap  32663  fz1nntr  32734  indval  32783  xrge0tsmsd  33009  nsgqusf1olem3  33393  elrspunidl  33406  isprmidl  33416  constrmon  33741  reff  33836  tpr2rico  33909  lmxrge0  33949  issiga  34109  isrnsiga  34110  isldsys  34153  isros  34165  issros  34172  ddeval1  34231  ddeval0  34232  ismbfm  34248  dya2icoseg  34275  dya2iocnrect  34279  ballotlem7  34534  bnj216  34729  bnj563  34740  bnj956  34773  bnj545  34892  bnj548  34894  bnj570  34902  bnj900  34926  bnj929  34933  bnj964  34940  bnj983  34948  bnj1001  34956  bnj1145  34990  bnj1398  35031  bnj1498  35058  wevgblacfn  35103  erdszelem1  35185  kur14lem9  35208  cnllysconn  35239  cvmsss2  35268  cvmcov2  35269  cvmsiota  35271  cvmopnlem  35272  cvmliftlem15  35292  satfv1  35357  satfdmlem  35362  mclsssvlem  35556  mclsind  35564  untelirr  35702  untsucf  35704  elintfv  35759  dfon2lem4  35781  dfon2lem7  35784  dfon2lem9  35786  dfiota3  35918  funpartlem  35937  funpartfun  35938  linethru  36148  hilbert1.1  36149  rankelg  36163  elhf2  36170  neibastop2lem  36355  bj-zfauscl  36919  bj-cleq  36957  bj-snsetex  36958  bj-clel3gALT  37043  bj-nuliota  37052  bj-isrvec  37289  mptsnunlem  37333  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  relowlpssretop  37359  exrecfnlem  37374  finxpeq1  37381  finxpreclem5  37390  finxpreclem6  37391  nlpineqsn  37403  fvineqsneq  37407  pibt2  37412  unccur  37604  fin2so  37608  matunitlindflem1  37617  ptrecube  37621  poimirlem9  37630  poimirlem30  37651  poimir  37654  heicant  37656  mblfinlem1  37658  ftc1anc  37702  ftc2nc  37703  cover2  37716  isbnd2  37784  prdstotbnd  37795  heibor1lem  37810  grpokerinj  37894  rngoueqz  37941  isidl  38015  1idl  38027  0rngo  38028  ispridl  38035  smprngopr  38053  isfldidl  38069  isdmn3  38075  mpobi123f  38163  iineq12f  38165  mptbi12f  38167  eqvrelqsel  38614  n0eldmqseq  38648  dmqseqim2  38656  disjlem17  38798  lsateln0  38995  ispsubsp  39746  linepsubN  39753  elpcliN  39894  dvh3dim3N  41450  dochsnnz  41451  mapdindp3  41723  sn-iotalem  42216  prjspval  42598  elmzpcl  42721  diophren  42808  dford3lem2  43023  ttac  43032  pw2f1ocnv  43033  wepwsolem  43038  kelac1  43059  onexgt  43236  onexlimgt  43239  ordnexbtwnsuc  43263  oaordnr  43292  omnord1  43301  nnoeomeqom  43308  oenord1  43312  succlg  43324  oacl2g  43326  omabs2  43328  omcl2  43329  omcl3g  43330  naddwordnexlem4  43397  nlimsuc  43437  intabssd  43515  elmapintrab  43572  eliunov2  43675  gneispaceel2  44140  mnuop23d  44262  mnuunid  44273  mnurndlem1  44277  expgrowthi  44329  dvconstbi  44330  tratrb  44533  suctrALT2VD  44832  suctrALT2  44833  en3lplem1VD  44839  en3lpVD  44841  tratrbVD  44857  suctrALTcf  44918  suctrALTcfVD  44919  suctrALT3  44920  unisnALT  44922  0elaxnul  44980  pwclaxpow  44981  prclaxpr  44982  uniclaxun  44983  omssaxinf2  44985  wfaxrep  44991  restuni3  45119  supminfxr  45467  xlimxrre  45836  xlimmnfvlem1  45837  xlimpnfvlem1  45841  icccncfext  45892  stoweidlem27  46032  stoweidlem35  46040  stoweidlem46  46051  stoweidlem52  46057  ioorrnopnlem  46309  ioorrnopnxrlem  46311  issal  46319  intsaluni  46334  salgencntex  46348  smfresal  46793  funressnfv  47048  fnbrafvb  47159  afvco2  47181  ndmaovg  47189  aovmpt4g  47206  fafv2elrnb  47240  fvelsetpreimafv  47392  elsetpreimafvbi  47396  sprsymrelf1lem  47496  paireqne  47516  fpprbasnn  47734  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  dfclnbgr6  47860  dfsclnbgr6  47862  grtri  47943  stgrvtx0  47965  stgrnbgr0  47967  isubgr3stgrlem3  47971  gpgvtx0  48048  gpgvtx1  48049  gpg3kgrtriex  48084  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  rngccatidALTV  48264  ringccatidALTV  48298  ldepspr  48466  mosn  48805  indthinc  49455  indthincALT  49456