Theorem eleq2 2830

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eleq12  2831  eleq2i  2833  nelneq2  2866  clelsb2OLD  2870  dvelimdc  2930  raleqf  3353  rexeqfOLD  3355  rmoeq1OLD  3418  reueq1OLD  3419  rmoeq1f  3424  rabeq  3451  rabeqd  3465  rabeqf  3472  clel3g  3661  clel4g  3663  sbcbi2  3848  sbcel2gv  3857  csbeq2  3904  difeq2  4120  uneq1  4161  unineq  4288  nel02  4339  n0i  4340  sbnfc2  4439  disjel  4457  elif  4569  exsnrex  4680  elinsn  4710  sneqrg  4839  preq1b  4846  preq12b  4850  elpreqprb  4868  elunii  4912  elinti  4955  intss1  4963  intmin  4968  intab  4978  iuneqconst  5003  iineq2  5012  dfiun2g  5030  dfiin2g  5032  breq  5145  zfrepclf  5291  zfauscl  5298  sseliALT  5309  inuni  5350  selsALT  5444  rext  5453  intidg  5462  intidOLD  5463  elopg  5471  opth1  5480  opthwiener  5519  xpeq1  5699  xpeq2  5706  0nelelxp  5720  opthprc  5749  ordtri1  6417  ordtri3  6420  nsuceq0  6467  suctr  6470  ordnbtwn  6477  funopg  6600  dffv2  7004  fveqdmss  7098  dffo4  7123  funopdmsn  7170  fnsnb  7186  elunirn  7271  f1oiso  7371  canth  7385  eusvobj2  7423  mpoeq123  7505  ndmovg  7616  uniuni  7782  iunpw  7791  oneqmin  7820  onuninsuci  7861  nlimsucg  7863  limomss  7892  nnlim  7901  peano5  7915  unielxp  8052  cnvf1o  8136  soseq  8184  smoel  8400  smo11  8404  tz7.44-2  8447  nlim2  8528  ord1eln01  8534  ord2eln012  8535  oawordeulem  8592  oaordex  8596  omordi  8604  oneo  8619  oeordi  8625  oeoa  8635  oeoe  8637  nnmordi  8669  nnaordex  8676  nnaordex2  8677  omabs  8689  nnneo  8693  omsmolem  8695  elqsn0  8826  qsel  8836  mapsnd  8926  undifixp  8974  boxriin  8980  boxcutc  8981  pssnn  9208  fineqvlem  9298  fineqv  9299  en1eqsn  9308  fissuni  9397  dffi2  9463  inficl  9465  dffi3  9471  wofib  9585  zfregcl  9634  en3lplem1  9652  en3lp  9654  suc11reg  9659  inf0  9661  inf3lem2  9669  inf3lem3  9670  infeq5i  9676  axinf2  9680  dfom3  9687  elom3  9688  cantnfle  9711  oemapvali  9724  cantnflem1  9729  tc2  9782  r1sdom  9814  rankwflemb  9833  rankval3b  9866  rankunb  9890  rankuni2b  9893  cardlim  10012  cardprclem  10019  infxpenlem  10053  alephnbtwn  10111  alephordi  10114  cardaleph  10129  alephfp  10148  alephval3  10150  dfac3  10161  dfac5lem2  10164  dfac5lem4  10166  dfac5lem4OLD  10168  dfac2b  10171  kmlem2  10192  coflim  10301  cfsmolem  10310  fin23lem30  10382  isf34lem4  10417  axdc2lem  10488  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  zorn2lem7  10542  axdclem  10559  brdom7disj  10571  brdom6disj  10572  axpowndlem3  10639  winainflem  10733  iswun  10744  eltskg  10790  inar1  10815  elgrug  10832  inaprc  10876  eltskm  10883  addnidpi  10941  indpi  10947  nqereu  10969  elnp  11027  elnpi  11028  genpnnp  11045  ltaddpr  11074  dfnn2  12279  dfnn3  12280  dfuzi  12709  uz11  12903  elfzonlteqm1  13780  fzoopth  13801  om2uzlti  13991  axdc4uz  14025  hashrabsn1  14413  hashbclem  14491  hashf1lem2  14495  hash2prb  14511  hash2prd  14514  hash3tpb  14534  wrdsymb0  14587  lsw0  14603  swrdwrdsymb  14700  rtrclreclem3  15099  prodeq1f  15942  prodeq1  15943  rpnnen2lem1  16250  rpnnen2lem2  16251  lcmfval  16658  lcmf0val  16659  ismre  17633  isacs  17694  initoid  18046  termoid  18047  initoeu2lem1  18059  clatl  18553  mreclatBAD  18608  issubmgm  18715  issubm  18816  dfgrp2e  18981  isnsg  19173  cycsubg  19226  resghm  19250  ghmeql  19257  gsmsymgreq  19450  f1otrspeq  19465  pmtrval  19469  pmtrdifellem4  19497  pmtrprfval  19505  gsumzsplit  19945  pgpfac1lem1  20094  pgpfac1lem5  20099  pgpfac1  20100  ablsimpnosubgd  20124  c0snmgmhm  20462  c0snmhm  20463  0ring01eq  20529  issubrg  20571  lmodfopnelem2  20897  islss  20932  lspsneq0  21010  lmhmeql  21054  lspdisjb  21128  lidl1el  21236  rngqiprngfulem2  21322  rngqipring1  21326  lidldvgen  21344  islindf4  21858  mplcoe1  22055  mplcoe5  22058  selvfval  22138  m1detdiag  22603  mdetunilem9  22626  maducoeval2  22646  madugsum  22649  chpmat1dlem  22841  istopg  22901  toprntopon  22931  fiinbas  22959  topbas  22979  ppttop  23014  pptbas  23015  epttop  23016  elcls  23081  clsndisj  23083  iscldtop  23103  neiptopnei  23140  restbas  23166  restntr  23190  pnfnei  23228  mnfnei  23229  cnpimaex  23264  lmcvg  23270  iscnp4  23271  cncnpi  23286  cnconst2  23291  cnprest  23297  cnprest2  23298  cnpdis  23301  lmss  23306  lmff  23309  cnt0  23354  ist1-3  23357  cnhaus  23362  isreg2  23385  dishaus  23390  ordthauslem  23391  cmpsublem  23407  cmpsub  23408  cmpcld  23410  hauscmplem  23414  unconn  23437  conncompid  23439  conncompss  23441  1stcfb  23453  1stcrest  23461  2ndcctbss  23463  2ndcomap  23466  dis2ndc  23468  1stcelcls  23469  llyeq  23478  nllyeq  23479  restnlly  23490  islly2  23492  lly1stc  23504  dislly  23505  hauspwdom  23509  finlocfin  23528  unisngl  23535  dissnlocfin  23537  locfindis  23538  comppfsc  23540  llycmpkgen2  23558  txbas  23575  eltx  23576  ptpjopn  23620  ptclsg  23623  txcnp  23628  ptcnplem  23629  ptcnp  23630  txlly  23644  pthaus  23646  txtube  23648  txhaus  23655  txlm  23656  tx1stc  23658  txkgen  23660  xkohaus  23661  xkopt  23663  xkococnlem  23667  tgqtop  23720  kqfvima  23738  kqt0lem  23744  isr0  23745  regr1lem  23747  kqreglem1  23749  kqreglem2  23750  reghmph  23801  fbssfi  23845  isfil  23855  filuni  23893  isufil  23911  isufil2  23916  fixufil  23930  uffixfr  23931  uffixsn  23933  rnelfm  23961  flimopn  23983  flimrest  23991  flimcls  23993  txflf  24014  fclsopni  24023  fclsrest  24032  fclscf  24033  fcfnei  24043  alexsublem  24052  alexsubALTlem3  24057  alexsubALT  24059  tmdgsum2  24104  symgtgp  24114  subgntr  24115  opnsubg  24116  ghmcnp  24123  tgpt0  24127  qustgpopn  24128  tsmsi  24142  tsmssubm  24151  tsmssplit  24160  isust  24212  ustn0  24229  blssps  24434  blss  24435  blssexps  24436  blssex  24437  neibl  24514  blcld  24518  metss  24521  methaus  24533  met1stc  24534  met2ndci  24535  metrest  24537  prdsxmslem2  24542  metcnp3  24553  dscopn  24586  idnghm  24764  qdensere  24790  tgioo  24817  tgqioo  24821  zdis  24838  xrge0tsms  24856  cnheibor  24987  lmmbr  25292  bcthlem4  25361  ovolicc2lem5  25556  dyadmbllem  25634  i1fd  25716  itg11  25726  itg2gt0  25795  itgeq1f  25806  itgeq1fOLD  25807  itgeq1  25808  bddmulibl  25874  ellimc2  25912  limcnlp  25913  ellimc3  25914  limcflf  25916  limciun  25929  lhop1lem  26052  ig1pdvds  26219  plycpn  26331  aannenlem2  26371  efopn  26700  xrlimcnp  27011  wilthlem2  27112  wilthlem3  27113  nodenselem8  27736  noetasuplem4  27781  noetainflem4  27785  nocvxminlem  27822  lrrecfr  27976  addsprop  28009  dfn0s2  28336  tghilberti1  28645  colline  28657  lmif  28793  islmib  28795  incistruhgr  29096  upgr1eopALT  29134  uhgrvtxedgiedgb  29153  upgredg2vtx  29158  edglnl  29160  numedglnl  29161  uhgr2edg  29225  umgrvad2edg  29230  usgredg4  29234  usgredg2vtxeuALT  29239  uspgredg2vlem  29240  ushgredgedg  29246  nbgr1vtx  29375  nbusgredgeu0  29385  nbusgrf1o0  29386  nb3grprlem1  29397  nb3grprlem2  29398  uvtx01vtx  29414  nbupgruvtxres  29424  cplgr1vlem  29446  cplgr1v  29447  vtxd0nedgb  29506  vtxduhgr0nedg  29510  1loopgrvd2  29521  1egrvtxdg0  29529  uspgrloopvtxel  29534  vtxdginducedm1lem4  29560  wlk1walk  29657  wlkp1lem1  29691  pthdivtx  29747  0enwwlksnge1  29884  umgrwwlks2on  29977  rusgr0edg  29993  eleclclwwlkn  30095  upgr4cycl4dv4e  30204  1conngr  30213  vdn0conngrumgrv2  30215  eupth2eucrct  30236  eupth2lem1  30237  frgrncvvdeqlem7  30324  frgrncvvdeqlem9  30326  frgrwopregasn  30335  frgrwopregbsn  30336  l2p  30498  lpni  30499  issh  31227  pjoc1  31453  h1dn0  31571  spansneleqi  31588  nonbooli  31670  pjch  31713  pjnel  31745  cdjreui  32451  rexunirn  32511  rabsnel  32519  nelun  32532  iinabrex  32582  opabdm  32623  opabrn  32624  fpwrelmapffslem  32743  fpwrelmap  32744  fz1nntr  32806  indval  32838  xrge0tsmsd  33065  nsgqusf1olem3  33443  elrspunidl  33456  isprmidl  33466  constrmon  33785  reff  33838  tpr2rico  33911  lmxrge0  33951  issiga  34113  isrnsiga  34114  isldsys  34157  isros  34169  issros  34176  ddeval1  34235  ddeval0  34236  ismbfm  34252  dya2icoseg  34279  dya2iocnrect  34283  ballotlem7  34538  bnj216  34746  bnj563  34757  bnj956  34790  bnj545  34909  bnj548  34911  bnj570  34919  bnj900  34943  bnj929  34950  bnj964  34957  bnj983  34965  bnj1001  34973  bnj1145  35007  bnj1398  35048  bnj1498  35075  wevgblacfn  35114  erdszelem1  35196  kur14lem9  35219  cnllysconn  35250  cvmsss2  35279  cvmcov2  35280  cvmsiota  35282  cvmopnlem  35283  cvmliftlem15  35303  satfv1  35368  satfdmlem  35373  mclsssvlem  35567  mclsind  35575  untelirr  35708  untsucf  35710  elintfv  35765  dfon2lem4  35787  dfon2lem7  35790  dfon2lem9  35792  dfiota3  35924  funpartlem  35943  funpartfun  35944  linethru  36154  hilbert1.1  36155  rankelg  36169  elhf2  36176  neibastop2lem  36361  bj-zfauscl  36925  bj-cleq  36963  bj-snsetex  36964  bj-clel3gALT  37049  bj-nuliota  37058  bj-isrvec  37295  mptsnunlem  37339  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlssretop  37364  relowlpssretop  37365  exrecfnlem  37380  finxpeq1  37387  finxpreclem5  37396  finxpreclem6  37397  nlpineqsn  37409  fvineqsneq  37413  pibt2  37418  unccur  37610  fin2so  37614  matunitlindflem1  37623  ptrecube  37627  poimirlem9  37636  poimirlem30  37657  poimir  37660  heicant  37662  mblfinlem1  37664  ftc1anc  37708  ftc2nc  37709  cover2  37722  isbnd2  37790  prdstotbnd  37801  heibor1lem  37816  grpokerinj  37900  rngoueqz  37947  isidl  38021  1idl  38033  0rngo  38034  ispridl  38041  smprngopr  38059  isfldidl  38075  isdmn3  38081  mpobi123f  38169  iineq12f  38171  mptbi12f  38173  eqvrelqsel  38617  n0eldmqseq  38650  dmqseqim2  38658  disjlem17  38800  lsateln0  38996  ispsubsp  39747  linepsubN  39754  elpcliN  39895  dvh3dim3N  41451  dochsnnz  41452  mapdindp3  41724  sn-iotalem  42260  prjspval  42613  elmzpcl  42737  diophren  42824  dford3lem2  43039  ttac  43048  pw2f1ocnv  43049  wepwsolem  43054  kelac1  43075  onexgt  43252  onexlimgt  43255  ordnexbtwnsuc  43280  oaordnr  43309  omnord1  43318  nnoeomeqom  43325  oenord1  43329  succlg  43341  oacl2g  43343  omabs2  43345  omcl2  43346  omcl3g  43347  naddwordnexlem4  43414  nlimsuc  43454  intabssd  43532  elmapintrab  43589  eliunov2  43692  gneispaceel2  44157  mnuop23d  44285  mnuunid  44296  mnurndlem1  44300  expgrowthi  44352  dvconstbi  44353  tratrb  44556  suctrALT2VD  44856  suctrALT2  44857  en3lplem1VD  44863  en3lpVD  44865  tratrbVD  44881  suctrALTcf  44942  suctrALTcfVD  44943  suctrALT3  44944  unisnALT  44946  0elaxnul  45000  pwclaxpow  45001  prclaxpr  45002  uniclaxun  45003  omssaxinf2  45005  wfaxrep  45011  restuni3  45123  supminfxr  45475  xlimxrre  45846  xlimmnfvlem1  45847  xlimpnfvlem1  45851  icccncfext  45902  stoweidlem27  46042  stoweidlem35  46050  stoweidlem46  46061  stoweidlem52  46067  ioorrnopnlem  46319  ioorrnopnxrlem  46321  issal  46329  intsaluni  46344  salgencntex  46358  smfresal  46803  funressnfv  47055  fnbrafvb  47166  afvco2  47188  ndmaovg  47196  aovmpt4g  47213  fafv2elrnb  47247  fvelsetpreimafv  47374  elsetpreimafvbi  47378  sprsymrelf1lem  47478  paireqne  47498  fpprbasnn  47716  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  dfclnbgr6  47842  dfsclnbgr6  47844  grtri  47907  stgrvtx0  47929  stgrnbgr0  47931  isubgr3stgrlem3  47935  gpgvtx0  48008  gpgvtx1  48009  gpg3kgrtriex  48045  rngccatidALTV  48188  ringccatidALTV  48222  ldepspr  48390  mosn  48732  indthinc  49109  indthincALT  49110