Theorem eleq2 2823

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eleq12  2824  eleq2i  2826  nelneq2  2859  clelsb2OLD  2863  dvelimdc  2931  raleleqOLD  3341  raleqf  3350  rexeqfOLD  3352  rmoeq1OLD  3417  reueq1OLD  3418  rmoeq1f  3421  rabeq  3447  rabeqd  3461  rabeqf  3467  rabeqiOLD  3472  clel3g  3650  clel4g  3652  clel4OLD  3654  sbcbi2  3839  sbcel2gv  3849  csbeq2  3898  difeq2  4116  uneq1  4156  unineq  4277  nel02  4332  n0i  4333  sbnfc2  4436  disjel  4456  elif  4571  exsnrex  4684  elinsn  4714  sneqrg  4840  preq1b  4847  preq12b  4851  elpreqprb  4868  elunii  4913  elinti  4959  intss1  4967  intmin  4972  intab  4982  iuneqconst  5008  iineq2  5017  dfiun2g  5033  dfiin2g  5035  breq  5150  zfrepclf  5294  zfauscl  5301  sseliALT  5309  inuni  5343  selsALT  5439  rext  5448  intidg  5457  intidOLD  5458  elopg  5466  opth1  5475  opthwiener  5514  xpeq1  5690  xpeq2  5697  0nelelxp  5711  opthprc  5739  ordtri1  6395  ordtri3  6398  nsuceq0  6445  suctr  6448  ordnbtwn  6455  funopg  6580  dffv2  6984  fveqdmss  7078  dffo4  7102  funopdmsn  7145  fnsnb  7161  elunirn  7247  f1oiso  7345  canth  7359  eusvobj2  7398  mpoeq123  7478  ndmovg  7587  uniuni  7746  iunpw  7755  oneqmin  7785  onuninsuci  7826  nlimsucg  7828  limomss  7857  nnlim  7866  peano5  7881  peano5OLD  7882  unielxp  8010  cnvf1o  8094  soseq  8142  smoel  8357  smo11  8361  tz7.44-2  8404  nlim2  8487  ord1eln01  8493  ord2eln012  8494  oawordeulem  8551  oaordex  8555  omordi  8563  oneo  8578  oeordi  8584  oeoa  8594  oeoe  8596  nnmordi  8628  nnaordex  8635  omabs  8647  nnneo  8651  omsmolem  8653  elqsn0  8777  qsel  8787  mapsnd  8877  undifixp  8925  boxriin  8931  boxcutc  8932  pssnn  9165  fineqvlem  9259  fineqv  9260  pssnnOLD  9262  en1eqsn  9271  fissuni  9354  dffi2  9415  inficl  9417  dffi3  9423  wofib  9537  zfregcl  9586  en3lplem1  9604  en3lp  9606  suc11reg  9611  inf0  9613  inf3lem2  9621  inf3lem3  9622  infeq5i  9628  axinf2  9632  dfom3  9639  elom3  9640  cantnfle  9663  oemapvali  9676  cantnflem1  9681  tc2  9734  r1sdom  9766  rankwflemb  9785  rankval3b  9818  rankunb  9842  rankuni2b  9845  cardlim  9964  cardprclem  9971  infxpenlem  10005  alephnbtwn  10063  alephordi  10066  cardaleph  10081  alephfp  10100  alephval3  10102  dfac3  10113  dfac5lem2  10116  dfac5lem4  10118  dfac2b  10122  kmlem2  10143  coflim  10253  cfsmolem  10262  fin23lem30  10334  isf34lem4  10369  axdc2lem  10440  axdc3lem2  10443  axdc3lem4  10445  axdc4lem  10447  zorn2lem7  10494  axdclem  10511  brdom7disj  10523  brdom6disj  10524  axpowndlem3  10591  winainflem  10685  iswun  10696  eltskg  10742  inar1  10767  elgrug  10784  inaprc  10828  eltskm  10835  addnidpi  10893  indpi  10899  nqereu  10921  elnp  10979  elnpi  10980  genpnnp  10997  ltaddpr  11026  dfnn2  12222  dfnn3  12223  dfuzi  12650  uz11  12844  elfzonlteqm1  13705  om2uzlti  13912  axdc4uz  13946  hashrabsn1  14331  hashbclem  14408  hashf1lem2  14414  hash2prb  14430  hash2prd  14433  wrdsymb0  14496  lsw0  14512  swrdwrdsymb  14609  rtrclreclem3  15004  prodeq1f  15849  rpnnen2lem1  16154  rpnnen2lem2  16155  lcmfval  16555  lcmf0val  16556  ismre  17531  isacs  17592  initoid  17948  termoid  17949  initoeu2lem1  17961  clatl  18458  mreclatBAD  18513  issubm  18681  dfgrp2e  18845  isnsg  19030  cycsubg  19080  resghm  19103  ghmeql  19110  gsmsymgreq  19295  f1otrspeq  19310  pmtrval  19314  pmtrdifellem4  19342  pmtrprfval  19350  gsumzsplit  19790  pgpfac1lem1  19939  pgpfac1lem5  19944  pgpfac1  19945  ablsimpnosubgd  19969  0ring01eq  20297  issubrg  20356  lmodfopnelem2  20502  islss  20538  lspsneq0  20616  lmhmeql  20659  lspdisjb  20732  lidl1el  20834  lidldvgen  20886  islindf4  21385  mplcoe1  21584  mplcoe5  21587  selvfval  21672  m1detdiag  22091  mdetunilem9  22114  maducoeval2  22134  madugsum  22137  chpmat1dlem  22329  istopg  22389  toprntopon  22419  fiinbas  22447  topbas  22467  ppttop  22502  pptbas  22503  epttop  22504  elcls  22569  clsndisj  22571  iscldtop  22591  neiptopnei  22628  restbas  22654  restntr  22678  pnfnei  22716  mnfnei  22717  cnpimaex  22752  lmcvg  22758  iscnp4  22759  cncnpi  22774  cnconst2  22779  cnprest  22785  cnprest2  22786  cnpdis  22789  lmss  22794  lmff  22797  cnt0  22842  ist1-3  22845  cnhaus  22850  isreg2  22873  dishaus  22878  ordthauslem  22879  cmpsublem  22895  cmpsub  22896  cmpcld  22898  hauscmplem  22902  unconn  22925  conncompid  22927  conncompss  22929  1stcfb  22941  1stcrest  22949  2ndcctbss  22951  2ndcomap  22954  dis2ndc  22956  1stcelcls  22957  llyeq  22966  nllyeq  22967  restnlly  22978  islly2  22980  lly1stc  22992  dislly  22993  hauspwdom  22997  finlocfin  23016  unisngl  23023  dissnlocfin  23025  locfindis  23026  comppfsc  23028  llycmpkgen2  23046  txbas  23063  eltx  23064  ptpjopn  23108  ptclsg  23111  txcnp  23116  ptcnplem  23117  ptcnp  23118  txlly  23132  pthaus  23134  txtube  23136  txhaus  23143  txlm  23144  tx1stc  23146  txkgen  23148  xkohaus  23149  xkopt  23151  xkococnlem  23155  tgqtop  23208  kqfvima  23226  kqt0lem  23232  isr0  23233  regr1lem  23235  kqreglem1  23237  kqreglem2  23238  reghmph  23289  fbssfi  23333  isfil  23343  filuni  23381  isufil  23399  isufil2  23404  fixufil  23418  uffixfr  23419  uffixsn  23421  rnelfm  23449  flimopn  23471  flimrest  23479  flimcls  23481  txflf  23502  fclsopni  23511  fclsrest  23520  fclscf  23521  fcfnei  23531  alexsublem  23540  alexsubALTlem3  23545  alexsubALT  23547  tmdgsum2  23592  symgtgp  23602  subgntr  23603  opnsubg  23604  ghmcnp  23611  tgpt0  23615  qustgpopn  23616  tsmsi  23630  tsmssubm  23639  tsmssplit  23648  isust  23700  ustn0  23717  blssps  23922  blss  23923  blssexps  23924  blssex  23925  neibl  24002  blcld  24006  metss  24009  methaus  24021  met1stc  24022  met2ndci  24023  metrest  24025  prdsxmslem2  24030  metcnp3  24041  dscopn  24074  idnghm  24252  qdensere  24278  tgioo  24304  tgqioo  24308  zdis  24324  xrge0tsms  24342  cnheibor  24463  lmmbr  24767  bcthlem4  24836  ovolicc2lem5  25030  dyadmbllem  25108  i1fd  25190  itg11  25200  itg2gt0  25270  itgeq1f  25281  bddmulibl  25348  ellimc2  25386  limcnlp  25387  ellimc3  25388  limcflf  25390  limciun  25403  lhop1lem  25522  ig1pdvds  25686  plycpn  25794  aannenlem2  25834  efopn  26158  xrlimcnp  26463  wilthlem2  26563  wilthlem3  26564  nodenselem8  27184  noetasuplem4  27229  noetainflem4  27233  nocvxminlem  27269  lrrecfr  27417  addsprop  27450  tghilberti1  27878  colline  27890  lmif  28026  islmib  28028  incistruhgr  28329  upgr1eopALT  28367  uhgrvtxedgiedgb  28386  upgredg2vtx  28391  edglnl  28393  numedglnl  28394  uhgr2edg  28455  umgrvad2edg  28460  usgredg4  28464  usgredg2vtxeuALT  28469  uspgredg2vlem  28470  ushgredgedg  28476  nbgr1vtx  28605  nbusgredgeu0  28615  nbusgrf1o0  28616  nb3grprlem1  28627  nb3grprlem2  28628  uvtx01vtx  28644  nbupgruvtxres  28654  cplgr1vlem  28676  cplgr1v  28677  vtxd0nedgb  28735  vtxduhgr0nedg  28739  1loopgrvd2  28750  1egrvtxdg0  28758  uspgrloopvtxel  28763  vtxdginducedm1lem4  28789  wlk1walk  28886  wlkp1lem1  28920  pthdivtx  28976  0enwwlksnge1  29108  umgrwwlks2on  29201  rusgr0edg  29217  eleclclwwlkn  29319  upgr4cycl4dv4e  29428  1conngr  29437  vdn0conngrumgrv2  29439  eupth2eucrct  29460  eupth2lem1  29461  frgrncvvdeqlem7  29548  frgrncvvdeqlem9  29550  frgrwopregasn  29559  frgrwopregbsn  29560  l2p  29720  lpni  29721  issh  30449  pjoc1  30675  h1dn0  30793  spansneleqi  30810  nonbooli  30892  pjch  30935  pjnel  30967  cdjreui  31673  rexunirn  31720  rabsnel  31728  nelun  31739  iinabrex  31788  opabdm  31828  opabrn  31829  fpwrelmapffslem  31945  fpwrelmap  31946  fz1nntr  32003  xrge0tsmsd  32197  nsgqusf1olem3  32515  elrspunidl  32535  isprmidl  32545  reff  32808  tpr2rico  32881  lmxrge0  32921  indval  33000  issiga  33099  isrnsiga  33100  isldsys  33143  isros  33155  issros  33162  ddeval1  33221  ddeval0  33222  ismbfm  33238  dya2icoseg  33265  dya2iocnrect  33269  ballotlem7  33523  bnj216  33732  bnj563  33743  bnj956  33776  bnj545  33895  bnj548  33897  bnj570  33905  bnj900  33929  bnj929  33936  bnj964  33943  bnj983  33951  bnj1001  33959  bnj1145  33993  bnj1398  34034  bnj1498  34061  erdszelem1  34171  kur14lem9  34194  cnllysconn  34225  cvmsss2  34254  cvmcov2  34255  cvmsiota  34257  cvmopnlem  34258  cvmliftlem15  34278  satfv1  34343  satfdmlem  34348  mclsssvlem  34542  mclsind  34550  untelirr  34666  untsucf  34668  elintfv  34725  dfon2lem4  34747  dfon2lem7  34750  dfon2lem9  34752  dfiota3  34884  funpartlem  34903  funpartfun  34904  linethru  35114  hilbert1.1  35115  rankelg  35129  elhf2  35136  neibastop2lem  35234  bj-zfauscl  35793  bj-cleq  35832  bj-snsetex  35833  bj-clel3gALT  35918  bj-nuliota  35927  bj-isrvec  36164  mptsnunlem  36208  isbasisrelowllem1  36225  isbasisrelowllem2  36226  relowlssretop  36233  relowlpssretop  36234  exrecfnlem  36249  finxpeq1  36256  finxpreclem5  36265  finxpreclem6  36266  nlpineqsn  36278  fvineqsneu  36281  fvineqsneq  36282  pibt2  36287  unccur  36460  fin2so  36464  matunitlindflem1  36473  ptrecube  36477  poimirlem9  36486  poimirlem30  36507  poimir  36510  heicant  36512  mblfinlem1  36514  ftc1anc  36558  ftc2nc  36559  cover2  36572  isbnd2  36640  prdstotbnd  36651  heibor1lem  36666  grpokerinj  36750  rngoueqz  36797  isidl  36871  1idl  36883  0rngo  36884  ispridl  36891  smprngopr  36909  isfldidl  36925  isdmn3  36931  mpobi123f  37019  iineq12f  37021  mptbi12f  37023  eqvrelqsel  37475  n0eldmqseq  37508  dmqseqim2  37516  disjlem17  37658  lsateln0  37854  ispsubsp  38605  linepsubN  38612  elpcliN  38753  dvh3dim3N  40309  dochsnnz  40310  mapdindp3  40582  sn-iotalem  41035  prjspval  41342  elmzpcl  41450  diophren  41537  dford3lem2  41752  ttac  41761  pw2f1ocnv  41762  wepwsolem  41770  kelac1  41791  onexgt  41975  onexlimgt  41978  ordnexbtwnsuc  42003  oaordnr  42032  omnord1  42041  nnoeomeqom  42048  oenord1  42052  succlg  42064  oacl2g  42066  omabs2  42068  omcl2  42069  omcl3g  42070  naddwordnexlem4  42138  nlimsuc  42178  intabssd  42256  elmapintrab  42313  eliunov2  42416  gneispaceel2  42881  mnuop23d  43011  mnuunid  43022  mnurndlem1  43026  expgrowthi  43078  dvconstbi  43079  tratrb  43283  suctrALT2VD  43583  suctrALT2  43584  en3lplem1VD  43590  en3lpVD  43592  tratrbVD  43608  suctrALTcf  43669  suctrALTcfVD  43670  suctrALT3  43671  unisnALT  43673  restuni3  43793  supminfxr  44161  xlimxrre  44534  xlimmnfvlem1  44535  xlimpnfvlem1  44539  icccncfext  44590  stoweidlem27  44730  stoweidlem35  44738  stoweidlem46  44749  stoweidlem52  44755  ioorrnopnlem  45007  ioorrnopnxrlem  45009  issal  45017  intsaluni  45032  salgencntex  45046  sge0f1o  45085  smfresal  45491  funressnfv  45740  fnbrafvb  45849  afvco2  45871  ndmaovg  45879  aovmpt4g  45896  fafv2elrnb  45930  fzoopth  46022  fvelsetpreimafv  46042  elsetpreimafvbi  46046  sprsymrelf1lem  46146  paireqne  46166  fpprbasnn  46384  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  issubmgm  46546  c0snmgmhm  46699  c0snmhm  46700  rngccatidALTV  46841  ringccatidALTV  46904  ldepspr  47108  mosn  47451  indthinc  47626  indthincALT  47627