Theorem eleq2 2820

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  eleq12  2821  eleq2i  2823  nelneq2  2856  dvelimdc  2919  raleqf  3321  rexeqfOLD  3323  rmoeq1OLD  3379  reueq1OLD  3380  rmoeq1f  3385  rabeq  3409  rabeqd  3423  rabeqf  3429  clel3g  3611  clel4g  3613  sbcbi2  3795  sbcel2gv  3803  csbeq2  3850  difeq2  4067  uneq1  4108  unineq  4235  nel02  4286  n0i  4287  sbnfc2  4386  disjel  4404  elif  4516  exsnrex  4630  elinsn  4660  sneqrg  4788  preq1b  4795  preq12b  4799  elpreqprb  4817  elunii  4861  elinti  4904  intss1  4911  intmin  4916  intab  4926  iuneqconst  4951  iineq2  4960  dfiun2g  4978  dfiin2g  4979  breq  5091  zfrepclf  5227  zfauscl  5234  sseliALT  5245  inuni  5286  selsALT  5380  rext  5387  intidg  5396  elopg  5404  opth1  5413  opthwiener  5452  xpeq1  5628  xpeq2  5635  0nelelxp  5649  opthprc  5678  ordtri1  6339  ordtri3  6342  nsuceq0  6391  suctr  6394  ordnbtwn  6401  funopg  6515  dffv2  6917  fveqdmss  7011  dffo4  7036  funopdmsn  7083  fnsnbOLD  7100  elunirn  7185  f1oiso  7285  canth  7300  eusvobj2  7338  mpoeq123  7418  ndmovg  7529  uniuni  7695  iunpw  7704  oneqmin  7733  onuninsuci  7770  nlimsucg  7772  limomss  7801  nnlim  7810  peano5  7823  unielxp  7959  cnvf1o  8041  soseq  8089  smoel  8280  smo11  8284  tz7.44-2  8326  nlim2  8405  ord1eln01  8411  ord2eln012  8412  oawordeulem  8469  oaordex  8473  omordi  8481  oneo  8496  oeordi  8502  oeoa  8512  oeoe  8514  nnmordi  8546  nnaordex  8553  nnaordex2  8554  omabs  8566  nnneo  8570  omsmolem  8572  elqsn0  8708  qsel  8720  mapsnd  8810  undifixp  8858  boxriin  8864  boxcutc  8865  pssnn  9078  fineqvlem  9150  fineqv  9151  en1eqsn  9159  fissuni  9241  dffi2  9307  inficl  9309  dffi3  9315  wofib  9431  zfregcl  9480  zfregclOLD  9481  nelaneq  9487  en3lplem1  9502  en3lp  9504  suc11reg  9509  inf0  9511  inf3lem2  9519  inf3lem3  9520  infeq5i  9526  axinf2  9530  dfom3  9537  elom3  9538  cantnfle  9561  oemapvali  9574  cantnflem1  9579  tc2  9630  r1sdom  9667  rankwflemb  9686  rankval3b  9719  rankunb  9743  rankuni2b  9746  cardlim  9865  cardprclem  9872  infxpenlem  9904  alephnbtwn  9962  alephordi  9965  cardaleph  9980  alephfp  9999  alephval3  10001  dfac3  10012  dfac5lem2  10015  dfac5lem4  10017  dfac5lem4OLD  10019  dfac2b  10022  kmlem2  10043  coflim  10152  cfsmolem  10161  fin23lem30  10233  isf34lem4  10268  axdc2lem  10339  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  zorn2lem7  10393  axdclem  10410  brdom7disj  10422  brdom6disj  10423  axpowndlem3  10490  winainflem  10584  iswun  10595  eltskg  10641  inar1  10666  elgrug  10683  inaprc  10727  eltskm  10734  addnidpi  10792  indpi  10798  nqereu  10820  elnp  10878  elnpi  10879  genpnnp  10896  ltaddpr  10925  dfnn2  12138  dfnn3  12139  dfuzi  12564  uz11  12757  elfzonlteqm1  13641  fzoopth  13662  om2uzlti  13857  axdc4uz  13891  hashrabsn1  14281  hashbclem  14359  hashf1lem2  14363  hash2prb  14379  hash2prd  14382  hash3tpb  14402  wrdsymb0  14456  lsw0  14472  swrdwrdsymb  14570  rtrclreclem3  14967  prodeq1f  15813  prodeq1  15814  rpnnen2lem1  16123  rpnnen2lem2  16124  lcmfval  16532  lcmf0val  16533  ismre  17492  isacs  17557  initoid  17908  termoid  17909  initoeu2lem1  17921  clatl  18414  mreclatBAD  18469  issubmgm  18610  issubm  18711  dfgrp2e  18876  isnsg  19067  cycsubg  19120  resghm  19144  ghmeql  19151  gsmsymgreq  19344  f1otrspeq  19359  pmtrval  19363  pmtrdifellem4  19391  pmtrprfval  19399  gsumzsplit  19839  pgpfac1lem1  19988  pgpfac1lem5  19993  pgpfac1  19994  ablsimpnosubgd  20018  c0snmgmhm  20380  c0snmhm  20381  0ring01eq  20444  issubrg  20486  lmodfopnelem2  20832  islss  20867  lspsneq0  20945  lmhmeql  20989  lspdisjb  21063  lidl1el  21163  rngqiprngfulem2  21249  rngqipring1  21253  lidldvgen  21271  islindf4  21775  mplcoe1  21972  mplcoe5  21975  selvfval  22049  m1detdiag  22512  mdetunilem9  22535  maducoeval2  22555  madugsum  22558  chpmat1dlem  22750  istopg  22810  toprntopon  22840  fiinbas  22867  topbas  22887  ppttop  22922  pptbas  22923  epttop  22924  elcls  22988  clsndisj  22990  iscldtop  23010  neiptopnei  23047  restbas  23073  restntr  23097  pnfnei  23135  mnfnei  23136  cnpimaex  23171  lmcvg  23177  iscnp4  23178  cncnpi  23193  cnconst2  23198  cnprest  23204  cnprest2  23205  cnpdis  23208  lmss  23213  lmff  23216  cnt0  23261  ist1-3  23264  cnhaus  23269  isreg2  23292  dishaus  23297  ordthauslem  23298  cmpsublem  23314  cmpsub  23315  cmpcld  23317  hauscmplem  23321  unconn  23344  conncompid  23346  conncompss  23348  1stcfb  23360  1stcrest  23368  2ndcctbss  23370  2ndcomap  23373  dis2ndc  23375  1stcelcls  23376  llyeq  23385  nllyeq  23386  restnlly  23397  islly2  23399  lly1stc  23411  dislly  23412  hauspwdom  23416  finlocfin  23435  unisngl  23442  dissnlocfin  23444  locfindis  23445  comppfsc  23447  llycmpkgen2  23465  txbas  23482  eltx  23483  ptpjopn  23527  ptclsg  23530  txcnp  23535  ptcnplem  23536  ptcnp  23537  txlly  23551  pthaus  23553  txtube  23555  txhaus  23562  txlm  23563  tx1stc  23565  txkgen  23567  xkohaus  23568  xkopt  23570  xkococnlem  23574  tgqtop  23627  kqfvima  23645  kqt0lem  23651  isr0  23652  regr1lem  23654  kqreglem1  23656  kqreglem2  23657  reghmph  23708  fbssfi  23752  isfil  23762  filuni  23800  isufil  23818  isufil2  23823  fixufil  23837  uffixfr  23838  uffixsn  23840  rnelfm  23868  flimopn  23890  flimrest  23898  flimcls  23900  txflf  23921  fclsopni  23930  fclsrest  23939  fclscf  23940  fcfnei  23950  alexsublem  23959  alexsubALTlem3  23964  alexsubALT  23966  tmdgsum2  24011  symgtgp  24021  subgntr  24022  opnsubg  24023  ghmcnp  24030  tgpt0  24034  qustgpopn  24035  tsmsi  24049  tsmssubm  24058  tsmssplit  24067  isust  24119  ustn0  24136  blssps  24339  blss  24340  blssexps  24341  blssex  24342  neibl  24416  blcld  24420  metss  24423  methaus  24435  met1stc  24436  met2ndci  24437  metrest  24439  prdsxmslem2  24444  metcnp3  24455  dscopn  24488  idnghm  24658  qdensere  24684  tgioo  24711  tgqioo  24715  zdis  24732  xrge0tsms  24750  cnheibor  24881  lmmbr  25185  bcthlem4  25254  ovolicc2lem5  25449  dyadmbllem  25527  i1fd  25609  itg11  25619  itg2gt0  25688  itgeq1f  25699  itgeq1fOLD  25700  itgeq1  25701  bddmulibl  25767  ellimc2  25805  limcnlp  25806  ellimc3  25807  limcflf  25809  limciun  25822  lhop1lem  25945  ig1pdvds  26112  plycpn  26224  aannenlem2  26264  efopn  26594  xrlimcnp  26905  wilthlem2  27006  wilthlem3  27007  nodenselem8  27630  noetasuplem4  27675  noetainflem4  27679  nocvxminlem  27717  lrrecfr  27886  addsprop  27919  bdayon  28209  dfn0s2  28260  tghilberti1  28615  colline  28627  lmif  28763  islmib  28765  incistruhgr  29057  upgr1eopALT  29095  uhgrvtxedgiedgb  29114  upgredg2vtx  29119  edglnl  29121  numedglnl  29122  uhgr2edg  29186  umgrvad2edg  29191  usgredg4  29195  usgredg2vtxeuALT  29200  uspgredg2vlem  29201  ushgredgedg  29207  nbgr1vtx  29336  nbusgredgeu0  29346  nbusgrf1o0  29347  nb3grprlem1  29358  nb3grprlem2  29359  uvtx01vtx  29375  nbupgruvtxres  29385  cplgr1vlem  29407  cplgr1v  29408  vtxd0nedgb  29467  vtxduhgr0nedg  29471  1loopgrvd2  29482  1egrvtxdg0  29490  uspgrloopvtxel  29495  vtxdginducedm1lem4  29521  wlk1walk  29617  wlkp1lem1  29650  pthdivtx  29705  0enwwlksnge1  29842  usgrwwlks2on  29936  umgrwwlks2on  29937  rusgr0edg  29954  eleclclwwlkn  30056  upgr4cycl4dv4e  30165  1conngr  30174  vdn0conngrumgrv2  30176  eupth2eucrct  30197  eupth2lem1  30198  frgrncvvdeqlem7  30285  frgrncvvdeqlem9  30287  frgrwopregasn  30296  frgrwopregbsn  30297  l2p  30459  lpni  30460  issh  31188  pjoc1  31414  h1dn0  31532  spansneleqi  31549  nonbooli  31631  pjch  31674  pjnel  31706  cdjreui  32412  rexunirn  32471  rabsnel  32480  nelun  32493  iinabrex  32549  opabdm  32594  opabrn  32595  fpwrelmapffslem  32715  fpwrelmap  32716  fz1nntr  32784  indval  32834  xrge0tsmsd  33042  nsgqusf1olem3  33380  elrspunidl  33393  isprmidl  33403  constrmon  33757  reff  33852  tpr2rico  33925  lmxrge0  33965  issiga  34125  isrnsiga  34126  isldsys  34169  isros  34181  issros  34188  ddeval1  34247  ddeval0  34248  ismbfm  34264  dya2icoseg  34290  dya2iocnrect  34294  ballotlem7  34549  bnj216  34744  bnj563  34755  bnj956  34788  bnj545  34907  bnj548  34909  bnj570  34917  bnj900  34941  bnj929  34948  bnj964  34955  bnj983  34963  bnj1001  34971  bnj1145  35005  bnj1398  35046  bnj1498  35073  fineqvnttrclselem2  35142  fineqvnttrclse  35144  wevgblacfn  35153  erdszelem1  35235  kur14lem9  35258  cnllysconn  35289  cvmsss2  35318  cvmcov2  35319  cvmsiota  35321  cvmopnlem  35322  cvmliftlem15  35342  satfv1  35407  satfdmlem  35412  mclsssvlem  35606  mclsind  35614  untelirr  35752  untsucf  35754  elintfv  35809  dfon2lem4  35828  dfon2lem7  35831  dfon2lem9  35833  dfiota3  35965  funpartlem  35986  funpartfun  35987  linethru  36197  hilbert1.1  36198  rankelg  36212  elhf2  36219  neibastop2lem  36404  bj-zfauscl  36968  bj-cleq  37006  bj-snsetex  37007  bj-clel3gALT  37092  bj-nuliota  37101  bj-isrvec  37338  mptsnunlem  37382  isbasisrelowllem1  37399  isbasisrelowllem2  37400  relowlssretop  37407  relowlpssretop  37408  exrecfnlem  37423  finxpeq1  37430  finxpreclem5  37439  finxpreclem6  37440  nlpineqsn  37452  fvineqsneq  37456  pibt2  37461  unccur  37653  fin2so  37657  matunitlindflem1  37666  ptrecube  37670  poimirlem9  37679  poimirlem30  37700  poimir  37703  heicant  37705  mblfinlem1  37707  ftc1anc  37751  ftc2nc  37752  cover2  37765  isbnd2  37833  prdstotbnd  37844  heibor1lem  37859  grpokerinj  37943  rngoueqz  37990  isidl  38064  1idl  38076  0rngo  38077  ispridl  38084  smprngopr  38102  isfldidl  38118  isdmn3  38124  mpobi123f  38212  iineq12f  38214  mptbi12f  38216  dfsuccl4  38497  eqvrelqsel  38722  n0eldmqseq  38757  dmqseqim2  38765  disjlem17  38907  lsateln0  39104  ispsubsp  39854  linepsubN  39861  elpcliN  40002  dvh3dim3N  41558  dochsnnz  41559  mapdindp3  41831  sn-iotalem  42324  prjspval  42706  elmzpcl  42829  diophren  42916  dford3lem2  43130  ttac  43139  pw2f1ocnv  43140  wepwsolem  43145  kelac1  43166  onexgt  43343  onexlimgt  43346  ordnexbtwnsuc  43370  oaordnr  43399  omnord1  43408  nnoeomeqom  43415  oenord1  43419  succlg  43431  oacl2g  43433  omabs2  43435  omcl2  43436  omcl3g  43437  naddwordnexlem4  43504  nlimsuc  43544  intabssd  43622  elmapintrab  43679  eliunov2  43782  gneispaceel2  44247  mnuop23d  44369  mnuunid  44380  mnurndlem1  44384  expgrowthi  44436  dvconstbi  44437  tratrb  44639  suctrALT2VD  44938  suctrALT2  44939  en3lplem1VD  44945  en3lpVD  44947  tratrbVD  44963  suctrALTcf  45024  suctrALTcfVD  45025  suctrALT3  45026  unisnALT  45028  0elaxnul  45086  pwclaxpow  45087  prclaxpr  45088  uniclaxun  45089  omssaxinf2  45091  wfaxrep  45097  restuni3  45225  supminfxr  45572  xlimxrre  45939  xlimmnfvlem1  45940  xlimpnfvlem1  45944  icccncfext  45995  stoweidlem27  46135  stoweidlem35  46143  stoweidlem46  46154  stoweidlem52  46160  ioorrnopnlem  46412  ioorrnopnxrlem  46414  issal  46422  intsaluni  46437  salgencntex  46451  smfresal  46896  tannpoly  47000  funressnfv  47153  fnbrafvb  47264  afvco2  47286  ndmaovg  47294  aovmpt4g  47311  fafv2elrnb  47345  fvelsetpreimafv  47497  elsetpreimafvbi  47501  sprsymrelf1lem  47601  paireqne  47621  fpprbasnn  47839  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  dfclnbgr6  47966  dfsclnbgr6  47968  grtri  48050  stgrvtx0  48072  stgrnbgr0  48074  isubgr3stgrlem3  48078  gpgvtx0  48163  gpgvtx1  48164  gpg3kgrtriex  48199  pgnbgreunbgrlem3  48228  pgnbgreunbgrlem6  48234  rngccatidALTV  48382  ringccatidALTV  48416  ldepspr  48584  mosn  48923  indthinc  49573  indthincALT  49574