Theorem eleq2 2818

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806

This theorem is referenced by:  eleq12  2819  eleq2i  2821  nelneq2  2854  clelsb2OLD  2858  dvelimdc  2926  raleleqOLD  3336  raleqf  3345  rexeqfOLD  3347  rmoeq1OLD  3412  reueq1OLD  3413  rmoeq1f  3416  rabeq  3442  rabeqd  3456  rabeqf  3462  rabeqiOLD  3467  clel3g  3647  clel4g  3649  clel4OLD  3651  sbcbi2  3837  sbcel2gv  3846  csbeq2  3895  difeq2  4113  uneq1  4153  unineq  4274  nel02  4329  n0i  4330  sbnfc2  4433  disjel  4453  elif  4568  exsnrex  4681  elinsn  4711  sneqrg  4837  preq1b  4844  preq12b  4848  elpreqprb  4865  elunii  4909  elinti  4954  intss1  4962  intmin  4967  intab  4977  iuneqconst  5003  iineq2  5012  dfiun2g  5028  dfiin2g  5030  breq  5145  zfrepclf  5289  zfauscl  5296  sseliALT  5304  inuni  5340  selsALT  5436  rext  5445  intidg  5454  intidOLD  5455  elopg  5463  opth1  5472  opthwiener  5511  xpeq1  5687  xpeq2  5694  0nelelxp  5708  opthprc  5737  ordtri1  6397  ordtri3  6400  nsuceq0  6447  suctr  6450  ordnbtwn  6457  funopg  6582  dffv2  6988  fveqdmss  7083  dffo4  7108  funopdmsn  7154  fnsnb  7170  elunirn  7256  f1oiso  7354  canth  7368  eusvobj2  7407  mpoeq123  7487  ndmovg  7599  uniuni  7759  iunpw  7768  oneqmin  7798  onuninsuci  7839  nlimsucg  7841  limomss  7870  nnlim  7879  peano5  7894  peano5OLD  7895  unielxp  8026  cnvf1o  8111  soseq  8159  smoel  8375  smo11  8379  tz7.44-2  8422  nlim2  8505  ord1eln01  8511  ord2eln012  8512  oawordeulem  8569  oaordex  8573  omordi  8581  oneo  8596  oeordi  8602  oeoa  8612  oeoe  8614  nnmordi  8646  nnaordex  8653  nnaordex2  8654  omabs  8666  nnneo  8670  omsmolem  8672  elqsn0  8799  qsel  8809  mapsnd  8899  undifixp  8947  boxriin  8953  boxcutc  8954  pssnn  9187  fineqvlem  9281  fineqv  9282  pssnnOLD  9284  en1eqsn  9293  fissuni  9376  dffi2  9441  inficl  9443  dffi3  9449  wofib  9563  zfregcl  9612  en3lplem1  9630  en3lp  9632  suc11reg  9637  inf0  9639  inf3lem2  9647  inf3lem3  9648  infeq5i  9654  axinf2  9658  dfom3  9665  elom3  9666  cantnfle  9689  oemapvali  9702  cantnflem1  9707  tc2  9760  r1sdom  9792  rankwflemb  9811  rankval3b  9844  rankunb  9868  rankuni2b  9871  cardlim  9990  cardprclem  9997  infxpenlem  10031  alephnbtwn  10089  alephordi  10092  cardaleph  10107  alephfp  10126  alephval3  10128  dfac3  10139  dfac5lem2  10142  dfac5lem4  10144  dfac2b  10148  kmlem2  10169  coflim  10279  cfsmolem  10288  fin23lem30  10360  isf34lem4  10395  axdc2lem  10466  axdc3lem2  10469  axdc3lem4  10471  axdc4lem  10473  zorn2lem7  10520  axdclem  10537  brdom7disj  10549  brdom6disj  10550  axpowndlem3  10617  winainflem  10711  iswun  10722  eltskg  10768  inar1  10793  elgrug  10810  inaprc  10854  eltskm  10861  addnidpi  10919  indpi  10925  nqereu  10947  elnp  11005  elnpi  11006  genpnnp  11023  ltaddpr  11052  dfnn2  12250  dfnn3  12251  dfuzi  12678  uz11  12872  elfzonlteqm1  13735  om2uzlti  13942  axdc4uz  13976  hashrabsn1  14360  hashbclem  14438  hashf1lem2  14444  hash2prb  14460  hash2prd  14463  wrdsymb0  14526  lsw0  14542  swrdwrdsymb  14639  rtrclreclem3  15034  prodeq1f  15879  rpnnen2lem1  16185  rpnnen2lem2  16186  lcmfval  16586  lcmf0val  16587  ismre  17564  isacs  17625  initoid  17984  termoid  17985  initoeu2lem1  17997  clatl  18494  mreclatBAD  18549  issubmgm  18656  issubm  18749  dfgrp2e  18914  isnsg  19104  cycsubg  19157  resghm  19180  ghmeql  19187  gsmsymgreq  19381  f1otrspeq  19396  pmtrval  19400  pmtrdifellem4  19428  pmtrprfval  19436  gsumzsplit  19876  pgpfac1lem1  20025  pgpfac1lem5  20030  pgpfac1  20031  ablsimpnosubgd  20055  c0snmgmhm  20395  c0snmhm  20396  0ring01eq  20460  issubrg  20504  lmodfopnelem2  20776  islss  20812  lspsneq0  20890  lmhmeql  20934  lspdisjb  21008  lidl1el  21116  rngqiprngfulem2  21196  rngqipring1  21200  lidldvgen  21218  islindf4  21766  mplcoe1  21969  mplcoe5  21972  selvfval  22054  m1detdiag  22493  mdetunilem9  22516  maducoeval2  22536  madugsum  22539  chpmat1dlem  22731  istopg  22791  toprntopon  22821  fiinbas  22849  topbas  22869  ppttop  22904  pptbas  22905  epttop  22906  elcls  22971  clsndisj  22973  iscldtop  22993  neiptopnei  23030  restbas  23056  restntr  23080  pnfnei  23118  mnfnei  23119  cnpimaex  23154  lmcvg  23160  iscnp4  23161  cncnpi  23176  cnconst2  23181  cnprest  23187  cnprest2  23188  cnpdis  23191  lmss  23196  lmff  23199  cnt0  23244  ist1-3  23247  cnhaus  23252  isreg2  23275  dishaus  23280  ordthauslem  23281  cmpsublem  23297  cmpsub  23298  cmpcld  23300  hauscmplem  23304  unconn  23327  conncompid  23329  conncompss  23331  1stcfb  23343  1stcrest  23351  2ndcctbss  23353  2ndcomap  23356  dis2ndc  23358  1stcelcls  23359  llyeq  23368  nllyeq  23369  restnlly  23380  islly2  23382  lly1stc  23394  dislly  23395  hauspwdom  23399  finlocfin  23418  unisngl  23425  dissnlocfin  23427  locfindis  23428  comppfsc  23430  llycmpkgen2  23448  txbas  23465  eltx  23466  ptpjopn  23510  ptclsg  23513  txcnp  23518  ptcnplem  23519  ptcnp  23520  txlly  23534  pthaus  23536  txtube  23538  txhaus  23545  txlm  23546  tx1stc  23548  txkgen  23550  xkohaus  23551  xkopt  23553  xkococnlem  23557  tgqtop  23610  kqfvima  23628  kqt0lem  23634  isr0  23635  regr1lem  23637  kqreglem1  23639  kqreglem2  23640  reghmph  23691  fbssfi  23735  isfil  23745  filuni  23783  isufil  23801  isufil2  23806  fixufil  23820  uffixfr  23821  uffixsn  23823  rnelfm  23851  flimopn  23873  flimrest  23881  flimcls  23883  txflf  23904  fclsopni  23913  fclsrest  23922  fclscf  23923  fcfnei  23933  alexsublem  23942  alexsubALTlem3  23947  alexsubALT  23949  tmdgsum2  23994  symgtgp  24004  subgntr  24005  opnsubg  24006  ghmcnp  24013  tgpt0  24017  qustgpopn  24018  tsmsi  24032  tsmssubm  24041  tsmssplit  24050  isust  24102  ustn0  24119  blssps  24324  blss  24325  blssexps  24326  blssex  24327  neibl  24404  blcld  24408  metss  24411  methaus  24423  met1stc  24424  met2ndci  24425  metrest  24427  prdsxmslem2  24432  metcnp3  24443  dscopn  24476  idnghm  24654  qdensere  24680  tgioo  24706  tgqioo  24710  zdis  24726  xrge0tsms  24744  cnheibor  24875  lmmbr  25180  bcthlem4  25249  ovolicc2lem5  25444  dyadmbllem  25522  i1fd  25604  itg11  25614  itg2gt0  25684  itgeq1f  25695  bddmulibl  25762  ellimc2  25800  limcnlp  25801  ellimc3  25802  limcflf  25804  limciun  25817  lhop1lem  25940  ig1pdvds  26108  plycpn  26218  aannenlem2  26258  efopn  26586  xrlimcnp  26894  wilthlem2  26995  wilthlem3  26996  nodenselem8  27618  noetasuplem4  27663  noetainflem4  27667  nocvxminlem  27704  lrrecfr  27854  addsprop  27887  dfn0s2  28195  tghilberti1  28435  colline  28447  lmif  28583  islmib  28585  incistruhgr  28886  upgr1eopALT  28924  uhgrvtxedgiedgb  28943  upgredg2vtx  28948  edglnl  28950  numedglnl  28951  uhgr2edg  29015  umgrvad2edg  29020  usgredg4  29024  usgredg2vtxeuALT  29029  uspgredg2vlem  29030  ushgredgedg  29036  nbgr1vtx  29165  nbusgredgeu0  29175  nbusgrf1o0  29176  nb3grprlem1  29187  nb3grprlem2  29188  uvtx01vtx  29204  nbupgruvtxres  29214  cplgr1vlem  29236  cplgr1v  29237  vtxd0nedgb  29296  vtxduhgr0nedg  29300  1loopgrvd2  29311  1egrvtxdg0  29319  uspgrloopvtxel  29324  vtxdginducedm1lem4  29350  wlk1walk  29447  wlkp1lem1  29481  pthdivtx  29537  0enwwlksnge1  29669  umgrwwlks2on  29762  rusgr0edg  29778  eleclclwwlkn  29880  upgr4cycl4dv4e  29989  1conngr  29998  vdn0conngrumgrv2  30000  eupth2eucrct  30021  eupth2lem1  30022  frgrncvvdeqlem7  30109  frgrncvvdeqlem9  30111  frgrwopregasn  30120  frgrwopregbsn  30121  l2p  30283  lpni  30284  issh  31012  pjoc1  31238  h1dn0  31356  spansneleqi  31373  nonbooli  31455  pjch  31498  pjnel  31530  cdjreui  32236  rexunirn  32284  rabsnel  32292  nelun  32303  iinabrex  32353  opabdm  32395  opabrn  32396  fpwrelmapffslem  32509  fpwrelmap  32510  fz1nntr  32567  xrge0tsmsd  32766  nsgqusf1olem3  33120  elrspunidl  33139  isprmidl  33149  reff  33435  tpr2rico  33508  lmxrge0  33548  indval  33627  issiga  33726  isrnsiga  33727  isldsys  33770  isros  33782  issros  33789  ddeval1  33848  ddeval0  33849  ismbfm  33865  dya2icoseg  33892  dya2iocnrect  33896  ballotlem7  34150  bnj216  34358  bnj563  34369  bnj956  34402  bnj545  34521  bnj548  34523  bnj570  34531  bnj900  34555  bnj929  34562  bnj964  34569  bnj983  34577  bnj1001  34585  bnj1145  34619  bnj1398  34660  bnj1498  34687  erdszelem1  34796  kur14lem9  34819  cnllysconn  34850  cvmsss2  34879  cvmcov2  34880  cvmsiota  34882  cvmopnlem  34883  cvmliftlem15  34903  satfv1  34968  satfdmlem  34973  mclsssvlem  35167  mclsind  35175  untelirr  35297  untsucf  35299  elintfv  35355  dfon2lem4  35377  dfon2lem7  35380  dfon2lem9  35382  dfiota3  35514  funpartlem  35533  funpartfun  35534  linethru  35744  hilbert1.1  35745  rankelg  35759  elhf2  35766  neibastop2lem  35839  bj-zfauscl  36397  bj-cleq  36436  bj-snsetex  36437  bj-clel3gALT  36522  bj-nuliota  36531  bj-isrvec  36768  mptsnunlem  36812  isbasisrelowllem1  36829  isbasisrelowllem2  36830  relowlssretop  36837  relowlpssretop  36838  exrecfnlem  36853  finxpeq1  36860  finxpreclem5  36869  finxpreclem6  36870  nlpineqsn  36882  fvineqsneu  36885  fvineqsneq  36886  pibt2  36891  unccur  37071  fin2so  37075  matunitlindflem1  37084  ptrecube  37088  poimirlem9  37097  poimirlem30  37118  poimir  37121  heicant  37123  mblfinlem1  37125  ftc1anc  37169  ftc2nc  37170  cover2  37183  isbnd2  37251  prdstotbnd  37262  heibor1lem  37277  grpokerinj  37361  rngoueqz  37408  isidl  37482  1idl  37494  0rngo  37495  ispridl  37502  smprngopr  37520  isfldidl  37536  isdmn3  37542  mpobi123f  37630  iineq12f  37632  mptbi12f  37634  eqvrelqsel  38083  n0eldmqseq  38116  dmqseqim2  38124  disjlem17  38266  lsateln0  38462  ispsubsp  39213  linepsubN  39220  elpcliN  39361  dvh3dim3N  40917  dochsnnz  40918  mapdindp3  41190  sn-iotalem  41700  prjspval  42018  elmzpcl  42137  diophren  42224  dford3lem2  42439  ttac  42448  pw2f1ocnv  42449  wepwsolem  42457  kelac1  42478  onexgt  42659  onexlimgt  42662  ordnexbtwnsuc  42687  oaordnr  42716  omnord1  42725  nnoeomeqom  42732  oenord1  42736  succlg  42748  oacl2g  42750  omabs2  42752  omcl2  42753  omcl3g  42754  naddwordnexlem4  42822  nlimsuc  42862  intabssd  42940  elmapintrab  42997  eliunov2  43100  gneispaceel2  43565  mnuop23d  43694  mnuunid  43705  mnurndlem1  43709  expgrowthi  43761  dvconstbi  43762  tratrb  43966  suctrALT2VD  44266  suctrALT2  44267  en3lplem1VD  44273  en3lpVD  44275  tratrbVD  44291  suctrALTcf  44352  suctrALTcfVD  44353  suctrALT3  44354  unisnALT  44356  restuni3  44475  supminfxr  44837  xlimxrre  45210  xlimmnfvlem1  45211  xlimpnfvlem1  45215  icccncfext  45266  stoweidlem27  45406  stoweidlem35  45414  stoweidlem46  45425  stoweidlem52  45431  ioorrnopnlem  45683  ioorrnopnxrlem  45685  issal  45693  intsaluni  45708  salgencntex  45722  sge0f1o  45761  smfresal  46167  funressnfv  46416  fnbrafvb  46525  afvco2  46547  ndmaovg  46555  aovmpt4g  46572  fafv2elrnb  46606  fzoopth  46698  fvelsetpreimafv  46718  elsetpreimafvbi  46722  sprsymrelf1lem  46822  paireqne  46842  fpprbasnn  47060  nnsum4primeseven  47131  nnsum4primesevenALTV  47132  rngccatidALTV  47325  ringccatidALTV  47359  ldepspr  47532  mosn  47874  indthinc  48049  indthincALT  48050

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »