Theorem eleq2 2827

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  eleq12  2828  eleq2i  2830  nelneq2  2863  clelsb2OLD  2867  dvelimdc  2927  raleqf  3350  rexeqfOLD  3352  rmoeq1OLD  3415  reueq1OLD  3416  rmoeq1f  3420  rabeq  3447  rabeqd  3462  rabeqf  3469  clel3g  3660  clel4g  3662  sbcbi2  3853  sbcel2gv  3862  csbeq2  3912  difeq2  4129  uneq1  4170  unineq  4293  nel02  4344  n0i  4345  sbnfc2  4444  disjel  4462  elif  4573  exsnrex  4684  elinsn  4714  sneqrg  4843  preq1b  4850  preq12b  4854  elpreqprb  4872  elunii  4916  elinti  4959  intss1  4967  intmin  4972  intab  4982  iuneqconst  5007  iineq2  5016  dfiun2g  5034  dfiin2g  5036  breq  5149  zfrepclf  5296  zfauscl  5303  sseliALT  5314  inuni  5355  selsALT  5449  rext  5458  intidg  5467  intidOLD  5468  elopg  5476  opth1  5485  opthwiener  5523  xpeq1  5702  xpeq2  5709  0nelelxp  5723  opthprc  5752  ordtri1  6418  ordtri3  6421  nsuceq0  6468  suctr  6471  ordnbtwn  6478  funopg  6601  dffv2  7003  fveqdmss  7097  dffo4  7122  funopdmsn  7169  fnsnb  7185  elunirn  7270  f1oiso  7370  canth  7384  eusvobj2  7422  mpoeq123  7504  ndmovg  7615  uniuni  7780  iunpw  7789  oneqmin  7819  onuninsuci  7860  nlimsucg  7862  limomss  7891  nnlim  7900  peano5  7915  unielxp  8050  cnvf1o  8134  soseq  8182  smoel  8398  smo11  8402  tz7.44-2  8445  nlim2  8526  ord1eln01  8532  ord2eln012  8533  oawordeulem  8590  oaordex  8594  omordi  8602  oneo  8617  oeordi  8623  oeoa  8633  oeoe  8635  nnmordi  8667  nnaordex  8674  nnaordex2  8675  omabs  8687  nnneo  8691  omsmolem  8693  elqsn0  8824  qsel  8834  mapsnd  8924  undifixp  8972  boxriin  8978  boxcutc  8979  pssnn  9206  fineqvlem  9295  fineqv  9296  en1eqsn  9305  fissuni  9394  dffi2  9460  inficl  9462  dffi3  9468  wofib  9582  zfregcl  9631  en3lplem1  9649  en3lp  9651  suc11reg  9656  inf0  9658  inf3lem2  9666  inf3lem3  9667  infeq5i  9673  axinf2  9677  dfom3  9684  elom3  9685  cantnfle  9708  oemapvali  9721  cantnflem1  9726  tc2  9779  r1sdom  9811  rankwflemb  9830  rankval3b  9863  rankunb  9887  rankuni2b  9890  cardlim  10009  cardprclem  10016  infxpenlem  10050  alephnbtwn  10108  alephordi  10111  cardaleph  10126  alephfp  10145  alephval3  10147  dfac3  10158  dfac5lem2  10161  dfac5lem4  10163  dfac5lem4OLD  10165  dfac2b  10168  kmlem2  10189  coflim  10298  cfsmolem  10307  fin23lem30  10379  isf34lem4  10414  axdc2lem  10485  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  zorn2lem7  10539  axdclem  10556  brdom7disj  10568  brdom6disj  10569  axpowndlem3  10636  winainflem  10730  iswun  10741  eltskg  10787  inar1  10812  elgrug  10829  inaprc  10873  eltskm  10880  addnidpi  10938  indpi  10944  nqereu  10966  elnp  11024  elnpi  11025  genpnnp  11042  ltaddpr  11071  dfnn2  12276  dfnn3  12277  dfuzi  12706  uz11  12900  elfzonlteqm1  13776  fzoopth  13797  om2uzlti  13987  axdc4uz  14021  hashrabsn1  14409  hashbclem  14487  hashf1lem2  14491  hash2prb  14507  hash2prd  14510  hash3tpb  14530  wrdsymb0  14583  lsw0  14599  swrdwrdsymb  14696  rtrclreclem3  15095  prodeq1f  15938  prodeq1  15939  rpnnen2lem1  16246  rpnnen2lem2  16247  lcmfval  16654  lcmf0val  16655  ismre  17634  isacs  17695  initoid  18054  termoid  18055  initoeu2lem1  18067  clatl  18565  mreclatBAD  18620  issubmgm  18727  issubm  18828  dfgrp2e  18993  isnsg  19185  cycsubg  19238  resghm  19262  ghmeql  19269  gsmsymgreq  19464  f1otrspeq  19479  pmtrval  19483  pmtrdifellem4  19511  pmtrprfval  19519  gsumzsplit  19959  pgpfac1lem1  20108  pgpfac1lem5  20113  pgpfac1  20114  ablsimpnosubgd  20138  c0snmgmhm  20478  c0snmhm  20479  0ring01eq  20545  issubrg  20587  lmodfopnelem2  20913  islss  20949  lspsneq0  21027  lmhmeql  21071  lspdisjb  21145  lidl1el  21253  rngqiprngfulem2  21339  rngqipring1  21343  lidldvgen  21361  islindf4  21875  mplcoe1  22072  mplcoe5  22075  selvfval  22155  m1detdiag  22618  mdetunilem9  22641  maducoeval2  22661  madugsum  22664  chpmat1dlem  22856  istopg  22916  toprntopon  22946  fiinbas  22974  topbas  22994  ppttop  23029  pptbas  23030  epttop  23031  elcls  23096  clsndisj  23098  iscldtop  23118  neiptopnei  23155  restbas  23181  restntr  23205  pnfnei  23243  mnfnei  23244  cnpimaex  23279  lmcvg  23285  iscnp4  23286  cncnpi  23301  cnconst2  23306  cnprest  23312  cnprest2  23313  cnpdis  23316  lmss  23321  lmff  23324  cnt0  23369  ist1-3  23372  cnhaus  23377  isreg2  23400  dishaus  23405  ordthauslem  23406  cmpsublem  23422  cmpsub  23423  cmpcld  23425  hauscmplem  23429  unconn  23452  conncompid  23454  conncompss  23456  1stcfb  23468  1stcrest  23476  2ndcctbss  23478  2ndcomap  23481  dis2ndc  23483  1stcelcls  23484  llyeq  23493  nllyeq  23494  restnlly  23505  islly2  23507  lly1stc  23519  dislly  23520  hauspwdom  23524  finlocfin  23543  unisngl  23550  dissnlocfin  23552  locfindis  23553  comppfsc  23555  llycmpkgen2  23573  txbas  23590  eltx  23591  ptpjopn  23635  ptclsg  23638  txcnp  23643  ptcnplem  23644  ptcnp  23645  txlly  23659  pthaus  23661  txtube  23663  txhaus  23670  txlm  23671  tx1stc  23673  txkgen  23675  xkohaus  23676  xkopt  23678  xkococnlem  23682  tgqtop  23735  kqfvima  23753  kqt0lem  23759  isr0  23760  regr1lem  23762  kqreglem1  23764  kqreglem2  23765  reghmph  23816  fbssfi  23860  isfil  23870  filuni  23908  isufil  23926  isufil2  23931  fixufil  23945  uffixfr  23946  uffixsn  23948  rnelfm  23976  flimopn  23998  flimrest  24006  flimcls  24008  txflf  24029  fclsopni  24038  fclsrest  24047  fclscf  24048  fcfnei  24058  alexsublem  24067  alexsubALTlem3  24072  alexsubALT  24074  tmdgsum2  24119  symgtgp  24129  subgntr  24130  opnsubg  24131  ghmcnp  24138  tgpt0  24142  qustgpopn  24143  tsmsi  24157  tsmssubm  24166  tsmssplit  24175  isust  24227  ustn0  24244  blssps  24449  blss  24450  blssexps  24451  blssex  24452  neibl  24529  blcld  24533  metss  24536  methaus  24548  met1stc  24549  met2ndci  24550  metrest  24552  prdsxmslem2  24557  metcnp3  24568  dscopn  24601  idnghm  24779  qdensere  24805  tgioo  24831  tgqioo  24835  zdis  24851  xrge0tsms  24869  cnheibor  25000  lmmbr  25305  bcthlem4  25374  ovolicc2lem5  25569  dyadmbllem  25647  i1fd  25729  itg11  25739  itg2gt0  25809  itgeq1f  25820  itgeq1fOLD  25821  itgeq1  25822  bddmulibl  25888  ellimc2  25926  limcnlp  25927  ellimc3  25928  limcflf  25930  limciun  25943  lhop1lem  26066  ig1pdvds  26233  plycpn  26345  aannenlem2  26385  efopn  26714  xrlimcnp  27025  wilthlem2  27126  wilthlem3  27127  nodenselem8  27750  noetasuplem4  27795  noetainflem4  27799  nocvxminlem  27836  lrrecfr  27990  addsprop  28023  dfn0s2  28350  tghilberti1  28659  colline  28671  lmif  28807  islmib  28809  incistruhgr  29110  upgr1eopALT  29148  uhgrvtxedgiedgb  29167  upgredg2vtx  29172  edglnl  29174  numedglnl  29175  uhgr2edg  29239  umgrvad2edg  29244  usgredg4  29248  usgredg2vtxeuALT  29253  uspgredg2vlem  29254  ushgredgedg  29260  nbgr1vtx  29389  nbusgredgeu0  29399  nbusgrf1o0  29400  nb3grprlem1  29411  nb3grprlem2  29412  uvtx01vtx  29428  nbupgruvtxres  29438  cplgr1vlem  29460  cplgr1v  29461  vtxd0nedgb  29520  vtxduhgr0nedg  29524  1loopgrvd2  29535  1egrvtxdg0  29543  uspgrloopvtxel  29548  vtxdginducedm1lem4  29574  wlk1walk  29671  wlkp1lem1  29705  pthdivtx  29761  0enwwlksnge1  29893  umgrwwlks2on  29986  rusgr0edg  30002  eleclclwwlkn  30104  upgr4cycl4dv4e  30213  1conngr  30222  vdn0conngrumgrv2  30224  eupth2eucrct  30245  eupth2lem1  30246  frgrncvvdeqlem7  30333  frgrncvvdeqlem9  30335  frgrwopregasn  30344  frgrwopregbsn  30345  l2p  30507  lpni  30508  issh  31236  pjoc1  31462  h1dn0  31580  spansneleqi  31597  nonbooli  31679  pjch  31722  pjnel  31754  cdjreui  32460  rexunirn  32519  rabsnel  32527  nelun  32540  iinabrex  32588  opabdm  32630  opabrn  32631  fpwrelmapffslem  32749  fpwrelmap  32750  fz1nntr  32811  xrge0tsmsd  33047  nsgqusf1olem3  33422  elrspunidl  33435  isprmidl  33445  constrmon  33748  reff  33799  tpr2rico  33872  lmxrge0  33912  indval  33993  issiga  34092  isrnsiga  34093  isldsys  34136  isros  34148  issros  34155  ddeval1  34214  ddeval0  34215  ismbfm  34231  dya2icoseg  34258  dya2iocnrect  34262  ballotlem7  34516  bnj216  34724  bnj563  34735  bnj956  34768  bnj545  34887  bnj548  34889  bnj570  34897  bnj900  34921  bnj929  34928  bnj964  34935  bnj983  34943  bnj1001  34951  bnj1145  34985  bnj1398  35026  bnj1498  35053  wevgblacfn  35092  erdszelem1  35175  kur14lem9  35198  cnllysconn  35229  cvmsss2  35258  cvmcov2  35259  cvmsiota  35261  cvmopnlem  35262  cvmliftlem15  35282  satfv1  35347  satfdmlem  35352  mclsssvlem  35546  mclsind  35554  untelirr  35687  untsucf  35689  elintfv  35745  dfon2lem4  35767  dfon2lem7  35770  dfon2lem9  35772  dfiota3  35904  funpartlem  35923  funpartfun  35924  linethru  36134  hilbert1.1  36135  rankelg  36149  elhf2  36156  neibastop2lem  36342  bj-zfauscl  36906  bj-cleq  36944  bj-snsetex  36945  bj-clel3gALT  37030  bj-nuliota  37039  bj-isrvec  37276  mptsnunlem  37320  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlssretop  37345  relowlpssretop  37346  exrecfnlem  37361  finxpeq1  37368  finxpreclem5  37377  finxpreclem6  37378  nlpineqsn  37390  fvineqsneq  37394  pibt2  37399  unccur  37589  fin2so  37593  matunitlindflem1  37602  ptrecube  37606  poimirlem9  37615  poimirlem30  37636  poimir  37639  heicant  37641  mblfinlem1  37643  ftc1anc  37687  ftc2nc  37688  cover2  37701  isbnd2  37769  prdstotbnd  37780  heibor1lem  37795  grpokerinj  37879  rngoueqz  37926  isidl  38000  1idl  38012  0rngo  38013  ispridl  38020  smprngopr  38038  isfldidl  38054  isdmn3  38060  mpobi123f  38148  iineq12f  38150  mptbi12f  38152  eqvrelqsel  38597  n0eldmqseq  38630  dmqseqim2  38638  disjlem17  38780  lsateln0  38976  ispsubsp  39727  linepsubN  39734  elpcliN  39875  dvh3dim3N  41431  dochsnnz  41432  mapdindp3  41704  sn-iotalem  42238  prjspval  42589  elmzpcl  42713  diophren  42800  dford3lem2  43015  ttac  43024  pw2f1ocnv  43025  wepwsolem  43030  kelac1  43051  onexgt  43228  onexlimgt  43231  ordnexbtwnsuc  43256  oaordnr  43285  omnord1  43294  nnoeomeqom  43301  oenord1  43305  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  omcl3g  43323  naddwordnexlem4  43390  nlimsuc  43430  intabssd  43508  elmapintrab  43565  eliunov2  43668  gneispaceel2  44133  mnuop23d  44261  mnuunid  44272  mnurndlem1  44276  expgrowthi  44328  dvconstbi  44329  tratrb  44533  suctrALT2VD  44833  suctrALT2  44834  en3lplem1VD  44840  en3lpVD  44842  tratrbVD  44858  suctrALTcf  44919  suctrALTcfVD  44920  suctrALT3  44921  unisnALT  44923  prclaxpr  44947  wfaxrep  44949  restuni3  45057  supminfxr  45413  xlimxrre  45786  xlimmnfvlem1  45787  xlimpnfvlem1  45791  icccncfext  45842  stoweidlem27  45982  stoweidlem35  45990  stoweidlem46  46001  stoweidlem52  46007  ioorrnopnlem  46259  ioorrnopnxrlem  46261  issal  46269  intsaluni  46284  salgencntex  46298  smfresal  46743  funressnfv  46992  fnbrafvb  47103  afvco2  47125  ndmaovg  47133  aovmpt4g  47150  fafv2elrnb  47184  fvelsetpreimafv  47311  elsetpreimafvbi  47315  sprsymrelf1lem  47415  paireqne  47435  fpprbasnn  47653  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  dfclnbgr6  47779  dfsclnbgr6  47781  grtri  47844  stgrvtx0  47864  stgrnbgr0  47866  isubgr3stgrlem3  47870  gpgvtx0  47943  gpgvtx1  47944  rngccatidALTV  48115  ringccatidALTV  48149  ldepspr  48318  mosn  48660  indthinc  48852  indthincALT  48853