Theorem eleq2 2823

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  eleq12  2824  eleq2i  2826  nelneq2  2859  dvelimdc  2921  raleqf  3323  rexeqfOLD  3325  rmoeq1OLD  3381  reueq1OLD  3382  rmoeq1f  3387  rabeq  3411  rabeqd  3425  rabeqf  3431  clel3g  3613  clel4g  3615  sbcbi2  3797  sbcel2gv  3805  csbeq2  3852  difeq2  4070  uneq1  4111  unineq  4238  nel02  4289  n0i  4290  sbnfc2  4389  disjel  4407  elif  4521  exsnrex  4635  elinsn  4665  sneqrg  4793  preq1b  4800  preq12b  4804  elpreqprb  4822  elunii  4866  elinti  4909  intss1  4916  intmin  4921  intab  4931  iuneqconst  4956  iineq2  4965  dfiun2g  4983  dfiin2g  4984  breq  5098  zfrepclf  5234  zfauscl  5241  sseliALT  5252  inuni  5293  selsALT  5387  rext  5394  intidg  5403  elopg  5412  opth1  5421  opthwiener  5460  xpeq1  5636  xpeq2  5643  0nelelxp  5657  opthprc  5686  ordtri1  6348  ordtri3  6351  nsuceq0  6400  suctr  6403  ordnbtwn  6410  funopg  6524  dffv2  6927  fveqdmss  7021  dffo4  7046  funopdmsn  7093  fnsnbOLD  7110  elunirn  7195  f1oiso  7295  canth  7310  eusvobj2  7348  mpoeq123  7428  ndmovg  7539  uniuni  7705  iunpw  7714  oneqmin  7743  onuninsuci  7780  nlimsucg  7782  limomss  7811  nnlim  7820  peano5  7833  unielxp  7969  cnvf1o  8051  soseq  8099  smoel  8290  smo11  8294  tz7.44-2  8336  nlim2  8415  ord1eln01  8421  ord2eln012  8422  oawordeulem  8479  oaordex  8483  omordi  8491  oneo  8506  oeordi  8513  oeoa  8523  oeoe  8525  nnmordi  8557  nnaordex  8564  nnaordex2  8565  omabs  8577  nnneo  8581  omsmolem  8583  elqsn0  8719  qsel  8731  mapsnd  8822  undifixp  8870  boxriin  8876  boxcutc  8877  pssnn  9091  fineqvlem  9164  fineqv  9165  en1eqsn  9173  fissuni  9255  dffi2  9324  inficl  9326  dffi3  9332  wofib  9448  zfregcl  9497  zfregclOLD  9498  nelaneq  9504  en3lplem1  9519  en3lp  9521  suc11reg  9526  inf0  9528  inf3lem2  9536  inf3lem3  9537  infeq5i  9543  axinf2  9547  dfom3  9554  elom3  9555  cantnfle  9578  oemapvali  9591  cantnflem1  9596  tc2  9647  r1sdom  9684  rankwflemb  9703  rankval3b  9736  rankunb  9760  rankuni2b  9763  cardlim  9882  cardprclem  9889  infxpenlem  9921  alephnbtwn  9979  alephordi  9982  cardaleph  9997  alephfp  10016  alephval3  10018  dfac3  10029  dfac5lem2  10032  dfac5lem4  10034  dfac5lem4OLD  10036  dfac2b  10039  kmlem2  10060  coflim  10169  cfsmolem  10178  fin23lem30  10250  isf34lem4  10285  axdc2lem  10356  axdc3lem2  10359  axdc3lem4  10361  axdc4lem  10363  zorn2lem7  10410  axdclem  10427  brdom7disj  10439  brdom6disj  10440  axpowndlem3  10508  winainflem  10602  iswun  10613  eltskg  10659  inar1  10684  elgrug  10701  inaprc  10745  eltskm  10752  addnidpi  10810  indpi  10816  nqereu  10838  elnp  10896  elnpi  10897  genpnnp  10914  ltaddpr  10943  dfnn2  12156  dfnn3  12157  dfuzi  12581  uz11  12774  elfzonlteqm1  13655  fzoopth  13676  om2uzlti  13871  axdc4uz  13905  hashrabsn1  14295  hashbclem  14373  hashf1lem2  14377  hash2prb  14393  hash2prd  14396  hash3tpb  14416  wrdsymb0  14470  lsw0  14486  swrdwrdsymb  14584  rtrclreclem3  14981  prodeq1f  15827  prodeq1  15828  rpnnen2lem1  16137  rpnnen2lem2  16138  lcmfval  16546  lcmf0val  16547  ismre  17507  isacs  17572  initoid  17923  termoid  17924  initoeu2lem1  17936  clatl  18429  mreclatBAD  18484  issubmgm  18625  issubm  18726  dfgrp2e  18891  isnsg  19082  cycsubg  19135  resghm  19159  ghmeql  19166  gsmsymgreq  19359  f1otrspeq  19374  pmtrval  19378  pmtrdifellem4  19406  pmtrprfval  19414  gsumzsplit  19854  pgpfac1lem1  20003  pgpfac1lem5  20008  pgpfac1  20009  ablsimpnosubgd  20033  c0snmgmhm  20396  c0snmhm  20397  0ring01eq  20460  issubrg  20502  lmodfopnelem2  20848  islss  20883  lspsneq0  20961  lmhmeql  21005  lspdisjb  21079  lidl1el  21179  rngqiprngfulem2  21265  rngqipring1  21269  lidldvgen  21287  islindf4  21791  mplcoe1  21990  mplcoe5  21993  selvfval  22075  m1detdiag  22539  mdetunilem9  22562  maducoeval2  22582  madugsum  22585  chpmat1dlem  22777  istopg  22837  toprntopon  22867  fiinbas  22894  topbas  22914  ppttop  22949  pptbas  22950  epttop  22951  elcls  23015  clsndisj  23017  iscldtop  23037  neiptopnei  23074  restbas  23100  restntr  23124  pnfnei  23162  mnfnei  23163  cnpimaex  23198  lmcvg  23204  iscnp4  23205  cncnpi  23220  cnconst2  23225  cnprest  23231  cnprest2  23232  cnpdis  23235  lmss  23240  lmff  23243  cnt0  23288  ist1-3  23291  cnhaus  23296  isreg2  23319  dishaus  23324  ordthauslem  23325  cmpsublem  23341  cmpsub  23342  cmpcld  23344  hauscmplem  23348  unconn  23371  conncompid  23373  conncompss  23375  1stcfb  23387  1stcrest  23395  2ndcctbss  23397  2ndcomap  23400  dis2ndc  23402  1stcelcls  23403  llyeq  23412  nllyeq  23413  restnlly  23424  islly2  23426  lly1stc  23438  dislly  23439  hauspwdom  23443  finlocfin  23462  unisngl  23469  dissnlocfin  23471  locfindis  23472  comppfsc  23474  llycmpkgen2  23492  txbas  23509  eltx  23510  ptpjopn  23554  ptclsg  23557  txcnp  23562  ptcnplem  23563  ptcnp  23564  txlly  23578  pthaus  23580  txtube  23582  txhaus  23589  txlm  23590  tx1stc  23592  txkgen  23594  xkohaus  23595  xkopt  23597  xkococnlem  23601  tgqtop  23654  kqfvima  23672  kqt0lem  23678  isr0  23679  regr1lem  23681  kqreglem1  23683  kqreglem2  23684  reghmph  23735  fbssfi  23779  isfil  23789  filuni  23827  isufil  23845  isufil2  23850  fixufil  23864  uffixfr  23865  uffixsn  23867  rnelfm  23895  flimopn  23917  flimrest  23925  flimcls  23927  txflf  23948  fclsopni  23957  fclsrest  23966  fclscf  23967  fcfnei  23977  alexsublem  23986  alexsubALTlem3  23991  alexsubALT  23993  tmdgsum2  24038  symgtgp  24048  subgntr  24049  opnsubg  24050  ghmcnp  24057  tgpt0  24061  qustgpopn  24062  tsmsi  24076  tsmssubm  24085  tsmssplit  24094  isust  24146  ustn0  24163  blssps  24366  blss  24367  blssexps  24368  blssex  24369  neibl  24443  blcld  24447  metss  24450  methaus  24462  met1stc  24463  met2ndci  24464  metrest  24466  prdsxmslem2  24471  metcnp3  24482  dscopn  24515  idnghm  24685  qdensere  24711  tgioo  24738  tgqioo  24742  zdis  24759  xrge0tsms  24777  cnheibor  24908  lmmbr  25212  bcthlem4  25281  ovolicc2lem5  25476  dyadmbllem  25554  i1fd  25636  itg11  25646  itg2gt0  25715  itgeq1f  25726  itgeq1fOLD  25727  itgeq1  25728  bddmulibl  25794  ellimc2  25832  limcnlp  25833  ellimc3  25834  limcflf  25836  limciun  25849  lhop1lem  25972  ig1pdvds  26139  plycpn  26251  aannenlem2  26291  efopn  26621  xrlimcnp  26932  wilthlem2  27033  wilthlem3  27034  nodenselem8  27657  noetasuplem4  27702  noetainflem4  27706  nocvxminlem  27744  lrrecfr  27913  addsprop  27946  bdayon  28240  dfn0s2  28292  tghilberti1  28658  colline  28670  lmif  28806  islmib  28808  incistruhgr  29101  upgr1eopALT  29139  uhgrvtxedgiedgb  29158  upgredg2vtx  29163  edglnl  29165  numedglnl  29166  uhgr2edg  29230  umgrvad2edg  29235  usgredg4  29239  usgredg2vtxeuALT  29244  uspgredg2vlem  29245  ushgredgedg  29251  nbgr1vtx  29380  nbusgredgeu0  29390  nbusgrf1o0  29391  nb3grprlem1  29402  nb3grprlem2  29403  uvtx01vtx  29419  nbupgruvtxres  29429  cplgr1vlem  29451  cplgr1v  29452  vtxd0nedgb  29511  vtxduhgr0nedg  29515  1loopgrvd2  29526  1egrvtxdg0  29534  uspgrloopvtxel  29539  vtxdginducedm1lem4  29565  wlk1walk  29661  wlkp1lem1  29694  pthdivtx  29749  0enwwlksnge1  29886  usgrwwlks2on  29980  umgrwwlks2on  29981  rusgr0edg  29998  eleclclwwlkn  30100  upgr4cycl4dv4e  30209  1conngr  30218  vdn0conngrumgrv2  30220  eupth2eucrct  30241  eupth2lem1  30242  frgrncvvdeqlem7  30329  frgrncvvdeqlem9  30331  frgrwopregasn  30340  frgrwopregbsn  30341  l2p  30503  lpni  30504  issh  31232  pjoc1  31458  h1dn0  31576  spansneleqi  31593  nonbooli  31675  pjch  31718  pjnel  31750  cdjreui  32456  rexunirn  32515  rabsnel  32524  nelun  32537  iinabrex  32593  opabdm  32638  opabrn  32639  fpwrelmapffslem  32760  fpwrelmap  32761  fz1nntr  32831  indval  32881  xrge0tsmsd  33104  nsgqusf1olem3  33445  elrspunidl  33458  isprmidl  33468  constrmon  33850  reff  33945  tpr2rico  34018  lmxrge0  34058  issiga  34218  isrnsiga  34219  isldsys  34262  isros  34274  issros  34281  ddeval1  34340  ddeval0  34341  ismbfm  34357  dya2icoseg  34383  dya2iocnrect  34387  ballotlem7  34642  bnj216  34837  bnj563  34848  bnj956  34881  bnj545  35000  bnj548  35002  bnj570  35010  bnj900  35034  bnj929  35041  bnj964  35048  bnj983  35056  bnj1001  35064  bnj1145  35098  bnj1398  35139  bnj1498  35166  fineqvnttrclselem2  35227  fineqvnttrclse  35229  fineqvinfep  35230  wevgblacfn  35252  erdszelem1  35334  kur14lem9  35357  cnllysconn  35388  cvmsss2  35417  cvmcov2  35418  cvmsiota  35420  cvmopnlem  35421  cvmliftlem15  35441  satfv1  35506  satfdmlem  35511  mclsssvlem  35705  mclsind  35713  untelirr  35851  untsucf  35853  elintfv  35908  dfon2lem4  35927  dfon2lem7  35930  dfon2lem9  35932  dfiota3  36064  funpartlem  36085  funpartfun  36086  linethru  36296  hilbert1.1  36297  rankelg  36311  elhf2  36318  neibastop2lem  36503  bj-zfauscl  37068  bj-cleq  37106  bj-snsetex  37107  bj-clel3gALT  37192  bj-nuliota  37201  bj-isrvec  37438  mptsnunlem  37482  isbasisrelowllem1  37499  isbasisrelowllem2  37500  relowlssretop  37507  relowlpssretop  37508  exrecfnlem  37523  finxpeq1  37530  finxpreclem5  37539  finxpreclem6  37540  nlpineqsn  37552  fvineqsneq  37556  pibt2  37561  unccur  37743  fin2so  37747  matunitlindflem1  37756  ptrecube  37760  poimirlem9  37769  poimirlem30  37790  poimir  37793  heicant  37795  mblfinlem1  37797  ftc1anc  37841  ftc2nc  37842  cover2  37855  isbnd2  37923  prdstotbnd  37934  heibor1lem  37949  grpokerinj  38033  rngoueqz  38080  isidl  38154  1idl  38166  0rngo  38167  ispridl  38174  smprngopr  38192  isfldidl  38208  isdmn3  38214  mpobi123f  38302  iineq12f  38304  mptbi12f  38306  dfsuccl4  38587  eqvrelqsel  38812  n0eldmqseq  38847  dmqseqim2  38855  disjlem17  38997  lsateln0  39194  ispsubsp  39944  linepsubN  39951  elpcliN  40092  dvh3dim3N  41648  dochsnnz  41649  mapdindp3  41921  sn-iotalem  42419  prjspval  42788  elmzpcl  42910  diophren  42997  dford3lem2  43211  ttac  43220  pw2f1ocnv  43221  wepwsolem  43226  kelac1  43247  onexgt  43424  onexlimgt  43427  ordnexbtwnsuc  43451  oaordnr  43480  omnord1  43489  nnoeomeqom  43496  oenord1  43500  succlg  43512  oacl2g  43514  omabs2  43516  omcl2  43517  omcl3g  43518  naddwordnexlem4  43585  nlimsuc  43624  intabssd  43702  elmapintrab  43759  eliunov2  43862  gneispaceel2  44327  mnuop23d  44449  mnuunid  44460  mnurndlem1  44464  expgrowthi  44516  dvconstbi  44517  tratrb  44719  suctrALT2VD  45018  suctrALT2  45019  en3lplem1VD  45025  en3lpVD  45027  tratrbVD  45043  suctrALTcf  45104  suctrALTcfVD  45105  suctrALT3  45106  unisnALT  45108  0elaxnul  45166  pwclaxpow  45167  prclaxpr  45168  uniclaxun  45169  omssaxinf2  45171  wfaxrep  45177  restuni3  45304  supminfxr  45650  xlimxrre  46017  xlimmnfvlem1  46018  xlimpnfvlem1  46022  icccncfext  46073  stoweidlem27  46213  stoweidlem35  46221  stoweidlem46  46232  stoweidlem52  46238  ioorrnopnlem  46490  ioorrnopnxrlem  46492  issal  46500  intsaluni  46515  salgencntex  46529  smfresal  46974  tannpoly  47078  funressnfv  47231  fnbrafvb  47342  afvco2  47364  ndmaovg  47372  aovmpt4g  47389  fafv2elrnb  47423  fvelsetpreimafv  47575  elsetpreimafvbi  47579  sprsymrelf1lem  47679  paireqne  47699  fpprbasnn  47917  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  dfclnbgr6  48044  dfsclnbgr6  48046  grtri  48128  stgrvtx0  48150  stgrnbgr0  48152  isubgr3stgrlem3  48156  gpgvtx0  48241  gpgvtx1  48242  gpg3kgrtriex  48277  pgnbgreunbgrlem3  48306  pgnbgreunbgrlem6  48312  rngccatidALTV  48460  ringccatidALTV  48494  ldepspr  48661  mosn  49000  indthinc  49649  indthincALT  49650