Theorem eleq2 2690

Description: Equality implies equivalence of membership. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)

Assertion

Ref	Expression
eleq2	|- ( A = B -> ( C e. A <-> C e. B ) )

Proof of Theorem eleq2

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( A = B -> A = B )
2	1	eleq2d 2687	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  eleq12  2691  eleq2i  2693  nelneq2  2726  dvelimdc  2786  nelne1  2890  raleqf  3134  rexeqf  3135  reueq1f  3136  rmoeq1f  3137  raleleq  3156  rabeqf  3190  clel3g  3340  clel4  3342  sbcbi2  3484  sbcel2gv  3496  csbeq2  3537  difeq2  3722  uneq1  3760  ineq1  3807  unineq  3877  n0i  3920  sbnfc2  4007  disjel  4023  elif  4128  exsnrex  4221  elinsn  4245  sneqrg  4370  preq1b  4377  preqr1OLD  4380  preq12b  4382  prel12  4383  elpreqprb  4397  elunii  4441  eluniab  4447  ssuniOLD  4460  elinti  4485  elintab  4487  intss1  4492  intmin  4497  intab  4507  iineq2  4538  dfiin2g  4553  breq  4655  zfrepclf  4777  zfauscl  4783  sseliALT  4791  inuni  4826  elALT  4910  rext  4916  intid  4926  elopg  4934  opth1  4944  opthwiener  4976  xpeq1  5128  xpeq2  5129  0nelelxp  5145  opthprc  5167  ordtri1  5756  ordtri3  5759  ordtri3OLD  5760  nsuceq0  5805  suctr  5808  suctrOLD  5809  ordnbtwn  5816  ordnbtwnOLD  5817  funopg  5922  dffv2  6271  fveqdmss  6354  dffo4  6375  funopdmsn  6415  fnsnb  6432  elunirn  6509  f1oiso  6601  canth  6608  eusvobj2  6643  mpt2eq123  6714  ndmovg  6817  snnexOLD  6967  uniuni  6971  iunpw  6978  oneqmin  7005  onuninsuci  7040  nlimsucg  7042  limomss  7070  nnlim  7078  peano5  7089  unielxp  7204  cnvf1o  7276  smoel  7457  smo11  7461  tz7.44-2  7503  oawordeulem  7634  oaordex  7638  omordi  7646  oneo  7661  oeordi  7667  oeoa  7677  oeoe  7679  nnmordi  7711  nnaordex  7718  omabs  7727  nnneo  7731  omsmolem  7733  elqsn0  7816  qsel  7826  mapsn  7899  undifixp  7944  boxriin  7950  boxcutc  7951  fineqvlem  8174  fineqv  8175  pssnn  8178  fissuni  8271  dffi2  8329  inficl  8331  dffi3  8337  wofib  8450  zfregcl  8499  zfregclOLD  8501  en3lplem1  8511  en3lp  8513  suc11reg  8516  inf0  8518  inf3lem2  8526  inf3lem3  8527  infeq5i  8533  axinf2  8537  dfom3  8544  elom3  8545  cantnfle  8568  oemapvali  8581  cantnflem1c  8584  cantnflem1  8586  tc2  8618  r1sdom  8637  rankwflemb  8656  rankval3b  8689  rankunb  8713  rankuni2b  8716  tcrank  8747  cardlim  8798  cardprclem  8805  infxpenlem  8836  alephnbtwn  8894  alephordi  8897  cardaleph  8912  alephfp  8931  alephval3  8933  dfac3  8944  dfac5lem2  8947  dfac5lem4  8949  dfac2  8953  kmlem2  8973  coflim  9083  cfsmolem  9092  fin23lem30  9164  isf32lem2  9176  isf34lem4  9199  axdc2lem  9270  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  zorn2lem7  9324  axdclem  9341  brdom7disj  9353  brdom6disj  9354  axpowndlem3  9421  winainflem  9515  iswun  9526  eltskg  9572  inar1  9597  elgrug  9614  inaprc  9658  eltskm  9665  addnidpi  9723  indpi  9729  nqereu  9751  elnp  9809  elnpi  9810  genpnnp  9827  ltaddpr  9856  dfnn2  11033  dfnn3  11034  dfuzi  11468  uz11  11710  elfzonlteqm1  12543  om2uzlti  12749  axdc4uz  12783  hashrabsn1  13163  hashbclem  13236  hashf1lem2  13240  hash2prb  13254  hash2prd  13257  wrdsymb0  13339  lsw0  13352  rtrclreclem3  13800  prodeq1f  14638  rpnnen2lem1  14943  rpnnen2lem2  14944  sadcp1  15177  lcmfval  15334  lcmf0val  15335  ismre  16250  isacs  16312  initoid  16655  termoid  16656  initoeu2lem1  16664  clatl  17116  mreclatBAD  17187  issubm  17347  dfgrp2e  17448  cycsubg  17622  isnsg  17623  subgacs  17629  nsgacs  17630  resghm  17676  ghmeql  17683  gsmsymgreq  17852  f1otrspeq  17867  pmtrval  17871  pmtrdifellem4  17899  pmtrprfval  17907  gsumzsplit  18327  pgpfac1lem1  18473  pgpfac1lem5  18478  pgpfac1  18479  issubrg  18780  lmodfopnelem2  18900  islss  18935  lssacs  18967  lspsneq0  19012  lmhmeql  19055  lspdisjb  19126  lidl1el  19218  lidldvgen  19255  0ring01eq  19271  mplcoe1  19465  mplcoe5  19468  islindf4  20177  m1detdiag  20403  mdetunilem9  20426  maducoeval2  20446  madugsum  20449  chpmat1dlem  20640  istopg  20700  toprntopon  20729  fiinbas  20756  topbas  20776  ppttop  20811  pptbas  20812  epttop  20813  elcls  20877  clsndisj  20879  elcls3  20887  iscldtop  20899  neiptopnei  20936  restbas  20962  restntr  20986  pnfnei  21024  mnfnei  21025  cnpimaex  21060  lmcvg  21066  iscnp4  21067  cncnpi  21082  cnconst2  21087  cnprest  21093  cnprest2  21094  cnpdis  21097  lmss  21102  lmff  21105  cnt0  21150  ist1-3  21153  cnhaus  21158  isreg2  21181  dishaus  21186  ordthauslem  21187  cmpsublem  21202  cmpsub  21203  cmpcld  21205  hauscmplem  21209  unconn  21232  conncompid  21234  conncompconn  21235  conncompss  21236  1stcfb  21248  1stcrest  21256  2ndcctbss  21258  2ndcomap  21261  dis2ndc  21263  1stcelcls  21264  llyeq  21273  nllyeq  21274  restnlly  21285  islly2  21287  lly1stc  21299  dislly  21300  hauspwdom  21304  finlocfin  21323  unisngl  21330  dissnlocfin  21332  locfindis  21333  comppfsc  21335  llycmpkgen2  21353  txbas  21370  eltx  21371  ptpjopn  21415  ptclsg  21418  dfac14lem  21420  txcnp  21423  ptcnplem  21424  ptcnp  21425  txlly  21439  pthaus  21441  txtube  21443  txhaus  21450  txlm  21451  tx1stc  21453  txkgen  21455  xkohaus  21456  xkopt  21458  xkococnlem  21462  tgqtop  21515  kqfvima  21533  kqt0lem  21539  isr0  21540  r0cld  21541  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  reghmph  21596  fbssfi  21641  isfil  21651  filuni  21689  isufil  21707  isufil2  21712  uffix  21725  fixufil  21726  uffixfr  21727  uffixsn  21729  rnelfm  21757  flimopn  21779  flimrest  21787  flimcls  21789  flftg  21800  txflf  21810  fclsopni  21819  fclsrest  21828  fclscf  21829  fcfnei  21839  alexsublem  21848  alexsubALTlem3  21853  alexsubALT  21855  tmdgsum2  21900  symgtgp  21905  subgntr  21910  opnsubg  21911  tgpconncompeqg  21915  ghmcnp  21918  tgpt0  21922  qustgpopn  21923  tsmsi  21937  tsmssubm  21946  tsmssplit  21955  isust  22007  ustn0  22024  blssps  22229  blss  22230  blssexps  22231  blssex  22232  neibl  22306  blcld  22310  metss  22313  methaus  22325  met1stc  22326  met2ndci  22327  metrest  22329  prdsxmslem2  22334  metcnp3  22345  dscopn  22378  idnghm  22547  qdensere  22573  tgioo  22599  tgqioo  22603  zdis  22619  xrge0tsms  22637  cnheibor  22754  lmmbr  23056  bcthlem4  23124  ovolicc2lem5  23289  dyadmbllem  23367  i1fd  23448  itg11  23458  itg2gt0  23527  itgeq1f  23538  bddmulibl  23605  ellimc2  23641  limcnlp  23642  ellimc3  23643  limcflf  23645  limciun  23658  lhop1lem  23776  ig1pdvds  23936  plycpn  24044  aannenlem2  24084  efopn  24404  xrlimcnp  24695  wilthlem2  24795  wilthlem3  24796  wilth  24797  tghilberti1  25532  tghilberti2  25533  colline  25544  lmif  25677  islmib  25679  incistruhgr  25974  upgr1eopALT  26012  uhgrvtxedgiedgb  26031  upgredg2vtx  26036  edglnl  26038  numedglnl  26039  uhgr2edg  26100  umgrvad2edg  26105  umgr2edgneu  26106  usgredg4  26109  usgredg2vtxeuALT  26114  uspgredg2vlem  26115  uspgredg2v  26116  ushgredgedg  26121  nbgr1vtx  26254  nbusgredgeu0  26270  nbusgrf1o0  26271  nbusgrf1o  26273  nb3grprlem1  26282  nb3grprlem2  26283  uvtxa01vtx0  26297  nbupgruvtxres  26308  cplgr1vlem  26325  cplgr1v  26326  vtxd0nedgb  26384  vtxduhgr0nedg  26388  1loopgrvd2  26399  1egrvtxdg0  26407  uspgrloopvtxel  26412  vtxdginducedm1lem4  26438  wlk1walk  26535  wlkp1lem1  26570  pthdivtx  26625  0enwwlksnge1  26749  umgrwwlks2on  26850  rusgr0edg  26868  eleclclwwlksn  26953  upgr4cycl4dv4e  27045  1conngr  27054  vdn0conngrumgrv2  27056  eupth2eucrct  27077  eupth2lem1  27078  frgrncvvdeqlem7  27169  frgrncvvdeqlem9  27171  frgrwopregasn  27180  frgrwopregbsn  27181  l2p  27331  lpni  27332  issh  28065  pjoc1  28293  h1dn0  28411  spansneleqi  28428  nonbooli  28510  pjch  28553  pjnel  28585  cdjreui  29291  rexunirn  29331  rabsnel  29341  opabdm  29423  opabrn  29424  fpwrelmapffslem  29507  fpwrelmap  29508  fz1nntr  29561  xrge0tsmsd  29785  reff  29906  tpr2rico  29958  lmxrge0  29998  indval  30075  issiga  30174  isrnsigaOLD  30175  isrnsiga  30176  isldsys  30219  isros  30231  issros  30238  ddeval1  30297  ddeval0  30298  ddemeas  30299  ismbfm  30314  isanmbfm  30318  dya2icoseg  30339  dya2iocnrect  30343  ballotlem7  30597  bnj145OLD  30795  bnj216  30800  bnj563  30813  bnj956  30847  bnj545  30965  bnj548  30967  bnj570  30975  bnj900  30999  bnj929  31006  bnj964  31013  bnj983  31021  bnj1001  31028  bnj1145  31061  bnj1398  31102  bnj1498  31129  erdszelem1  31173  kur14lem9  31196  cnllysconn  31227  cvmcov  31245  cvmsss2  31256  cvmcov2  31257  cvmseu  31258  cvmsiota  31259  cvmopnlem  31260  cvmliftlem15  31280  mclsssvlem  31459  mclsind  31467  untelirr  31585  untsucf  31587  elintfv  31662  dfon2lem4  31691  dfon2lem7  31694  dfon2lem9  31696  soseq  31751  frrlem4  31783  frrlem5e  31788  frrlem11  31792  nodenselem8  31841  noetalem3  31865  nocvxminlem  31893  dfiota3  32030  funpartlem  32049  funpartfun  32050  linethru  32260  hilbert1.1  32261  hilbert1.2  32262  rankelg  32275  elhf2  32282  fneint  32343  neibastop2lem  32355  bj-rabeqd  32916  bj-cleq  32949  bj-snsetex  32951  bj-nuliota  33019  mptsnunlem  33185  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  relowlpssretop  33212  finxpeq1  33223  finxpreclem5  33232  finxpreclem6  33233  unccur  33392  fin2so  33396  matunitlindflem1  33405  ptrecube  33409  poimirlem9  33418  poimirlem30  33439  poimir  33442  heicant  33444  mblfinlem1  33446  ftc1anc  33493  ftc2nc  33494  cover2  33508  isbnd2  33582  prdstotbnd  33593  heibor1lem  33608  grpokerinj  33692  rngoueqz  33739  isidl  33813  1idl  33825  0rngo  33826  ispridl  33833  smprngopr  33851  isfldidl  33867  isdmn3  33873  mpt2bi123f  33971  iineq12f  33973  mptbi12f  33975  nel02  34097  lsateln0  34282  ispsubsp  35031  linepsubN  35038  elpcliN  35179  dvh3dim3N  36738  dochsnnz  36739  mapdindp3  37011  elmzpcl  37289  diophren  37377  dford3lem2  37594  ttac  37603  pw2f1ocnv  37604  wepwsolem  37612  kelac1  37633  sdrgacs  37771  elintabg  37880  elmapintrab  37882  intabssd  37916  eliunov2  37971  gneispaceel2  38442  expgrowthi  38532  dvconstbi  38533  tratrb  38746  suctrALT2VD  39071  suctrALT2  39072  en3lplem1VD  39078  en3lpVD  39080  tratrbVD  39097  suctrALTcf  39158  suctrALTcfVD  39159  suctrALT3  39160  unisnALT  39162  elunif  39175  fnchoice  39188  restuni3  39301  mapsnd  39388  supminfxr  39694  xlimxrre  40057  xlimmnfvlem1  40058  xlimpnfvlem1  40062  icccncfext  40100  stoweidlem27  40244  stoweidlem35  40252  stoweidlem46  40263  stoweidlem52  40269  ioorrnopnlem  40524  ioorrnopnxrlem  40526  issal  40534  intsaluni  40547  salgencntex  40561  sge0f1o  40599  smfresal  40995  funressnfv  41208  fnbrafvb  41234  afvco2  41256  ndmaovg  41264  aovmpt4g  41281  fzoopth  41337  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  sprsymrelf1lem  41741  issubmgm  41789  c0snmgmhm  41914  c0snmhm  41915  rngccatidALTV  41989  ringccatidALTV  42052  ldepspr  42262