Theorem eleq2 2852

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838

This theorem is used by:  eleq12  2853  eleq2i  2855  nelneq2  2888  dvelimdc  2949  raleqf  3344  rmoeq1f  3405  rabeq  3429  rabeqd  3442  rabeqf  3448  clel3g  3617  clel4g  3619  sbcel2gv  3807  csbeq2  3855  difeq2  4059  uneq1  4162  unineq  4235  nel02  4287  sbnfc2  4399  disjel  4412  elif  4528  exsnrex  4640  elinsn  4670  sneqrg  4796  preq1b  4803  preq12b  4807  elpreqprb  4825  elunii  4874  elinti  4918  intss1  4925  intmin  4930  intab  4940  iuneqconst  4965  iineq2  4974  dfiun2g  4990  breq  5107  zfrepclf  5246  sepg  5253  zfausclOLD  5255  sseliALT  5265  vneqv  5272  inuni  5314  selsALT  5412  rext  5419  intidg  5428  elopg  5438  opth1  5447  opthwiener  5490  xpeq1  5668  xpeq2  5675  0nelelxp  5689  opthprc  5718  ordtri1  6402  ordtri3  6405  nsuceq0  6454  suctr  6457  ordnbtwn  6464  funopg  6582  dffv2  6988  fveqdmss  7086  dffo4  7111  funopdmsn  7162  elunirn  7262  f1oiso  7366  canth  7381  eusvobj2  7419  mpoeq123  7499  ndmovg  7611  uniuni  7783  iunpw  7792  oneqmin  7821  onuninsuci  7858  nlimsucg  7860  limomss  7889  nnlim  7898  peano5  7912  unielxp  8046  cnvf1o  8132  soseq  8186  smoel  8379  smo11  8383  tz7.44-2  8426  nlim2  8509  ord1eln01  8515  ord2eln012  8516  oawordeulem  8573  oaordex  8577  omordi  8585  oneo  8600  oeordi  8607  oeoa  8617  oeoe  8619  nnmordi  8651  nnaordex  8658  nnaordex2  8659  omabs  8671  nnneo  8675  omsmolem  8677  elqsn0  8816  qsel  8828  mapsnd  8925  undifixp  8973  boxriin  8979  boxcutc  8980  pssnn  9195  fineqvlem  9268  fineqv  9269  en1eqsn  9277  fissuni  9357  dffi2  9425  inficl  9427  dffi3  9433  wofib  9549  zfregcl  9598  zfregclOLD  9599  nelaneq  9606  nelaneqOLD  9607  en3lplem1  9623  en3lp  9625  suc11reg  9630  inf0  9632  inf3lem2  9640  inf3lem3  9641  infeq5i  9647  axinf2  9651  dfom3  9658  elom3  9659  cantnfle  9682  oemapvali  9695  cantnflem1  9700  tc2  9751  r1sdom  9791  rankwflemb  9810  rankwflembOLD  9811  rankval3b  9846  rankelg  9862  rankunb  9874  rankuni2b  9877  elhf2  9920  karden  9969  cardlim  10063  cardprclem  10070  infxpenlem  10102  alephnbtwn  10160  alephordi  10163  cardaleph  10178  alephfp  10197  alephval3  10199  dfac3  10210  dfac5lem2  10213  dfac5lem4  10215  dfac2b  10219  kmlem2  10240  coflim  10349  cfsmolem  10358  fin23lem30  10430  isf34lem4  10465  axdc2lem  10536  axdc3lem2  10539  axdc3lem4  10541  axdc4lem  10543  zorn2lem7  10590  axdclem  10607  brdom7disj  10620  brdom6disj  10621  axpowndlem3  10694  winainflem  10788  iswun  10799  eltskg  10845  inar1  10870  elgrug  10887  inaprc  10931  eltskm  10938  addnidpi  10996  indpi  11002  nqereu  11024  elnp  11082  elnpi  11083  genpnnp  11100  ltaddpr  11129  indval  12333  dfnn2  12358  dfnn3  12359  dfuzi  12800  uz11  13000  elfzonlteqm1  13886  fzoopth  13907  om2uzlti  14103  axdc4uz  14137  hashrabsn1  14528  hashbclem  14607  hashf1lem2  14611  hash2prb  14627  hash2prd  14630  hash3tpb  14650  wrdsymb0  14704  lsw0  14720  swrdwrdsymb  14823  rtrclreclem3  15225  prodeq1f  16087  prodeq1  16088  rpnnen2lem1  16394  rpnnen2lem2  16395  lcmfval  16808  lcmf0val  16809  ismre  17772  isacs  17837  initoid  18188  termoid  18189  initoeu2lem1  18201  clatl  18694  mreclatBAD  18749  issubmgm  18903  issubm  19010  dfgrp2e  19186  isnsg  19377  cycsubg  19435  resghm  19458  ghmeql  19465  gsmsymgreq  19658  f1otrspeq  19673  pmtrval  19677  pmtrdifellem4  19705  pmtrprfval  19713  gsumzsplit  20153  pgpfac1lem1  20302  pgpfac1lem5  20307  pgpfac1  20308  ablsimpnosubgd  20332  c0snmgmhm  20704  c0snmhm  20705  0ring01eq  20792  issubrg  20835  lmodfopnelem2  21186  islss  21221  lspsneq0  21299  lmhmeql  21342  lspdisjb  21416  lidl1el  21517  rngqiprngfulem2  21620  rngqipring1  21624  isprmidl  21631  lidldvgen  21670  islindf4  22156  mplcoe1  22358  mplcoe5  22361  selvfval  22440  m1detdiag  22924  mdetunilem9  22947  maducoeval2  22967  madugsum  22970  matunitlindflem1  23006  chpmat1dlem  23165  istopg  23225  toprntopon  23255  fiinbas  23282  topbas  23302  ppttop  23337  pptbas  23338  epttop  23339  elcls  23403  clsndisj  23405  iscldtop  23425  neiptopnei  23462  restbas  23488  restntr  23512  pnfnei  23550  mnfnei  23551  cnpimaex  23586  lmcvg  23592  iscnp4  23593  cncnpi  23608  cnconst2  23613  cnprest  23619  cnprest2  23620  cnpdis  23623  lmss  23628  lmff  23631  cnt0  23676  ist1-3  23679  cnhaus  23684  isreg2  23707  dishaus  23712  ordthauslem  23713  cmpsublem  23729  cmpsub  23730  cmpcld  23732  hauscmplem  23736  unconn  23759  conncompid  23761  conncompss  23763  1stcfb  23775  1stcrest  23783  2ndcctbss  23786  2ndcomap  23789  dis2ndc  23791  1stcelcls  23792  llyeq  23801  nllyeq  23802  restnlly  23813  islly2  23815  lly1stc  23827  dislly  23828  hauspwdom  23832  finlocfin  23851  unisngl  23858  dissnlocfin  23860  locfindis  23861  comppfsc  23863  llycmpkgen2  23881  txbas  23898  eltx  23899  ptpjopn  23943  ptclsg  23946  txcnp  23951  ptcnplem  23952  ptcnp  23953  txlly  23967  pthaus  23969  txtube  23971  txhaus  23978  txlm  23979  tx1stc  23981  txkgen  23983  xkohaus  23984  xkopt  23986  xkococnlem  23990  tgqtop  24043  kqfvima  24061  kqt0lem  24067  isr0  24068  regr1lem  24070  kqreglem1  24072  kqreglem2  24073  reghmph  24124  fbssfi  24168  isfil  24178  filuni  24216  isufil  24234  isufil2  24239  fixufil  24253  uffixfr  24254  uffixsn  24256  rnelfm  24284  flimopn  24306  flimrest  24314  flimcls  24316  txflf  24337  fclsopni  24346  fclsrest  24355  fclscf  24356  fcfnei  24366  alexsublem  24375  alexsubALTlem3  24380  alexsubALT  24382  tmdgsum2  24427  symgtgp  24437  subgntr  24438  opnsubg  24439  ghmcnp  24446  tgpt0  24450  qustgpopn  24451  tsmsi  24465  tsmssubm  24474  tsmssplit  24483  isust  24535  ustn0  24552  blssps  24755  blss  24756  blssexps  24757  blssex  24758  neibl  24832  blcld  24836  metss  24839  methaus  24851  met1stc  24852  met2ndci  24853  metrest  24855  prdsxmslem2  24860  metcnp3  24871  dscopn  24904  idnghm  25074  qdensere  25100  tgioo  25127  tgqioo  25131  zdis  25148  xrge0tsms  25166  cnheibor  25288  lmmbr  25591  bcthlem4  25660  ovolicc2lem5  25854  dyadmbllem  25932  i1fd  26014  itg11  26024  itg2gt0  26093  itgeq1f  26104  itgeq1  26105  bddmulibl  26171  ellimc2  26209  limcnlp  26210  ellimc3  26211  limcflf  26213  limciun  26226  lhop1lem  26345  ig1pdvds  26510  plycpn  26622  aannenlem2  26668  efopn  26998  xrlimcnp  27308  wilthlem2  27408  wilthlem3  27409  nodenselem8  28060  noetasuplem4  28105  noetainflem4  28109  nocvxminlem  28152  lrrecfr  28341  addsprop  28374  bdayons  28674  addonbday  28677  dfn0s2  28730  tghilberti1  29117  colline  29130  lmif  29302  islmib  29304  prlngex  29441  prlngeq  29447  incistruhgr  29669  upgr1eopALT  29707  uhgrvtxedgiedgb  29726  upgredg2vtx  29731  edglnl  29733  numedglnl  29734  uhgr2edg  29801  umgrvad2edg  29806  usgredg4  29810  usgredg2vtxeuALT  29815  uspgredg2vlem  29816  ushgredgedg  29822  nbgr1vtx  29951  nbusgredgeu0  29961  nbusgrf1o0  29962  nb3grprlem1  29973  nb3grprlem2  29974  uvtx01vtx  29990  nbupgruvtxres  30000  cplgr1vlem  30022  cplgr1v  30023  vtxd0nedgb  30081  vtxduhgr0nedg  30085  1loopgrvd2  30096  1egrvtxdg0  30104  uspgrloopvtxel  30109  vtxdginducedm1lem4  30135  wlk1walk  30231  wlkp1lem1  30264  pthdivtx  30324  0enwwlksnge1  30465  usgrwwlks2on  30559  umgrwwlks2on  30560  rusgr0edg  30577  eleclclwwlkn  30679  upgr4cycl4dv4e  30798  1conngr  30807  vdn0conngrumgrv2  30809  eupth2eucrct  30830  eupth2lem1  30831  frgrncvvdeqlem7  30918  frgrncvvdeqlem9  30920  frgrwopregasn  30929  frgrwopregbsn  30930  l2p  31093  lpni  31094  issh  31822  pjoc1  32048  h1dn0  32166  spansneleqi  32183  nonbooli  32265  pjch  32308  pjnel  32340  cdjreui  33046  rexunirn  33142  rabsnel  33150  nelun  33163  iinabrex  33217  opabdm  33259  opabrn  33260  fpwrelmapffslem  33377  fpwrelmap  33378  fz1nntr  33447  xrge0tsmsd  33687  nsgqusf1olem3  34019  elrspunidl  34031  constrmon  34429  reff  34524  tpr2rico  34597  lmxrge0  34637  issiga  34797  isrnsiga  34798  isldsys  34842  isros  34854  issros  34861  ddeval1  34920  ddeval0  34921  ismbfm  34937  dya2icoseg  34962  dya2iocnrect  34966  ballotlem7  35221  bnj216  35416  bnj563  35427  bnj956  35460  bnj545  35578  bnj548  35580  bnj570  35588  bnj900  35612  bnj929  35619  bnj964  35626  bnj983  35634  bnj1001  35642  bnj1145  35676  bnj1398  35717  bnj1498  35744  fineqvnttrclselem2  35861  fineqvnttrclse  35863  fineqvinfep  35864  wevgblacfn  35993  erdszelem1  36077  kur14lem9  36100  cnllysconn  36131  cvmsss2  36160  cvmcov2  36161  cvmsiota  36163  cvmopnlem  36164  cvmliftlem15  36184  satfv1  36249  satfdmlem  36254  mclsssvlem  36448  mclsind  36456  mirimanoffr  36581  untelirr  36600  untsucf  36602  elintfv  36657  dfon2lem4  36675  dfon2lem7  36678  dfon2lem9  36680  dfiota3  36812  funpartlem  36833  funpartfun  36834  linethru  37045  hilbert1.1  37046  ltnadd  37094  neibastop2lem  37275  regsfromregtco  37453  regsfromunir1  37455  bj-sepg  37963  bj-cleq  38002  bj-snsetex  38003  bj-clel3gALT  38102  bj-nuliota  38111  bj-isrvec  38355  mptsnunlem  38401  isbasisrelowllem1  38418  isbasisrelowllem2  38419  relowlssretop  38426  relowlpssretop  38427  exrecfnlem  38442  finxpeq1  38449  finxpreclem5  38458  finxpreclem6  38459  nlpineqsn  38471  fvineqsneq  38475  pibt2  38480  unccur  38666  fin2so  38670  ptrecube  38678  poimirlem9  38687  poimirlem30  38708  poimir  38711  heicant  38713  mblfinlem1  38715  ftc1anc  38759  ftc2nc  38760  cover2  38789  isbnd2  38857  prdstotbnd  38868  heibor1lem  38883  grpokerinj  38967  rngoueqz  39014  isidl  39088  1idl  39100  0rngo  39101  ispridl  39108  smprngopr  39126  isfldidl  39142  isdmn3  39148  mpobi123f  39234  iineq12f  39236  mptbi12f  39238  dfsuccl4  39546  eqvrelqsel  39772  n0eldmqseq  39806  dmqseqim2  39814  suceldisj  39890  disjlem17  39974  lsateln0  40192  ispsubsp  40942  linepsubN  40949  elpcliN  41090  dvh3dim3N  42646  dochsnnz  42647  mapdindp3  42919  sn-iotalem  43415  prjspval  43771  elmzpcl  43877  diophren  43960  dford3lem2  44174  ttac  44183  pw2f1ocnv  44184  wepwsolem  44189  kelac1  44205  onexgt  44382  onexlimgt  44385  ordnexbtwnsuc  44409  oaordnr  44438  omnord1  44447  nnoeomeqom  44454  oenord1  44458  succlg  44470  oacl2g  44472  omabs2  44474  omcl2  44475  omcl3g  44476  naddwordnexlem4  44543  nlimsuc  44582  intabssd  44660  elmapintrab  44717  eliunov2  44819  gneispaceel2  45284  mnuop23d  45390  mnuunid  45401  mnurndlem1  45405  expgrowthi  45457  dvconstbi  45458  tratrb  45658  suctrALT2VD  45957  suctrALT2  45958  en3lplem1VD  45964  en3lpVD  45966  tratrbVD  45982  suctrALTcf  46043  suctrALTcfVD  46044  suctrALT3  46045  unisnALT  46047  0elaxnul  46112  pwclaxpow  46113  prclaxpr  46114  uniclaxun  46115  omssaxinf2  46117  wfaxrep  46123  restuni3  46272  supminfxr  46613  xlimxrre  46980  xlimmnfvlem1  46981  xlimpnfvlem1  46985  icccncfext  47036  stoweidlem27  47176  stoweidlem35  47184  stoweidlem46  47195  stoweidlem52  47201  ioorrnopnlem  47453  ioorrnopnxrlem  47455  issal  47463  intsaluni  47478  salgencntex  47492  smfresal  47937  tannpoly  48079  funressnfv  48252  fnbrafvb  48363  afvco2  48385  ndmaovg  48393  aovmpt4g  48410  fafv2elrnb  48444  fvelsetpreimafv  48608  elsetpreimafvbi  48612  sprsymrelf1lem  48712  paireqne  48732  fpprbasnn  48966  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  dfclnbgr6  49093  dfsclnbgr6  49095  grtri  49177  stgrvtx0  49199  stgrnbgr0  49201  isubgr3stgrlem3  49205  gpgvtx0  49290  gpgvtx1  49291  gpg3kgrtriex  49326  pgnbgreunbgrlem3  49355  pgnbgreunbgrlem6  49361  rngccatidALTV  49508  ringccatidALTV  49542  prmringnzring  49573  isidom3  49581  ldepspr  49724  mosn  50063  indthinc  50736  indthincALT  50737