Theorem eleq2 2854

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  eleq12  2855  eleq2i  2857  nelneq2  2890  dvelimdc  2951  raleqf  3347  rmoeq1f  3408  rabeq  3432  rabeqd  3446  rabeqf  3452  clel3g  3622  clel4g  3624  sbcel2gv  3812  csbeq2  3859  difeq2  4075  uneq1  4115  unineq  4241  nel02  4292  sbnfc2  4404  disjel  4417  elif  4533  exsnrex  4648  elinsn  4678  sneqrg  4806  preq1b  4813  preq12b  4817  elpreqprb  4835  elunii  4879  elinti  4923  intss1  4930  intmin  4935  intab  4945  iuneqconst  4970  iineq2  4979  dfiun2g  4996  breq  5113  zfrepclf  5254  sepg  5261  zfausclOLD  5263  sseliALT  5274  vneqv  5281  inuni  5322  selsALT  5424  rext  5431  intidg  5440  elopg  5450  opth1  5459  opthwiener  5499  xpeq1  5677  xpeq2  5684  0nelelxp  5698  opthprc  5727  ordtri1  6398  ordtri3  6401  nsuceq0  6450  suctr  6453  ordnbtwn  6460  funopg  6574  dffv2  6980  fveqdmss  7077  dffo4  7102  funopdmsn  7153  fnsnbOLD  7170  elunirn  7254  f1oiso  7358  canth  7373  eusvobj2  7411  mpoeq123  7491  ndmovg  7603  uniuni  7767  iunpw  7776  oneqmin  7805  onuninsuci  7842  nlimsucg  7844  limomss  7873  nnlim  7882  peano5  7896  unielxp  8030  cnvf1o  8112  soseq  8161  smoel  8353  smo11  8357  tz7.44-2  8400  nlim2  8481  ord1eln01  8487  ord2eln012  8488  oawordeulem  8545  oaordex  8549  omordi  8557  oneo  8572  oeordi  8579  oeoa  8589  oeoe  8591  nnmordi  8623  nnaordex  8630  nnaordex2  8631  omabs  8643  nnneo  8647  omsmolem  8649  elqsn0  8788  qsel  8800  mapsnd  8890  undifixp  8938  boxriin  8944  boxcutc  8945  pssnn  9160  fineqvlem  9233  fineqv  9234  en1eqsn  9242  fissuni  9321  dffi2  9390  inficl  9392  dffi3  9398  wofib  9514  zfregcl  9563  zfregclOLD  9564  nelaneq  9571  nelaneqOLD  9572  en3lplem1  9588  en3lp  9590  suc11reg  9595  inf0  9597  inf3lem2  9605  inf3lem3  9606  infeq5i  9612  axinf2  9616  dfom3  9623  elom3  9624  cantnfle  9647  oemapvali  9660  cantnflem1  9665  tc2  9716  r1sdom  9753  rankwflemb  9772  rankval3b  9805  rankunb  9829  rankuni2b  9832  karden  9895  cardlim  9974  cardprclem  9981  infxpenlem  10013  alephnbtwn  10071  alephordi  10074  cardaleph  10089  alephfp  10108  alephval3  10110  dfac3  10121  dfac5lem2  10124  dfac5lem4  10126  dfac2b  10130  kmlem2  10151  coflim  10260  cfsmolem  10269  fin23lem30  10341  isf34lem4  10376  axdc2lem  10447  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  zorn2lem7  10501  axdclem  10518  brdom7disj  10530  brdom6disj  10531  axpowndlem3  10601  winainflem  10695  iswun  10706  eltskg  10752  inar1  10777  elgrug  10794  inaprc  10838  eltskm  10845  addnidpi  10903  indpi  10909  nqereu  10931  elnp  10989  elnpi  10990  genpnnp  11007  ltaddpr  11036  indval  12238  dfnn2  12263  dfnn3  12264  dfuzi  12705  uz11  12905  elfzonlteqm1  13789  fzoopth  13810  om2uzlti  14006  axdc4uz  14040  hashrabsn1  14430  hashbclem  14509  hashf1lem2  14513  hash2prb  14529  hash2prd  14532  hash3tpb  14552  wrdsymb0  14606  lsw0  14622  swrdwrdsymb  14724  rtrclreclem3  15123  prodeq1f  15985  prodeq1  15986  rpnnen2lem1  16294  rpnnen2lem2  16295  lcmfval  16703  lcmf0val  16704  ismre  17666  isacs  17731  initoid  18082  termoid  18083  initoeu2lem1  18095  clatl  18588  mreclatBAD  18643  issubmgm  18794  issubm  18900  dfgrp2e  19076  isnsg  19267  cycsubg  19325  resghm  19348  ghmeql  19355  gsmsymgreq  19548  f1otrspeq  19563  pmtrval  19567  pmtrdifellem4  19595  pmtrprfval  19603  gsumzsplit  20043  pgpfac1lem1  20192  pgpfac1lem5  20197  pgpfac1  20198  ablsimpnosubgd  20222  c0snmgmhm  20592  c0snmhm  20593  0ring01eq  20679  issubrg  20722  lmodfopnelem2  21072  islss  21107  lspsneq0  21185  lmhmeql  21228  lspdisjb  21302  lidl1el  21403  rngqiprngfulem2  21504  rngqipring1  21508  isprmidl  21515  lidldvgen  21554  islindf4  22040  mplcoe1  22240  mplcoe5  22243  selvfval  22322  m1detdiag  22806  mdetunilem9  22829  maducoeval2  22849  madugsum  22852  chpmat1dlem  23044  istopg  23104  toprntopon  23134  fiinbas  23161  topbas  23181  ppttop  23216  pptbas  23217  epttop  23218  elcls  23282  clsndisj  23284  iscldtop  23304  neiptopnei  23341  restbas  23367  restntr  23391  pnfnei  23429  mnfnei  23430  cnpimaex  23465  lmcvg  23471  iscnp4  23472  cncnpi  23487  cnconst2  23492  cnprest  23498  cnprest2  23499  cnpdis  23502  lmss  23507  lmff  23510  cnt0  23555  ist1-3  23558  cnhaus  23563  isreg2  23586  dishaus  23591  ordthauslem  23592  cmpsublem  23608  cmpsub  23609  cmpcld  23611  hauscmplem  23615  unconn  23638  conncompid  23640  conncompss  23642  1stcfb  23654  1stcrest  23662  2ndcctbss  23665  2ndcomap  23668  dis2ndc  23670  1stcelcls  23671  llyeq  23680  nllyeq  23681  restnlly  23692  islly2  23694  lly1stc  23706  dislly  23707  hauspwdom  23711  finlocfin  23730  unisngl  23737  dissnlocfin  23739  locfindis  23740  comppfsc  23742  llycmpkgen2  23760  txbas  23777  eltx  23778  ptpjopn  23822  ptclsg  23825  txcnp  23830  ptcnplem  23831  ptcnp  23832  txlly  23846  pthaus  23848  txtube  23850  txhaus  23857  txlm  23858  tx1stc  23860  txkgen  23862  xkohaus  23863  xkopt  23865  xkococnlem  23869  tgqtop  23922  kqfvima  23940  kqt0lem  23946  isr0  23947  regr1lem  23949  kqreglem1  23951  kqreglem2  23952  reghmph  24003  fbssfi  24047  isfil  24057  filuni  24095  isufil  24113  isufil2  24118  fixufil  24132  uffixfr  24133  uffixsn  24135  rnelfm  24163  flimopn  24185  flimrest  24193  flimcls  24195  txflf  24216  fclsopni  24225  fclsrest  24234  fclscf  24235  fcfnei  24245  alexsublem  24254  alexsubALTlem3  24259  alexsubALT  24261  tmdgsum2  24306  symgtgp  24316  subgntr  24317  opnsubg  24318  ghmcnp  24325  tgpt0  24329  qustgpopn  24330  tsmsi  24344  tsmssubm  24353  tsmssplit  24362  isust  24414  ustn0  24431  blssps  24634  blss  24635  blssexps  24636  blssex  24637  neibl  24711  blcld  24715  metss  24718  methaus  24730  met1stc  24731  met2ndci  24732  metrest  24734  prdsxmslem2  24739  metcnp3  24750  dscopn  24783  idnghm  24953  qdensere  24979  tgioo  25006  tgqioo  25010  zdis  25027  xrge0tsms  25045  cnheibor  25167  lmmbr  25470  bcthlem4  25539  ovolicc2lem5  25733  dyadmbllem  25811  i1fd  25893  itg11  25903  itg2gt0  25972  itgeq1f  25983  itgeq1fOLD  25984  itgeq1  25985  bddmulibl  26051  ellimc2  26089  limcnlp  26090  ellimc3  26091  limcflf  26093  limciun  26106  lhop1lem  26225  ig1pdvds  26390  plycpn  26503  aannenlem2  26545  efopn  26876  xrlimcnp  27186  wilthlem2  27286  wilthlem3  27287  nodenselem8  27908  noetasuplem4  27953  noetainflem4  27957  nocvxminlem  28000  lrrecfr  28189  addsprop  28222  bdayons  28522  addonbday  28525  dfn0s2  28578  tghilberti1  28963  colline  28976  lmif  29147  islmib  29149  prlngex  29258  prlngeq  29264  incistruhgr  29486  upgr1eopALT  29524  uhgrvtxedgiedgb  29543  upgredg2vtx  29548  edglnl  29550  numedglnl  29551  uhgr2edg  29618  umgrvad2edg  29623  usgredg4  29627  usgredg2vtxeuALT  29632  uspgredg2vlem  29633  ushgredgedg  29639  nbgr1vtx  29768  nbusgredgeu0  29778  nbusgrf1o0  29779  nb3grprlem1  29790  nb3grprlem2  29791  uvtx01vtx  29807  nbupgruvtxres  29817  cplgr1vlem  29839  cplgr1v  29840  vtxd0nedgb  29898  vtxduhgr0nedg  29902  1loopgrvd2  29913  1egrvtxdg0  29921  uspgrloopvtxel  29926  vtxdginducedm1lem4  29952  wlk1walk  30048  wlkp1lem1  30081  pthdivtx  30141  0enwwlksnge1  30282  usgrwwlks2on  30376  umgrwwlks2on  30377  rusgr0edg  30394  eleclclwwlkn  30496  upgr4cycl4dv4e  30609  1conngr  30618  vdn0conngrumgrv2  30620  eupth2eucrct  30641  eupth2lem1  30642  frgrncvvdeqlem7  30729  frgrncvvdeqlem9  30731  frgrwopregasn  30740  frgrwopregbsn  30741  l2p  30904  lpni  30905  issh  31633  pjoc1  31859  h1dn0  31977  spansneleqi  31994  nonbooli  32076  pjch  32119  pjnel  32151  cdjreui  32857  rexunirn  32911  rabsnel  32919  nelun  32932  iinabrex  32987  opabdm  33029  opabrn  33030  fpwrelmapffslem  33149  fpwrelmap  33150  fz1nntr  33219  xrge0tsmsd  33459  nsgqusf1olem3  33790  elrspunidl  33802  constrmon  34200  reff  34295  tpr2rico  34368  lmxrge0  34408  issiga  34568  isrnsiga  34569  isldsys  34613  isros  34625  issros  34632  ddeval1  34691  ddeval0  34692  ismbfm  34708  dya2icoseg  34734  dya2iocnrect  34738  ballotlem7  34993  bnj216  35188  bnj563  35199  bnj956  35232  bnj545  35350  bnj548  35352  bnj570  35360  bnj900  35384  bnj929  35391  bnj964  35398  bnj983  35406  bnj1001  35414  bnj1145  35448  bnj1398  35489  bnj1498  35516  fineqvnttrclselem2  35594  fineqvnttrclse  35596  fineqvinfep  35597  wevgblacfn  35654  erdszelem1  35722  kur14lem9  35745  cnllysconn  35776  cvmsss2  35805  cvmcov2  35806  cvmsiota  35808  cvmopnlem  35809  cvmliftlem15  35829  satfv1  35894  satfdmlem  35899  mclsssvlem  36093  mclsind  36101  untelirr  36239  untsucf  36241  elintfv  36296  dfon2lem4  36315  dfon2lem7  36318  dfon2lem9  36320  dfiota3  36452  funpartlem  36473  funpartfun  36474  linethru  36684  hilbert1.1  36685  rankelg  36699  elhf2  36706  ltnadd  36749  neibastop2lem  36930  regsfromregtco  37108  regsfromunir1  37110  bj-sepg  37618  bj-cleq  37657  bj-snsetex  37658  bj-clel3gALT  37743  bj-nuliota  37752  bj-isrvec  37997  mptsnunlem  38043  isbasisrelowllem1  38060  isbasisrelowllem2  38061  relowlssretop  38068  relowlpssretop  38069  exrecfnlem  38084  finxpeq1  38091  finxpreclem5  38100  finxpreclem6  38101  nlpineqsn  38113  fvineqsneq  38117  pibt2  38122  unccur  38313  fin2so  38317  matunitlindflem1  38326  ptrecube  38330  poimirlem9  38339  poimirlem30  38360  poimir  38363  heicant  38365  mblfinlem1  38367  ftc1anc  38411  ftc2nc  38412  cover2  38426  isbnd2  38494  prdstotbnd  38505  heibor1lem  38520  grpokerinj  38604  rngoueqz  38651  isidl  38725  1idl  38737  0rngo  38738  ispridl  38745  smprngopr  38763  isfldidl  38779  isdmn3  38785  mpobi123f  38871  iineq12f  38873  mptbi12f  38875  dfsuccl4  39183  eqvrelqsel  39409  n0eldmqseq  39443  dmqseqim2  39451  suceldisj  39527  disjlem17  39611  lsateln0  39829  ispsubsp  40579  linepsubN  40586  elpcliN  40727  dvh3dim3N  42283  dochsnnz  42284  mapdindp3  42556  sn-iotalem  43052  prjspval  43395  elmzpcl  43517  diophren  43600  dford3lem2  43814  ttac  43823  pw2f1ocnv  43824  wepwsolem  43829  kelac1  43850  onexgt  44027  onexlimgt  44030  ordnexbtwnsuc  44054  oaordnr  44083  omnord1  44092  nnoeomeqom  44099  oenord1  44103  succlg  44115  oacl2g  44117  omabs2  44119  omcl2  44120  omcl3g  44121  naddwordnexlem4  44188  nlimsuc  44227  intabssd  44305  elmapintrab  44362  eliunov2  44465  gneispaceel2  44930  mnuop23d  45036  mnuunid  45047  mnurndlem1  45051  expgrowthi  45103  dvconstbi  45104  tratrb  45305  suctrALT2VD  45604  suctrALT2  45605  en3lplem1VD  45611  en3lpVD  45613  tratrbVD  45629  suctrALTcf  45690  suctrALTcfVD  45691  suctrALT3  45692  unisnALT  45694  0elaxnul  45752  pwclaxpow  45753  prclaxpr  45754  uniclaxun  45755  omssaxinf2  45757  wfaxrep  45763  restuni3  45896  supminfxr  46238  xlimxrre  46605  xlimmnfvlem1  46606  xlimpnfvlem1  46610  icccncfext  46661  stoweidlem27  46801  stoweidlem35  46809  stoweidlem46  46820  stoweidlem52  46826  ioorrnopnlem  47078  ioorrnopnxrlem  47080  issal  47088  intsaluni  47103  salgencntex  47117  smfresal  47562  tannpoly  47687  funressnfv  47840  fnbrafvb  47951  afvco2  47973  ndmaovg  47981  aovmpt4g  47998  fafv2elrnb  48032  fvelsetpreimafv  48196  elsetpreimafvbi  48200  sprsymrelf1lem  48300  paireqne  48320  fpprbasnn  48554  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  dfclnbgr6  48681  dfsclnbgr6  48683  grtri  48765  stgrvtx0  48787  stgrnbgr0  48789  isubgr3stgrlem3  48793  gpgvtx0  48878  gpgvtx1  48879  gpg3kgrtriex  48914  pgnbgreunbgrlem3  48943  pgnbgreunbgrlem6  48949  rngccatidALTV  49096  ringccatidALTV  49130  prmringnzring  49161  isidom3  49169  ldepspr  49312  mosn  49650  indthinc  50299  indthincALT  50300