Theorem eleq2 2826

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleq12  2827  eleq2i  2829  nelneq2  2862  dvelimdc  2924  raleqf  3327  rexeqfOLD  3329  rmoeq1OLD  3385  reueq1OLD  3386  rmoeq1f  3391  rabeq  3415  rabeqd  3429  rabeqf  3435  clel3g  3617  clel4g  3619  sbcbi2  3801  sbcel2gv  3809  csbeq2  3856  difeq2  4074  uneq1  4115  unineq  4242  nel02  4293  n0i  4294  sbnfc2  4393  disjel  4411  elif  4525  exsnrex  4639  elinsn  4669  sneqrg  4797  preq1b  4804  preq12b  4808  elpreqprb  4826  elunii  4870  elinti  4913  intss1  4920  intmin  4925  intab  4935  iuneqconst  4960  iineq2  4969  dfiun2g  4987  dfiin2g  4988  breq  5102  zfrepclf  5238  zfauscl  5245  sseliALT  5256  inuni  5297  selsALT  5396  rext  5403  intidg  5412  elopg  5422  opth1  5431  opthwiener  5470  xpeq1  5646  xpeq2  5653  0nelelxp  5667  opthprc  5696  ordtri1  6358  ordtri3  6361  nsuceq0  6410  suctr  6413  ordnbtwn  6420  funopg  6534  dffv2  6937  fveqdmss  7032  dffo4  7057  funopdmsn  7105  fnsnbOLD  7122  elunirn  7207  f1oiso  7307  canth  7322  eusvobj2  7360  mpoeq123  7440  ndmovg  7551  uniuni  7717  iunpw  7726  oneqmin  7755  onuninsuci  7792  nlimsucg  7794  limomss  7823  nnlim  7832  peano5  7845  unielxp  7981  cnvf1o  8063  soseq  8111  smoel  8302  smo11  8306  tz7.44-2  8348  nlim2  8427  ord1eln01  8433  ord2eln012  8434  oawordeulem  8491  oaordex  8495  omordi  8503  oneo  8518  oeordi  8525  oeoa  8535  oeoe  8537  nnmordi  8569  nnaordex  8576  nnaordex2  8577  omabs  8589  nnneo  8593  omsmolem  8595  elqsn0  8733  qsel  8745  mapsnd  8836  undifixp  8884  boxriin  8890  boxcutc  8891  pssnn  9105  fineqvlem  9178  fineqv  9179  en1eqsn  9187  fissuni  9269  dffi2  9338  inficl  9340  dffi3  9346  wofib  9462  zfregcl  9511  zfregclOLD  9512  nelaneq  9518  en3lplem1  9533  en3lp  9535  suc11reg  9540  inf0  9542  inf3lem2  9550  inf3lem3  9551  infeq5i  9557  axinf2  9561  dfom3  9568  elom3  9569  cantnfle  9592  oemapvali  9605  cantnflem1  9610  tc2  9661  r1sdom  9698  rankwflemb  9717  rankval3b  9750  rankunb  9774  rankuni2b  9777  cardlim  9896  cardprclem  9903  infxpenlem  9935  alephnbtwn  9993  alephordi  9996  cardaleph  10011  alephfp  10030  alephval3  10032  dfac3  10043  dfac5lem2  10046  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  kmlem2  10074  coflim  10183  cfsmolem  10192  fin23lem30  10264  isf34lem4  10299  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  zorn2lem7  10424  axdclem  10441  brdom7disj  10453  brdom6disj  10454  axpowndlem3  10522  winainflem  10616  iswun  10627  eltskg  10673  inar1  10698  elgrug  10715  inaprc  10759  eltskm  10766  addnidpi  10824  indpi  10830  nqereu  10852  elnp  10910  elnpi  10911  genpnnp  10928  ltaddpr  10957  dfnn2  12170  dfnn3  12171  dfuzi  12595  uz11  12788  elfzonlteqm1  13669  fzoopth  13690  om2uzlti  13885  axdc4uz  13919  hashrabsn1  14309  hashbclem  14387  hashf1lem2  14391  hash2prb  14407  hash2prd  14410  hash3tpb  14430  wrdsymb0  14484  lsw0  14500  swrdwrdsymb  14598  rtrclreclem3  14995  prodeq1f  15841  prodeq1  15842  rpnnen2lem1  16151  rpnnen2lem2  16152  lcmfval  16560  lcmf0val  16561  ismre  17521  isacs  17586  initoid  17937  termoid  17938  initoeu2lem1  17950  clatl  18443  mreclatBAD  18498  issubmgm  18639  issubm  18740  dfgrp2e  18905  isnsg  19096  cycsubg  19149  resghm  19173  ghmeql  19180  gsmsymgreq  19373  f1otrspeq  19388  pmtrval  19392  pmtrdifellem4  19420  pmtrprfval  19428  gsumzsplit  19868  pgpfac1lem1  20017  pgpfac1lem5  20022  pgpfac1  20023  ablsimpnosubgd  20047  c0snmgmhm  20410  c0snmhm  20411  0ring01eq  20474  issubrg  20516  lmodfopnelem2  20862  islss  20897  lspsneq0  20975  lmhmeql  21019  lspdisjb  21093  lidl1el  21193  rngqiprngfulem2  21279  rngqipring1  21283  lidldvgen  21301  islindf4  21805  mplcoe1  22004  mplcoe5  22007  selvfval  22089  m1detdiag  22553  mdetunilem9  22576  maducoeval2  22596  madugsum  22599  chpmat1dlem  22791  istopg  22851  toprntopon  22881  fiinbas  22908  topbas  22928  ppttop  22963  pptbas  22964  epttop  22965  elcls  23029  clsndisj  23031  iscldtop  23051  neiptopnei  23088  restbas  23114  restntr  23138  pnfnei  23176  mnfnei  23177  cnpimaex  23212  lmcvg  23218  iscnp4  23219  cncnpi  23234  cnconst2  23239  cnprest  23245  cnprest2  23246  cnpdis  23249  lmss  23254  lmff  23257  cnt0  23302  ist1-3  23305  cnhaus  23310  isreg2  23333  dishaus  23338  ordthauslem  23339  cmpsublem  23355  cmpsub  23356  cmpcld  23358  hauscmplem  23362  unconn  23385  conncompid  23387  conncompss  23389  1stcfb  23401  1stcrest  23409  2ndcctbss  23411  2ndcomap  23414  dis2ndc  23416  1stcelcls  23417  llyeq  23426  nllyeq  23427  restnlly  23438  islly2  23440  lly1stc  23452  dislly  23453  hauspwdom  23457  finlocfin  23476  unisngl  23483  dissnlocfin  23485  locfindis  23486  comppfsc  23488  llycmpkgen2  23506  txbas  23523  eltx  23524  ptpjopn  23568  ptclsg  23571  txcnp  23576  ptcnplem  23577  ptcnp  23578  txlly  23592  pthaus  23594  txtube  23596  txhaus  23603  txlm  23604  tx1stc  23606  txkgen  23608  xkohaus  23609  xkopt  23611  xkococnlem  23615  tgqtop  23668  kqfvima  23686  kqt0lem  23692  isr0  23693  regr1lem  23695  kqreglem1  23697  kqreglem2  23698  reghmph  23749  fbssfi  23793  isfil  23803  filuni  23841  isufil  23859  isufil2  23864  fixufil  23878  uffixfr  23879  uffixsn  23881  rnelfm  23909  flimopn  23931  flimrest  23939  flimcls  23941  txflf  23962  fclsopni  23971  fclsrest  23980  fclscf  23981  fcfnei  23991  alexsublem  24000  alexsubALTlem3  24005  alexsubALT  24007  tmdgsum2  24052  symgtgp  24062  subgntr  24063  opnsubg  24064  ghmcnp  24071  tgpt0  24075  qustgpopn  24076  tsmsi  24090  tsmssubm  24099  tsmssplit  24108  isust  24160  ustn0  24177  blssps  24380  blss  24381  blssexps  24382  blssex  24383  neibl  24457  blcld  24461  metss  24464  methaus  24476  met1stc  24477  met2ndci  24478  metrest  24480  prdsxmslem2  24485  metcnp3  24496  dscopn  24529  idnghm  24699  qdensere  24725  tgioo  24752  tgqioo  24756  zdis  24773  xrge0tsms  24791  cnheibor  24922  lmmbr  25226  bcthlem4  25295  ovolicc2lem5  25490  dyadmbllem  25568  i1fd  25650  itg11  25660  itg2gt0  25729  itgeq1f  25740  itgeq1fOLD  25741  itgeq1  25742  bddmulibl  25808  ellimc2  25846  limcnlp  25847  ellimc3  25848  limcflf  25850  limciun  25863  lhop1lem  25986  ig1pdvds  26153  plycpn  26265  aannenlem2  26305  efopn  26635  xrlimcnp  26946  wilthlem2  27047  wilthlem3  27048  nodenselem8  27671  noetasuplem4  27716  noetainflem4  27720  nocvxminlem  27762  lrrecfr  27951  addsprop  27984  bdayons  28284  addonbday  28287  dfn0s2  28340  tghilberti1  28721  colline  28733  lmif  28869  islmib  28871  incistruhgr  29164  upgr1eopALT  29202  uhgrvtxedgiedgb  29221  upgredg2vtx  29226  edglnl  29228  numedglnl  29229  uhgr2edg  29293  umgrvad2edg  29298  usgredg4  29302  usgredg2vtxeuALT  29307  uspgredg2vlem  29308  ushgredgedg  29314  nbgr1vtx  29443  nbusgredgeu0  29453  nbusgrf1o0  29454  nb3grprlem1  29465  nb3grprlem2  29466  uvtx01vtx  29482  nbupgruvtxres  29492  cplgr1vlem  29514  cplgr1v  29515  vtxd0nedgb  29574  vtxduhgr0nedg  29578  1loopgrvd2  29589  1egrvtxdg0  29597  uspgrloopvtxel  29602  vtxdginducedm1lem4  29628  wlk1walk  29724  wlkp1lem1  29757  pthdivtx  29812  0enwwlksnge1  29949  usgrwwlks2on  30043  umgrwwlks2on  30044  rusgr0edg  30061  eleclclwwlkn  30163  upgr4cycl4dv4e  30272  1conngr  30281  vdn0conngrumgrv2  30283  eupth2eucrct  30304  eupth2lem1  30305  frgrncvvdeqlem7  30392  frgrncvvdeqlem9  30394  frgrwopregasn  30403  frgrwopregbsn  30404  l2p  30567  lpni  30568  issh  31296  pjoc1  31522  h1dn0  31640  spansneleqi  31657  nonbooli  31739  pjch  31782  pjnel  31814  cdjreui  32520  rexunirn  32578  rabsnel  32587  nelun  32600  iinabrex  32656  opabdm  32701  opabrn  32702  fpwrelmapffslem  32822  fpwrelmap  32823  fz1nntr  32893  indval  32943  xrge0tsmsd  33167  nsgqusf1olem3  33508  elrspunidl  33521  isprmidl  33531  constrmon  33922  reff  34017  tpr2rico  34090  lmxrge0  34130  issiga  34290  isrnsiga  34291  isldsys  34334  isros  34346  issros  34353  ddeval1  34412  ddeval0  34413  ismbfm  34429  dya2icoseg  34455  dya2iocnrect  34459  ballotlem7  34714  bnj216  34909  bnj563  34920  bnj956  34953  bnj545  35071  bnj548  35073  bnj570  35081  bnj900  35105  bnj929  35112  bnj964  35119  bnj983  35127  bnj1001  35135  bnj1145  35169  bnj1398  35210  bnj1498  35237  fineqvnttrclselem2  35300  fineqvnttrclse  35302  fineqvinfep  35303  wevgblacfn  35325  erdszelem1  35407  kur14lem9  35430  cnllysconn  35461  cvmsss2  35490  cvmcov2  35491  cvmsiota  35493  cvmopnlem  35494  cvmliftlem15  35514  satfv1  35579  satfdmlem  35584  mclsssvlem  35778  mclsind  35786  untelirr  35924  untsucf  35926  elintfv  35981  dfon2lem4  36000  dfon2lem7  36003  dfon2lem9  36005  dfiota3  36137  funpartlem  36158  funpartfun  36159  linethru  36369  hilbert1.1  36370  rankelg  36384  elhf2  36391  neibastop2lem  36576  exeltr  36687  regsfromregtr  36690  regsfromunir1  36692  bj-zfauscl  37172  bj-cleq  37210  bj-snsetex  37211  bj-clel3gALT  37296  bj-nuliota  37305  bj-isrvec  37549  mptsnunlem  37593  isbasisrelowllem1  37610  isbasisrelowllem2  37611  relowlssretop  37618  relowlpssretop  37619  exrecfnlem  37634  finxpeq1  37641  finxpreclem5  37650  finxpreclem6  37651  nlpineqsn  37663  fvineqsneq  37667  pibt2  37672  unccur  37854  fin2so  37858  matunitlindflem1  37867  ptrecube  37871  poimirlem9  37880  poimirlem30  37901  poimir  37904  heicant  37906  mblfinlem1  37908  ftc1anc  37952  ftc2nc  37953  cover2  37966  isbnd2  38034  prdstotbnd  38045  heibor1lem  38060  grpokerinj  38144  rngoueqz  38191  isidl  38265  1idl  38277  0rngo  38278  ispridl  38285  smprngopr  38303  isfldidl  38319  isdmn3  38325  mpobi123f  38413  iineq12f  38415  mptbi12f  38417  dfsuccl4  38725  eqvrelqsel  38951  n0eldmqseq  38985  dmqseqim2  38993  suceldisj  39069  disjlem17  39153  lsateln0  39371  ispsubsp  40121  linepsubN  40128  elpcliN  40269  dvh3dim3N  41825  dochsnnz  41826  mapdindp3  42098  sn-iotalem  42593  prjspval  42961  elmzpcl  43083  diophren  43170  dford3lem2  43384  ttac  43393  pw2f1ocnv  43394  wepwsolem  43399  kelac1  43420  onexgt  43597  onexlimgt  43600  ordnexbtwnsuc  43624  oaordnr  43653  omnord1  43662  nnoeomeqom  43669  oenord1  43673  succlg  43685  oacl2g  43687  omabs2  43689  omcl2  43690  omcl3g  43691  naddwordnexlem4  43758  nlimsuc  43797  intabssd  43875  elmapintrab  43932  eliunov2  44035  gneispaceel2  44500  mnuop23d  44622  mnuunid  44633  mnurndlem1  44637  expgrowthi  44689  dvconstbi  44690  tratrb  44892  suctrALT2VD  45191  suctrALT2  45192  en3lplem1VD  45198  en3lpVD  45200  tratrbVD  45216  suctrALTcf  45277  suctrALTcfVD  45278  suctrALT3  45279  unisnALT  45281  0elaxnul  45339  pwclaxpow  45340  prclaxpr  45341  uniclaxun  45342  omssaxinf2  45344  wfaxrep  45350  restuni3  45477  supminfxr  45822  xlimxrre  46189  xlimmnfvlem1  46190  xlimpnfvlem1  46194  icccncfext  46245  stoweidlem27  46385  stoweidlem35  46393  stoweidlem46  46404  stoweidlem52  46410  ioorrnopnlem  46662  ioorrnopnxrlem  46664  issal  46672  intsaluni  46687  salgencntex  46701  smfresal  47146  tannpoly  47250  funressnfv  47403  fnbrafvb  47514  afvco2  47536  ndmaovg  47544  aovmpt4g  47561  fafv2elrnb  47595  fvelsetpreimafv  47747  elsetpreimafvbi  47751  sprsymrelf1lem  47851  paireqne  47871  fpprbasnn  48089  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  dfclnbgr6  48216  dfsclnbgr6  48218  grtri  48300  stgrvtx0  48322  stgrnbgr0  48324  isubgr3stgrlem3  48328  gpgvtx0  48413  gpgvtx1  48414  gpg3kgrtriex  48449  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  rngccatidALTV  48632  ringccatidALTV  48666  ldepspr  48833  mosn  49172  indthinc  49821  indthincALT  49822