Theorem eleq2 2823

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  eleq12  2824  eleq2i  2826  nelneq2  2859  clelsb2OLD  2863  dvelimdc  2923  raleqf  3332  rexeqfOLD  3334  rmoeq1OLD  3397  reueq1OLD  3398  rmoeq1f  3403  rabeq  3430  rabeqd  3444  rabeqf  3451  clel3g  3640  clel4g  3642  sbcbi2  3824  sbcel2gv  3832  csbeq2  3879  difeq2  4095  uneq1  4136  unineq  4263  nel02  4314  n0i  4315  sbnfc2  4414  disjel  4432  elif  4544  exsnrex  4656  elinsn  4686  sneqrg  4815  preq1b  4822  preq12b  4826  elpreqprb  4844  elunii  4888  elinti  4931  intss1  4939  intmin  4944  intab  4954  iuneqconst  4979  iineq2  4988  dfiun2g  5006  dfiin2g  5008  breq  5121  zfrepclf  5261  zfauscl  5268  sseliALT  5279  inuni  5320  selsALT  5414  rext  5423  intidg  5432  intidOLD  5433  elopg  5441  opth1  5450  opthwiener  5489  xpeq1  5668  xpeq2  5675  0nelelxp  5689  opthprc  5718  ordtri1  6385  ordtri3  6388  nsuceq0  6436  suctr  6439  ordnbtwn  6446  funopg  6569  dffv2  6973  fveqdmss  7067  dffo4  7092  funopdmsn  7139  fnsnbOLD  7157  elunirn  7242  f1oiso  7343  canth  7357  eusvobj2  7395  mpoeq123  7477  ndmovg  7588  uniuni  7754  iunpw  7763  oneqmin  7792  onuninsuci  7833  nlimsucg  7835  limomss  7864  nnlim  7873  peano5  7887  unielxp  8024  cnvf1o  8108  soseq  8156  smoel  8372  smo11  8376  tz7.44-2  8419  nlim2  8500  ord1eln01  8506  ord2eln012  8507  oawordeulem  8564  oaordex  8568  omordi  8576  oneo  8591  oeordi  8597  oeoa  8607  oeoe  8609  nnmordi  8641  nnaordex  8648  nnaordex2  8649  omabs  8661  nnneo  8665  omsmolem  8667  elqsn0  8798  qsel  8808  mapsnd  8898  undifixp  8946  boxriin  8952  boxcutc  8953  pssnn  9180  fineqvlem  9268  fineqv  9269  en1eqsn  9278  fissuni  9367  dffi2  9433  inficl  9435  dffi3  9441  wofib  9557  zfregcl  9606  en3lplem1  9624  en3lp  9626  suc11reg  9631  inf0  9633  inf3lem2  9641  inf3lem3  9642  infeq5i  9648  axinf2  9652  dfom3  9659  elom3  9660  cantnfle  9683  oemapvali  9696  cantnflem1  9701  tc2  9754  r1sdom  9786  rankwflemb  9805  rankval3b  9838  rankunb  9862  rankuni2b  9865  cardlim  9984  cardprclem  9991  infxpenlem  10025  alephnbtwn  10083  alephordi  10086  cardaleph  10101  alephfp  10120  alephval3  10122  dfac3  10133  dfac5lem2  10136  dfac5lem4  10138  dfac5lem4OLD  10140  dfac2b  10143  kmlem2  10164  coflim  10273  cfsmolem  10282  fin23lem30  10354  isf34lem4  10389  axdc2lem  10460  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  zorn2lem7  10514  axdclem  10531  brdom7disj  10543  brdom6disj  10544  axpowndlem3  10611  winainflem  10705  iswun  10716  eltskg  10762  inar1  10787  elgrug  10804  inaprc  10848  eltskm  10855  addnidpi  10913  indpi  10919  nqereu  10941  elnp  10999  elnpi  11000  genpnnp  11017  ltaddpr  11046  dfnn2  12251  dfnn3  12252  dfuzi  12682  uz11  12875  elfzonlteqm1  13755  fzoopth  13776  om2uzlti  13966  axdc4uz  14000  hashrabsn1  14390  hashbclem  14468  hashf1lem2  14472  hash2prb  14488  hash2prd  14491  hash3tpb  14511  wrdsymb0  14565  lsw0  14581  swrdwrdsymb  14678  rtrclreclem3  15077  prodeq1f  15920  prodeq1  15921  rpnnen2lem1  16230  rpnnen2lem2  16231  lcmfval  16638  lcmf0val  16639  ismre  17600  isacs  17661  initoid  18012  termoid  18013  initoeu2lem1  18025  clatl  18516  mreclatBAD  18571  issubmgm  18678  issubm  18779  dfgrp2e  18944  isnsg  19136  cycsubg  19189  resghm  19213  ghmeql  19220  gsmsymgreq  19411  f1otrspeq  19426  pmtrval  19430  pmtrdifellem4  19458  pmtrprfval  19466  gsumzsplit  19906  pgpfac1lem1  20055  pgpfac1lem5  20060  pgpfac1  20061  ablsimpnosubgd  20085  c0snmgmhm  20420  c0snmhm  20421  0ring01eq  20487  issubrg  20529  lmodfopnelem2  20854  islss  20889  lspsneq0  20967  lmhmeql  21011  lspdisjb  21085  lidl1el  21185  rngqiprngfulem2  21271  rngqipring1  21275  lidldvgen  21293  islindf4  21796  mplcoe1  21993  mplcoe5  21996  selvfval  22070  m1detdiag  22533  mdetunilem9  22556  maducoeval2  22576  madugsum  22579  chpmat1dlem  22771  istopg  22831  toprntopon  22861  fiinbas  22888  topbas  22908  ppttop  22943  pptbas  22944  epttop  22945  elcls  23009  clsndisj  23011  iscldtop  23031  neiptopnei  23068  restbas  23094  restntr  23118  pnfnei  23156  mnfnei  23157  cnpimaex  23192  lmcvg  23198  iscnp4  23199  cncnpi  23214  cnconst2  23219  cnprest  23225  cnprest2  23226  cnpdis  23229  lmss  23234  lmff  23237  cnt0  23282  ist1-3  23285  cnhaus  23290  isreg2  23313  dishaus  23318  ordthauslem  23319  cmpsublem  23335  cmpsub  23336  cmpcld  23338  hauscmplem  23342  unconn  23365  conncompid  23367  conncompss  23369  1stcfb  23381  1stcrest  23389  2ndcctbss  23391  2ndcomap  23394  dis2ndc  23396  1stcelcls  23397  llyeq  23406  nllyeq  23407  restnlly  23418  islly2  23420  lly1stc  23432  dislly  23433  hauspwdom  23437  finlocfin  23456  unisngl  23463  dissnlocfin  23465  locfindis  23466  comppfsc  23468  llycmpkgen2  23486  txbas  23503  eltx  23504  ptpjopn  23548  ptclsg  23551  txcnp  23556  ptcnplem  23557  ptcnp  23558  txlly  23572  pthaus  23574  txtube  23576  txhaus  23583  txlm  23584  tx1stc  23586  txkgen  23588  xkohaus  23589  xkopt  23591  xkococnlem  23595  tgqtop  23648  kqfvima  23666  kqt0lem  23672  isr0  23673  regr1lem  23675  kqreglem1  23677  kqreglem2  23678  reghmph  23729  fbssfi  23773  isfil  23783  filuni  23821  isufil  23839  isufil2  23844  fixufil  23858  uffixfr  23859  uffixsn  23861  rnelfm  23889  flimopn  23911  flimrest  23919  flimcls  23921  txflf  23942  fclsopni  23951  fclsrest  23960  fclscf  23961  fcfnei  23971  alexsublem  23980  alexsubALTlem3  23985  alexsubALT  23987  tmdgsum2  24032  symgtgp  24042  subgntr  24043  opnsubg  24044  ghmcnp  24051  tgpt0  24055  qustgpopn  24056  tsmsi  24070  tsmssubm  24079  tsmssplit  24088  isust  24140  ustn0  24157  blssps  24361  blss  24362  blssexps  24363  blssex  24364  neibl  24438  blcld  24442  metss  24445  methaus  24457  met1stc  24458  met2ndci  24459  metrest  24461  prdsxmslem2  24466  metcnp3  24477  dscopn  24510  idnghm  24680  qdensere  24706  tgioo  24733  tgqioo  24737  zdis  24754  xrge0tsms  24772  cnheibor  24903  lmmbr  25208  bcthlem4  25277  ovolicc2lem5  25472  dyadmbllem  25550  i1fd  25632  itg11  25642  itg2gt0  25711  itgeq1f  25722  itgeq1fOLD  25723  itgeq1  25724  bddmulibl  25790  ellimc2  25828  limcnlp  25829  ellimc3  25830  limcflf  25832  limciun  25845  lhop1lem  25968  ig1pdvds  26135  plycpn  26247  aannenlem2  26287  efopn  26617  xrlimcnp  26928  wilthlem2  27029  wilthlem3  27030  nodenselem8  27653  noetasuplem4  27698  noetainflem4  27702  nocvxminlem  27739  lrrecfr  27893  addsprop  27926  dfn0s2  28253  tghilberti1  28562  colline  28574  lmif  28710  islmib  28712  incistruhgr  29004  upgr1eopALT  29042  uhgrvtxedgiedgb  29061  upgredg2vtx  29066  edglnl  29068  numedglnl  29069  uhgr2edg  29133  umgrvad2edg  29138  usgredg4  29142  usgredg2vtxeuALT  29147  uspgredg2vlem  29148  ushgredgedg  29154  nbgr1vtx  29283  nbusgredgeu0  29293  nbusgrf1o0  29294  nb3grprlem1  29305  nb3grprlem2  29306  uvtx01vtx  29322  nbupgruvtxres  29332  cplgr1vlem  29354  cplgr1v  29355  vtxd0nedgb  29414  vtxduhgr0nedg  29418  1loopgrvd2  29429  1egrvtxdg0  29437  uspgrloopvtxel  29442  vtxdginducedm1lem4  29468  wlk1walk  29565  wlkp1lem1  29599  pthdivtx  29655  0enwwlksnge1  29792  umgrwwlks2on  29885  rusgr0edg  29901  eleclclwwlkn  30003  upgr4cycl4dv4e  30112  1conngr  30121  vdn0conngrumgrv2  30123  eupth2eucrct  30144  eupth2lem1  30145  frgrncvvdeqlem7  30232  frgrncvvdeqlem9  30234  frgrwopregasn  30243  frgrwopregbsn  30244  l2p  30406  lpni  30407  issh  31135  pjoc1  31361  h1dn0  31479  spansneleqi  31496  nonbooli  31578  pjch  31621  pjnel  31653  cdjreui  32359  rexunirn  32419  rabsnel  32427  nelun  32440  iinabrex  32496  opabdm  32537  opabrn  32538  fpwrelmapffslem  32655  fpwrelmap  32656  fz1nntr  32727  indval  32776  xrge0tsmsd  33002  nsgqusf1olem3  33376  elrspunidl  33389  isprmidl  33399  constrmon  33724  reff  33816  tpr2rico  33889  lmxrge0  33929  issiga  34089  isrnsiga  34090  isldsys  34133  isros  34145  issros  34152  ddeval1  34211  ddeval0  34212  ismbfm  34228  dya2icoseg  34255  dya2iocnrect  34259  ballotlem7  34514  bnj216  34709  bnj563  34720  bnj956  34753  bnj545  34872  bnj548  34874  bnj570  34882  bnj900  34906  bnj929  34913  bnj964  34920  bnj983  34928  bnj1001  34936  bnj1145  34970  bnj1398  35011  bnj1498  35038  wevgblacfn  35077  erdszelem1  35159  kur14lem9  35182  cnllysconn  35213  cvmsss2  35242  cvmcov2  35243  cvmsiota  35245  cvmopnlem  35246  cvmliftlem15  35266  satfv1  35331  satfdmlem  35336  mclsssvlem  35530  mclsind  35538  untelirr  35671  untsucf  35673  elintfv  35728  dfon2lem4  35750  dfon2lem7  35753  dfon2lem9  35755  dfiota3  35887  funpartlem  35906  funpartfun  35907  linethru  36117  hilbert1.1  36118  rankelg  36132  elhf2  36139  neibastop2lem  36324  bj-zfauscl  36888  bj-cleq  36926  bj-snsetex  36927  bj-clel3gALT  37012  bj-nuliota  37021  bj-isrvec  37258  mptsnunlem  37302  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlssretop  37327  relowlpssretop  37328  exrecfnlem  37343  finxpeq1  37350  finxpreclem5  37359  finxpreclem6  37360  nlpineqsn  37372  fvineqsneq  37376  pibt2  37381  unccur  37573  fin2so  37577  matunitlindflem1  37586  ptrecube  37590  poimirlem9  37599  poimirlem30  37620  poimir  37623  heicant  37625  mblfinlem1  37627  ftc1anc  37671  ftc2nc  37672  cover2  37685  isbnd2  37753  prdstotbnd  37764  heibor1lem  37779  grpokerinj  37863  rngoueqz  37910  isidl  37984  1idl  37996  0rngo  37997  ispridl  38004  smprngopr  38022  isfldidl  38038  isdmn3  38044  mpobi123f  38132  iineq12f  38134  mptbi12f  38136  eqvrelqsel  38580  n0eldmqseq  38613  dmqseqim2  38621  disjlem17  38763  lsateln0  38959  ispsubsp  39710  linepsubN  39717  elpcliN  39858  dvh3dim3N  41414  dochsnnz  41415  mapdindp3  41687  sn-iotalem  42218  prjspval  42573  elmzpcl  42696  diophren  42783  dford3lem2  42998  ttac  43007  pw2f1ocnv  43008  wepwsolem  43013  kelac1  43034  onexgt  43211  onexlimgt  43214  ordnexbtwnsuc  43238  oaordnr  43267  omnord1  43276  nnoeomeqom  43283  oenord1  43287  succlg  43299  oacl2g  43301  omabs2  43303  omcl2  43304  omcl3g  43305  naddwordnexlem4  43372  nlimsuc  43412  intabssd  43490  elmapintrab  43547  eliunov2  43650  gneispaceel2  44115  mnuop23d  44238  mnuunid  44249  mnurndlem1  44253  expgrowthi  44305  dvconstbi  44306  tratrb  44509  suctrALT2VD  44808  suctrALT2  44809  en3lplem1VD  44815  en3lpVD  44817  tratrbVD  44833  suctrALTcf  44894  suctrALTcfVD  44895  suctrALT3  44896  unisnALT  44898  0elaxnul  44956  pwclaxpow  44957  prclaxpr  44958  uniclaxun  44959  omssaxinf2  44961  wfaxrep  44967  restuni3  45090  supminfxr  45439  xlimxrre  45808  xlimmnfvlem1  45809  xlimpnfvlem1  45813  icccncfext  45864  stoweidlem27  46004  stoweidlem35  46012  stoweidlem46  46023  stoweidlem52  46029  ioorrnopnlem  46281  ioorrnopnxrlem  46283  issal  46291  intsaluni  46306  salgencntex  46320  smfresal  46765  funressnfv  47020  fnbrafvb  47131  afvco2  47153  ndmaovg  47161  aovmpt4g  47178  fafv2elrnb  47212  fvelsetpreimafv  47349  elsetpreimafvbi  47353  sprsymrelf1lem  47453  paireqne  47473  fpprbasnn  47691  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  dfclnbgr6  47817  dfsclnbgr6  47819  grtri  47900  stgrvtx0  47922  stgrnbgr0  47924  isubgr3stgrlem3  47928  gpgvtx0  48005  gpgvtx1  48006  gpg3kgrtriex  48039  rngccatidALTV  48195  ringccatidALTV  48229  ldepspr  48397  mosn  48739  indthinc  49296  indthincALT  49297