Theorem eleq2 2825

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleq12  2826  eleq2i  2828  nelneq2  2861  dvelimdc  2923  raleqf  3318  rmoeq1f  3379  rabeq  3403  rabeqd  3417  rabeqf  3423  clel3g  3603  clel4g  3605  sbcel2gv  3795  csbeq2  3842  difeq2  4060  uneq1  4101  unineq  4228  nel02  4279  sbnfc2  4379  disjel  4397  elif  4510  exsnrex  4624  elinsn  4654  sneqrg  4782  preq1b  4789  preq12b  4793  elpreqprb  4811  elunii  4855  elinti  4898  intss1  4905  intmin  4910  intab  4920  iuneqconst  4945  iineq2  4954  dfiun2g  4972  breq  5087  zfrepclf  5226  zfauscl  5233  sseliALT  5244  vneqv  5251  inuni  5291  selsALT  5393  rext  5400  intidg  5409  elopg  5419  opth1  5428  opthwiener  5468  xpeq1  5645  xpeq2  5652  0nelelxp  5666  opthprc  5695  ordtri1  6356  ordtri3  6359  nsuceq0  6408  suctr  6411  ordnbtwn  6418  funopg  6532  dffv2  6935  fveqdmss  7030  dffo4  7055  funopdmsn  7104  fnsnbOLD  7121  elunirn  7206  f1oiso  7306  canth  7321  eusvobj2  7359  mpoeq123  7439  ndmovg  7550  uniuni  7716  iunpw  7725  oneqmin  7754  onuninsuci  7791  nlimsucg  7793  limomss  7822  nnlim  7831  peano5  7844  unielxp  7980  cnvf1o  8061  soseq  8109  smoel  8300  smo11  8304  tz7.44-2  8346  nlim2  8425  ord1eln01  8431  ord2eln012  8432  oawordeulem  8489  oaordex  8493  omordi  8501  oneo  8516  oeordi  8523  oeoa  8533  oeoe  8535  nnmordi  8567  nnaordex  8574  nnaordex2  8575  omabs  8587  nnneo  8591  omsmolem  8593  elqsn0  8731  qsel  8743  mapsnd  8834  undifixp  8882  boxriin  8888  boxcutc  8889  pssnn  9103  fineqvlem  9176  fineqv  9177  en1eqsn  9185  fissuni  9267  dffi2  9336  inficl  9338  dffi3  9344  wofib  9460  zfregcl  9509  zfregclOLD  9510  nelaneq  9516  nelaneqOLD  9517  en3lplem1  9533  en3lp  9535  suc11reg  9540  inf0  9542  inf3lem2  9550  inf3lem3  9551  infeq5i  9557  axinf2  9561  dfom3  9568  elom3  9569  cantnfle  9592  oemapvali  9605  cantnflem1  9610  tc2  9661  r1sdom  9698  rankwflemb  9717  rankval3b  9750  rankunb  9774  rankuni2b  9777  cardlim  9896  cardprclem  9903  infxpenlem  9935  alephnbtwn  9993  alephordi  9996  cardaleph  10011  alephfp  10030  alephval3  10032  dfac3  10043  dfac5lem2  10046  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  kmlem2  10074  coflim  10183  cfsmolem  10192  fin23lem30  10264  isf34lem4  10299  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  zorn2lem7  10424  axdclem  10441  brdom7disj  10453  brdom6disj  10454  axpowndlem3  10522  winainflem  10616  iswun  10627  eltskg  10673  inar1  10698  elgrug  10715  inaprc  10759  eltskm  10766  addnidpi  10824  indpi  10830  nqereu  10852  elnp  10910  elnpi  10911  genpnnp  10928  ltaddpr  10957  indval  12162  dfnn2  12187  dfnn3  12188  dfuzi  12620  uz11  12813  elfzonlteqm1  13696  fzoopth  13717  om2uzlti  13912  axdc4uz  13946  hashrabsn1  14336  hashbclem  14414  hashf1lem2  14418  hash2prb  14434  hash2prd  14437  hash3tpb  14457  wrdsymb0  14511  lsw0  14527  swrdwrdsymb  14625  rtrclreclem3  15022  prodeq1f  15871  prodeq1  15872  rpnnen2lem1  16181  rpnnen2lem2  16182  lcmfval  16590  lcmf0val  16591  ismre  17552  isacs  17617  initoid  17968  termoid  17969  initoeu2lem1  17981  clatl  18474  mreclatBAD  18529  issubmgm  18670  issubm  18771  dfgrp2e  18939  isnsg  19130  cycsubg  19183  resghm  19207  ghmeql  19214  gsmsymgreq  19407  f1otrspeq  19422  pmtrval  19426  pmtrdifellem4  19454  pmtrprfval  19462  gsumzsplit  19902  pgpfac1lem1  20051  pgpfac1lem5  20056  pgpfac1  20057  ablsimpnosubgd  20081  c0snmgmhm  20442  c0snmhm  20443  0ring01eq  20506  issubrg  20548  lmodfopnelem2  20894  islss  20929  lspsneq0  21007  lmhmeql  21050  lspdisjb  21124  lidl1el  21224  rngqiprngfulem2  21310  rngqipring1  21314  lidldvgen  21332  islindf4  21818  mplcoe1  22015  mplcoe5  22018  selvfval  22100  m1detdiag  22562  mdetunilem9  22585  maducoeval2  22605  madugsum  22608  chpmat1dlem  22800  istopg  22860  toprntopon  22890  fiinbas  22917  topbas  22937  ppttop  22972  pptbas  22973  epttop  22974  elcls  23038  clsndisj  23040  iscldtop  23060  neiptopnei  23097  restbas  23123  restntr  23147  pnfnei  23185  mnfnei  23186  cnpimaex  23221  lmcvg  23227  iscnp4  23228  cncnpi  23243  cnconst2  23248  cnprest  23254  cnprest2  23255  cnpdis  23258  lmss  23263  lmff  23266  cnt0  23311  ist1-3  23314  cnhaus  23319  isreg2  23342  dishaus  23347  ordthauslem  23348  cmpsublem  23364  cmpsub  23365  cmpcld  23367  hauscmplem  23371  unconn  23394  conncompid  23396  conncompss  23398  1stcfb  23410  1stcrest  23418  2ndcctbss  23420  2ndcomap  23423  dis2ndc  23425  1stcelcls  23426  llyeq  23435  nllyeq  23436  restnlly  23447  islly2  23449  lly1stc  23461  dislly  23462  hauspwdom  23466  finlocfin  23485  unisngl  23492  dissnlocfin  23494  locfindis  23495  comppfsc  23497  llycmpkgen2  23515  txbas  23532  eltx  23533  ptpjopn  23577  ptclsg  23580  txcnp  23585  ptcnplem  23586  ptcnp  23587  txlly  23601  pthaus  23603  txtube  23605  txhaus  23612  txlm  23613  tx1stc  23615  txkgen  23617  xkohaus  23618  xkopt  23620  xkococnlem  23624  tgqtop  23677  kqfvima  23695  kqt0lem  23701  isr0  23702  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  reghmph  23758  fbssfi  23802  isfil  23812  filuni  23850  isufil  23868  isufil2  23873  fixufil  23887  uffixfr  23888  uffixsn  23890  rnelfm  23918  flimopn  23940  flimrest  23948  flimcls  23950  txflf  23971  fclsopni  23980  fclsrest  23989  fclscf  23990  fcfnei  24000  alexsublem  24009  alexsubALTlem3  24014  alexsubALT  24016  tmdgsum2  24061  symgtgp  24071  subgntr  24072  opnsubg  24073  ghmcnp  24080  tgpt0  24084  qustgpopn  24085  tsmsi  24099  tsmssubm  24108  tsmssplit  24117  isust  24169  ustn0  24186  blssps  24389  blss  24390  blssexps  24391  blssex  24392  neibl  24466  blcld  24470  metss  24473  methaus  24485  met1stc  24486  met2ndci  24487  metrest  24489  prdsxmslem2  24494  metcnp3  24505  dscopn  24538  idnghm  24708  qdensere  24734  tgioo  24761  tgqioo  24765  zdis  24782  xrge0tsms  24800  cnheibor  24922  lmmbr  25225  bcthlem4  25294  ovolicc2lem5  25488  dyadmbllem  25566  i1fd  25648  itg11  25658  itg2gt0  25727  itgeq1f  25738  itgeq1fOLD  25739  itgeq1  25740  bddmulibl  25806  ellimc2  25844  limcnlp  25845  ellimc3  25846  limcflf  25848  limciun  25861  lhop1lem  25980  ig1pdvds  26145  plycpn  26255  aannenlem2  26295  efopn  26622  xrlimcnp  26932  wilthlem2  27032  wilthlem3  27033  nodenselem8  27655  noetasuplem4  27700  noetainflem4  27704  nocvxminlem  27746  lrrecfr  27935  addsprop  27968  bdayons  28268  addonbday  28271  dfn0s2  28324  tghilberti1  28705  colline  28717  lmif  28853  islmib  28855  incistruhgr  29148  upgr1eopALT  29186  uhgrvtxedgiedgb  29205  upgredg2vtx  29210  edglnl  29212  numedglnl  29213  uhgr2edg  29277  umgrvad2edg  29282  usgredg4  29286  usgredg2vtxeuALT  29291  uspgredg2vlem  29292  ushgredgedg  29298  nbgr1vtx  29427  nbusgredgeu0  29437  nbusgrf1o0  29438  nb3grprlem1  29449  nb3grprlem2  29450  uvtx01vtx  29466  nbupgruvtxres  29476  cplgr1vlem  29498  cplgr1v  29499  vtxd0nedgb  29557  vtxduhgr0nedg  29561  1loopgrvd2  29572  1egrvtxdg0  29580  uspgrloopvtxel  29585  vtxdginducedm1lem4  29611  wlk1walk  29707  wlkp1lem1  29740  pthdivtx  29795  0enwwlksnge1  29932  usgrwwlks2on  30026  umgrwwlks2on  30027  rusgr0edg  30044  eleclclwwlkn  30146  upgr4cycl4dv4e  30255  1conngr  30264  vdn0conngrumgrv2  30266  eupth2eucrct  30287  eupth2lem1  30288  frgrncvvdeqlem7  30375  frgrncvvdeqlem9  30377  frgrwopregasn  30386  frgrwopregbsn  30387  l2p  30550  lpni  30551  issh  31279  pjoc1  31505  h1dn0  31623  spansneleqi  31640  nonbooli  31722  pjch  31765  pjnel  31797  cdjreui  32503  rexunirn  32561  rabsnel  32570  nelun  32583  iinabrex  32639  opabdm  32684  opabrn  32685  fpwrelmapffslem  32805  fpwrelmap  32806  fz1nntr  32875  xrge0tsmsd  33134  nsgqusf1olem3  33475  elrspunidl  33488  isprmidl  33498  constrmon  33888  reff  33983  tpr2rico  34056  lmxrge0  34096  issiga  34256  isrnsiga  34257  isldsys  34300  isros  34312  issros  34319  ddeval1  34378  ddeval0  34379  ismbfm  34395  dya2icoseg  34421  dya2iocnrect  34425  ballotlem7  34680  bnj216  34875  bnj563  34886  bnj956  34919  bnj545  35037  bnj548  35039  bnj570  35047  bnj900  35071  bnj929  35078  bnj964  35085  bnj983  35093  bnj1001  35101  bnj1145  35135  bnj1398  35176  bnj1498  35203  fineqvnttrclselem2  35266  fineqvnttrclse  35268  fineqvinfep  35269  wevgblacfn  35291  erdszelem1  35373  kur14lem9  35396  cnllysconn  35427  cvmsss2  35456  cvmcov2  35457  cvmsiota  35459  cvmopnlem  35460  cvmliftlem15  35480  satfv1  35545  satfdmlem  35550  mclsssvlem  35744  mclsind  35752  untelirr  35890  untsucf  35892  elintfv  35947  dfon2lem4  35966  dfon2lem7  35969  dfon2lem9  35971  dfiota3  36103  funpartlem  36124  funpartfun  36125  linethru  36335  hilbert1.1  36336  rankelg  36350  elhf2  36357  neibastop2lem  36542  regsfromregtco  36720  regsfromunir1  36722  bj-zfauscl  37231  bj-cleq  37269  bj-snsetex  37270  bj-clel3gALT  37355  bj-nuliota  37364  bj-isrvec  37608  mptsnunlem  37654  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  relowlpssretop  37680  exrecfnlem  37695  finxpeq1  37702  finxpreclem5  37711  finxpreclem6  37712  nlpineqsn  37724  fvineqsneq  37728  pibt2  37733  unccur  37924  fin2so  37928  matunitlindflem1  37937  ptrecube  37941  poimirlem9  37950  poimirlem30  37971  poimir  37974  heicant  37976  mblfinlem1  37978  ftc1anc  38022  ftc2nc  38023  cover2  38036  isbnd2  38104  prdstotbnd  38115  heibor1lem  38130  grpokerinj  38214  rngoueqz  38261  isidl  38335  1idl  38347  0rngo  38348  ispridl  38355  smprngopr  38373  isfldidl  38389  isdmn3  38395  mpobi123f  38483  iineq12f  38485  mptbi12f  38487  dfsuccl4  38795  eqvrelqsel  39021  n0eldmqseq  39055  dmqseqim2  39063  suceldisj  39139  disjlem17  39223  lsateln0  39441  ispsubsp  40191  linepsubN  40198  elpcliN  40339  dvh3dim3N  41895  dochsnnz  41896  mapdindp3  42168  sn-iotalem  42662  prjspval  43036  elmzpcl  43158  diophren  43241  dford3lem2  43455  ttac  43464  pw2f1ocnv  43465  wepwsolem  43470  kelac1  43491  onexgt  43668  onexlimgt  43671  ordnexbtwnsuc  43695  oaordnr  43724  omnord1  43733  nnoeomeqom  43740  oenord1  43744  succlg  43756  oacl2g  43758  omabs2  43760  omcl2  43761  omcl3g  43762  naddwordnexlem4  43829  nlimsuc  43868  intabssd  43946  elmapintrab  44003  eliunov2  44106  gneispaceel2  44571  mnuop23d  44693  mnuunid  44704  mnurndlem1  44708  expgrowthi  44760  dvconstbi  44761  tratrb  44963  suctrALT2VD  45262  suctrALT2  45263  en3lplem1VD  45269  en3lpVD  45271  tratrbVD  45287  suctrALTcf  45348  suctrALTcfVD  45349  suctrALT3  45350  unisnALT  45352  0elaxnul  45410  pwclaxpow  45411  prclaxpr  45412  uniclaxun  45413  omssaxinf2  45415  wfaxrep  45421  restuni3  45548  supminfxr  45892  xlimxrre  46259  xlimmnfvlem1  46260  xlimpnfvlem1  46264  icccncfext  46315  stoweidlem27  46455  stoweidlem35  46463  stoweidlem46  46474  stoweidlem52  46480  ioorrnopnlem  46732  ioorrnopnxrlem  46734  issal  46742  intsaluni  46757  salgencntex  46771  smfresal  47216  tannpoly  47338  funressnfv  47491  fnbrafvb  47602  afvco2  47624  ndmaovg  47632  aovmpt4g  47649  fafv2elrnb  47683  fvelsetpreimafv  47847  elsetpreimafvbi  47851  sprsymrelf1lem  47951  paireqne  47971  fpprbasnn  48205  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  dfclnbgr6  48332  dfsclnbgr6  48334  grtri  48416  stgrvtx0  48438  stgrnbgr0  48440  isubgr3stgrlem3  48444  gpgvtx0  48529  gpgvtx1  48530  gpg3kgrtriex  48565  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  rngccatidALTV  48748  ringccatidALTV  48782  ldepspr  48949  mosn  49288  indthinc  49937  indthincALT  49938