Theorem eleq2 2851

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  eleq12  2852  eleq2i  2854  nelneq2  2887  dvelimdc  2948  raleqf  3343  rmoeq1f  3404  rabeq  3428  rabeqd  3442  rabeqf  3448  clel3g  3620  clel4g  3622  sbcel2gv  3810  csbeq2  3857  difeq2  4074  uneq1  4114  unineq  4240  nel02  4291  sbnfc2  4393  disjel  4411  elif  4524  exsnrex  4639  elinsn  4669  sneqrg  4797  preq1b  4804  preq12b  4808  elpreqprb  4826  elunii  4870  elinti  4914  intss1  4921  intmin  4926  intab  4936  iuneqconst  4961  iineq2  4970  dfiun2g  4987  breq  5102  zfrepclf  5241  zfauscl  5248  sseliALT  5259  vneqv  5266  inuni  5306  selsALT  5408  rext  5415  intidg  5424  elopg  5434  opth1  5443  opthwiener  5483  xpeq1  5661  xpeq2  5668  0nelelxp  5682  opthprc  5711  ordtri1  6379  ordtri3  6382  nsuceq0  6431  suctr  6434  ordnbtwn  6441  funopg  6555  dffv2  6962  fveqdmss  7059  dffo4  7084  funopdmsn  7133  fnsnbOLD  7150  elunirn  7235  f1oiso  7335  canth  7350  eusvobj2  7388  mpoeq123  7468  ndmovg  7579  uniuni  7745  iunpw  7754  oneqmin  7783  onuninsuci  7820  nlimsucg  7822  limomss  7851  nnlim  7860  peano5  7874  unielxp  8008  cnvf1o  8090  soseq  8139  smoel  8331  smo11  8335  tz7.44-2  8378  nlim2  8459  ord1eln01  8465  ord2eln012  8466  oawordeulem  8523  oaordex  8527  omordi  8535  oneo  8550  oeordi  8557  oeoa  8567  oeoe  8569  nnmordi  8601  nnaordex  8608  nnaordex2  8609  omabs  8621  nnneo  8625  omsmolem  8627  elqsn0  8766  qsel  8778  mapsnd  8868  undifixp  8916  boxriin  8922  boxcutc  8923  pssnn  9137  fineqvlem  9210  fineqv  9211  en1eqsn  9219  fissuni  9300  dffi2  9369  inficl  9371  dffi3  9377  wofib  9493  zfregcl  9542  zfregclOLD  9543  nelaneq  9550  nelaneqOLD  9551  en3lplem1  9567  en3lp  9569  suc11reg  9574  inf0  9576  inf3lem2  9584  inf3lem3  9585  infeq5i  9591  axinf2  9595  dfom3  9602  elom3  9603  cantnfle  9626  oemapvali  9639  cantnflem1  9644  tc2  9695  r1sdom  9732  rankwflemb  9751  rankval3b  9784  rankunb  9808  rankuni2b  9811  cardlim  9930  cardprclem  9937  infxpenlem  9969  alephnbtwn  10027  alephordi  10030  cardaleph  10045  alephfp  10064  alephval3  10066  dfac3  10077  dfac5lem2  10080  dfac5lem4  10082  dfac5lem4OLD  10084  dfac2b  10087  kmlem2  10108  coflim  10218  cfsmolem  10227  fin23lem30  10299  isf34lem4  10334  axdc2lem  10405  axdc3lem2  10408  axdc3lem4  10410  axdc4lem  10412  zorn2lem7  10459  axdclem  10476  brdom7disj  10488  brdom6disj  10489  axpowndlem3  10557  winainflem  10651  iswun  10662  eltskg  10708  inar1  10733  elgrug  10750  inaprc  10794  eltskm  10801  addnidpi  10859  indpi  10865  nqereu  10887  elnp  10945  elnpi  10946  genpnnp  10963  ltaddpr  10992  indval  12198  dfnn2  12223  dfnn3  12224  dfuzi  12664  uz11  12864  elfzonlteqm1  13747  fzoopth  13768  om2uzlti  13963  axdc4uz  13997  hashrabsn1  14387  hashbclem  14465  hashf1lem2  14469  hash2prb  14485  hash2prd  14488  hash3tpb  14508  wrdsymb0  14562  lsw0  14578  swrdwrdsymb  14676  rtrclreclem3  15073  prodeq1f  15936  prodeq1  15937  rpnnen2lem1  16246  rpnnen2lem2  16247  lcmfval  16655  lcmf0val  16656  ismre  17618  isacs  17683  initoid  18034  termoid  18035  initoeu2lem1  18047  clatl  18540  mreclatBAD  18595  issubmgm  18736  issubm  18837  dfgrp2e  19005  isnsg  19196  cycsubg  19249  resghm  19272  ghmeql  19279  gsmsymgreq  19472  f1otrspeq  19487  pmtrval  19491  pmtrdifellem4  19519  pmtrprfval  19527  gsumzsplit  19967  pgpfac1lem1  20116  pgpfac1lem5  20121  pgpfac1  20122  ablsimpnosubgd  20146  c0snmgmhm  20511  c0snmhm  20512  0ring01eq  20579  issubrg  20621  lmodfopnelem2  20966  islss  21001  lspsneq0  21079  lmhmeql  21122  lspdisjb  21196  lidl1el  21296  rngqiprngfulem2  21382  rngqipring1  21386  lidldvgen  21404  islindf4  21890  mplcoe1  22090  mplcoe5  22093  selvfval  22172  m1detdiag  22657  mdetunilem9  22680  maducoeval2  22700  madugsum  22703  chpmat1dlem  22895  istopg  22955  toprntopon  22985  fiinbas  23012  topbas  23032  ppttop  23067  pptbas  23068  epttop  23069  elcls  23133  clsndisj  23135  iscldtop  23155  neiptopnei  23192  restbas  23218  restntr  23242  pnfnei  23280  mnfnei  23281  cnpimaex  23316  lmcvg  23322  iscnp4  23323  cncnpi  23338  cnconst2  23343  cnprest  23349  cnprest2  23350  cnpdis  23353  lmss  23358  lmff  23361  cnt0  23406  ist1-3  23409  cnhaus  23414  isreg2  23437  dishaus  23442  ordthauslem  23443  cmpsublem  23459  cmpsub  23460  cmpcld  23462  hauscmplem  23466  unconn  23489  conncompid  23491  conncompss  23493  1stcfb  23505  1stcrest  23513  2ndcctbss  23515  2ndcomap  23518  dis2ndc  23520  1stcelcls  23521  llyeq  23530  nllyeq  23531  restnlly  23542  islly2  23544  lly1stc  23556  dislly  23557  hauspwdom  23561  finlocfin  23580  unisngl  23587  dissnlocfin  23589  locfindis  23590  comppfsc  23592  llycmpkgen2  23610  txbas  23627  eltx  23628  ptpjopn  23672  ptclsg  23675  txcnp  23680  ptcnplem  23681  ptcnp  23682  txlly  23696  pthaus  23698  txtube  23700  txhaus  23707  txlm  23708  tx1stc  23710  txkgen  23712  xkohaus  23713  xkopt  23715  xkococnlem  23719  tgqtop  23772  kqfvima  23790  kqt0lem  23796  isr0  23797  regr1lem  23799  kqreglem1  23801  kqreglem2  23802  reghmph  23853  fbssfi  23897  isfil  23907  filuni  23945  isufil  23963  isufil2  23968  fixufil  23982  uffixfr  23983  uffixsn  23985  rnelfm  24013  flimopn  24035  flimrest  24043  flimcls  24045  txflf  24066  fclsopni  24075  fclsrest  24084  fclscf  24085  fcfnei  24095  alexsublem  24104  alexsubALTlem3  24109  alexsubALT  24111  tmdgsum2  24156  symgtgp  24166  subgntr  24167  opnsubg  24168  ghmcnp  24175  tgpt0  24179  qustgpopn  24180  tsmsi  24194  tsmssubm  24203  tsmssplit  24212  isust  24264  ustn0  24281  blssps  24484  blss  24485  blssexps  24486  blssex  24487  neibl  24561  blcld  24565  metss  24568  methaus  24580  met1stc  24581  met2ndci  24582  metrest  24584  prdsxmslem2  24589  metcnp3  24600  dscopn  24633  idnghm  24803  qdensere  24829  tgioo  24856  tgqioo  24860  zdis  24877  xrge0tsms  24895  cnheibor  25017  lmmbr  25320  bcthlem4  25389  ovolicc2lem5  25583  dyadmbllem  25661  i1fd  25743  itg11  25753  itg2gt0  25822  itgeq1f  25833  itgeq1fOLD  25834  itgeq1  25835  bddmulibl  25901  ellimc2  25939  limcnlp  25940  ellimc3  25941  limcflf  25943  limciun  25956  lhop1lem  26075  ig1pdvds  26240  plycpn  26353  aannenlem2  26393  efopn  26723  xrlimcnp  27033  wilthlem2  27133  wilthlem3  27134  nodenselem8  27755  noetasuplem4  27800  noetainflem4  27804  nocvxminlem  27847  lrrecfr  28036  addsprop  28069  bdayons  28369  addonbday  28372  dfn0s2  28425  tghilberti1  28806  colline  28819  lmif  28958  islmib  28960  incistruhgr  29280  upgr1eopALT  29318  uhgrvtxedgiedgb  29337  upgredg2vtx  29342  edglnl  29344  numedglnl  29345  uhgr2edg  29409  umgrvad2edg  29414  usgredg4  29418  usgredg2vtxeuALT  29423  uspgredg2vlem  29424  ushgredgedg  29430  nbgr1vtx  29559  nbusgredgeu0  29569  nbusgrf1o0  29570  nb3grprlem1  29581  nb3grprlem2  29582  uvtx01vtx  29598  nbupgruvtxres  29608  cplgr1vlem  29630  cplgr1v  29631  vtxd0nedgb  29689  vtxduhgr0nedg  29693  1loopgrvd2  29704  1egrvtxdg0  29712  uspgrloopvtxel  29717  vtxdginducedm1lem4  29743  wlk1walk  29839  wlkp1lem1  29872  pthdivtx  29927  0enwwlksnge1  30064  usgrwwlks2on  30158  umgrwwlks2on  30159  rusgr0edg  30176  eleclclwwlkn  30278  upgr4cycl4dv4e  30387  1conngr  30396  vdn0conngrumgrv2  30398  eupth2eucrct  30419  eupth2lem1  30420  frgrncvvdeqlem7  30507  frgrncvvdeqlem9  30509  frgrwopregasn  30518  frgrwopregbsn  30519  l2p  30682  lpni  30683  issh  31411  pjoc1  31637  h1dn0  31755  spansneleqi  31772  nonbooli  31854  pjch  31897  pjnel  31929  cdjreui  32635  rexunirn  32691  rabsnel  32699  nelun  32712  iinabrex  32769  opabdm  32813  opabrn  32814  fpwrelmapffslem  32934  fpwrelmap  32935  fz1nntr  33004  xrge0tsmsd  33253  nsgqusf1olem3  33601  elrspunidl  33614  isprmidl  33624  constrmon  34041  reff  34136  tpr2rico  34209  lmxrge0  34249  issiga  34409  isrnsiga  34410  isldsys  34453  isros  34465  issros  34472  ddeval1  34531  ddeval0  34532  ismbfm  34548  dya2icoseg  34574  dya2iocnrect  34578  ballotlem7  34833  bnj216  35028  bnj563  35039  bnj956  35072  bnj545  35190  bnj548  35192  bnj570  35200  bnj900  35224  bnj929  35231  bnj964  35238  bnj983  35246  bnj1001  35254  bnj1145  35288  bnj1398  35329  bnj1498  35356  fineqvnttrclselem2  35418  fineqvnttrclse  35420  fineqvinfep  35421  wevgblacfn  35454  erdszelem1  35541  kur14lem9  35564  cnllysconn  35595  cvmsss2  35624  cvmcov2  35625  cvmsiota  35627  cvmopnlem  35628  cvmliftlem15  35648  satfv1  35713  satfdmlem  35718  mclsssvlem  35912  mclsind  35920  untelirr  36058  untsucf  36060  elintfv  36115  dfon2lem4  36134  dfon2lem7  36137  dfon2lem9  36139  dfiota3  36271  funpartlem  36292  funpartfun  36293  linethru  36503  hilbert1.1  36504  rankelg  36518  elhf2  36525  neibastop2lem  36720  regsfromregtco  36898  regsfromunir1  36900  bj-zfauscl  37409  bj-cleq  37447  bj-snsetex  37448  bj-clel3gALT  37533  bj-nuliota  37542  bj-isrvec  37786  mptsnunlem  37832  isbasisrelowllem1  37849  isbasisrelowllem2  37850  relowlssretop  37857  relowlpssretop  37858  exrecfnlem  37873  finxpeq1  37880  finxpreclem5  37889  finxpreclem6  37890  nlpineqsn  37902  fvineqsneq  37906  pibt2  37911  unccur  38102  fin2so  38106  matunitlindflem1  38115  ptrecube  38119  poimirlem9  38128  poimirlem30  38149  poimir  38152  heicant  38154  mblfinlem1  38156  ftc1anc  38200  ftc2nc  38201  cover2  38214  isbnd2  38282  prdstotbnd  38293  heibor1lem  38308  grpokerinj  38392  rngoueqz  38439  isidl  38513  1idl  38525  0rngo  38526  ispridl  38533  smprngopr  38551  isfldidl  38567  isdmn3  38573  mpobi123f  38661  iineq12f  38663  mptbi12f  38665  dfsuccl4  38973  eqvrelqsel  39199  n0eldmqseq  39233  dmqseqim2  39241  suceldisj  39317  disjlem17  39401  lsateln0  39619  ispsubsp  40369  linepsubN  40376  elpcliN  40517  dvh3dim3N  42073  dochsnnz  42074  mapdindp3  42346  sn-iotalem  42840  prjspval  43185  elmzpcl  43307  diophren  43390  dford3lem2  43604  ttac  43613  pw2f1ocnv  43614  wepwsolem  43619  kelac1  43640  onexgt  43817  onexlimgt  43820  ordnexbtwnsuc  43844  oaordnr  43873  omnord1  43882  nnoeomeqom  43889  oenord1  43893  succlg  43905  oacl2g  43907  omabs2  43909  omcl2  43910  omcl3g  43911  naddwordnexlem4  43978  nlimsuc  44017  intabssd  44095  elmapintrab  44152  eliunov2  44255  gneispaceel2  44720  mnuop23d  44842  mnuunid  44853  mnurndlem1  44857  expgrowthi  44909  dvconstbi  44910  tratrb  45112  suctrALT2VD  45411  suctrALT2  45412  en3lplem1VD  45418  en3lpVD  45420  tratrbVD  45436  suctrALTcf  45497  suctrALTcfVD  45498  suctrALT3  45499  unisnALT  45501  0elaxnul  45559  pwclaxpow  45560  prclaxpr  45561  uniclaxun  45562  omssaxinf2  45564  wfaxrep  45570  restuni3  45696  supminfxr  46038  xlimxrre  46405  xlimmnfvlem1  46406  xlimpnfvlem1  46410  icccncfext  46461  stoweidlem27  46601  stoweidlem35  46609  stoweidlem46  46620  stoweidlem52  46626  ioorrnopnlem  46878  ioorrnopnxrlem  46880  issal  46888  intsaluni  46903  salgencntex  46917  smfresal  47362  tannpoly  47484  funressnfv  47637  fnbrafvb  47748  afvco2  47770  ndmaovg  47778  aovmpt4g  47795  fafv2elrnb  47829  fvelsetpreimafv  47993  elsetpreimafvbi  47997  sprsymrelf1lem  48097  paireqne  48117  fpprbasnn  48351  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  dfclnbgr6  48478  dfsclnbgr6  48480  grtri  48562  stgrvtx0  48584  stgrnbgr0  48586  isubgr3stgrlem3  48590  gpgvtx0  48675  gpgvtx1  48676  gpg3kgrtriex  48711  pgnbgreunbgrlem3  48740  pgnbgreunbgrlem6  48746  rngccatidALTV  48894  ringccatidALTV  48928  ldepspr  49095  mosn  49434  indthinc  50083  indthincALT  50084