Theorem eleq2 2850

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eleq2d 2847	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  eleq12  2851  eleq2i  2853  nelneq2  2886  dvelimdc  2947  raleqf  3342  rmoeq1f  3403  rabeq  3427  rabeqd  3440  rabeqf  3446  clel3g  3615  clel4g  3617  sbcel2gv  3805  csbeq2  3852  difeq2  4068  uneq1  4108  unineq  4234  nel02  4285  sbnfc2  4397  disjel  4410  elif  4526  exsnrex  4641  elinsn  4671  sneqrg  4799  preq1b  4806  preq12b  4810  elpreqprb  4828  elunii  4872  elinti  4916  intss1  4923  intmin  4928  intab  4938  iuneqconst  4963  iineq2  4972  dfiun2g  4988  breq  5105  zfrepclf  5244  sepg  5251  zfausclOLD  5253  sseliALT  5263  vneqv  5270  inuni  5311  selsALT  5409  rext  5416  intidg  5425  elopg  5435  opth1  5444  opthwiener  5487  xpeq1  5665  xpeq2  5672  0nelelxp  5686  opthprc  5715  ordtri1  6396  ordtri3  6399  nsuceq0  6448  suctr  6451  ordnbtwn  6458  funopg  6574  dffv2  6980  fveqdmss  7078  dffo4  7103  funopdmsn  7154  fnsnbOLD  7171  elunirn  7255  f1oiso  7359  canth  7374  eusvobj2  7412  mpoeq123  7492  ndmovg  7604  uniuni  7776  iunpw  7785  oneqmin  7814  onuninsuci  7851  nlimsucg  7853  limomss  7882  nnlim  7891  peano5  7905  unielxp  8039  cnvf1o  8122  soseq  8176  smoel  8368  smo11  8372  tz7.44-2  8415  nlim2  8498  ord1eln01  8504  ord2eln012  8505  oawordeulem  8562  oaordex  8566  omordi  8574  oneo  8589  oeordi  8596  oeoa  8606  oeoe  8608  nnmordi  8640  nnaordex  8647  nnaordex2  8648  omabs  8660  nnneo  8664  omsmolem  8666  elqsn0  8805  qsel  8817  mapsnd  8914  undifixp  8962  boxriin  8968  boxcutc  8969  pssnn  9184  fineqvlem  9257  fineqv  9258  en1eqsn  9266  fissuni  9346  dffi2  9415  inficl  9417  dffi3  9423  wofib  9539  zfregcl  9588  zfregclOLD  9589  nelaneq  9596  nelaneqOLD  9597  en3lplem1  9613  en3lp  9615  suc11reg  9620  inf0  9622  inf3lem2  9630  inf3lem3  9631  infeq5i  9637  axinf2  9641  dfom3  9648  elom3  9649  cantnfle  9672  oemapvali  9685  cantnflem1  9690  tc2  9741  r1sdom  9781  rankwflemb  9800  rankwflembOLD  9801  rankval3b  9836  rankelg  9852  rankunb  9864  rankuni2b  9867  elhf2  9910  karden  9959  cardlim  10053  cardprclem  10060  infxpenlem  10092  alephnbtwn  10150  alephordi  10153  cardaleph  10168  alephfp  10187  alephval3  10189  dfac3  10200  dfac5lem2  10203  dfac5lem4  10205  dfac2b  10209  kmlem2  10230  coflim  10339  cfsmolem  10348  fin23lem30  10420  isf34lem4  10455  axdc2lem  10526  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  zorn2lem7  10580  axdclem  10597  brdom7disj  10610  brdom6disj  10611  axpowndlem3  10684  winainflem  10778  iswun  10789  eltskg  10835  inar1  10860  elgrug  10877  inaprc  10921  eltskm  10928  addnidpi  10986  indpi  10992  nqereu  11014  elnp  11072  elnpi  11073  genpnnp  11090  ltaddpr  11119  indval  12323  dfnn2  12348  dfnn3  12349  dfuzi  12790  uz11  12990  elfzonlteqm1  13876  fzoopth  13897  om2uzlti  14093  axdc4uz  14127  hashrabsn1  14518  hashbclem  14597  hashf1lem2  14601  hash2prb  14617  hash2prd  14620  hash3tpb  14640  wrdsymb0  14694  lsw0  14710  swrdwrdsymb  14812  rtrclreclem3  15213  prodeq1f  16075  prodeq1  16076  rpnnen2lem1  16382  rpnnen2lem2  16383  lcmfval  16796  lcmf0val  16797  ismre  17760  isacs  17825  initoid  18176  termoid  18177  initoeu2lem1  18189  clatl  18682  mreclatBAD  18737  issubmgm  18891  issubm  18998  dfgrp2e  19174  isnsg  19365  cycsubg  19423  resghm  19446  ghmeql  19453  gsmsymgreq  19646  f1otrspeq  19661  pmtrval  19665  pmtrdifellem4  19693  pmtrprfval  19701  gsumzsplit  20141  pgpfac1lem1  20290  pgpfac1lem5  20295  pgpfac1  20296  ablsimpnosubgd  20320  c0snmgmhm  20692  c0snmhm  20693  0ring01eq  20780  issubrg  20823  lmodfopnelem2  21174  islss  21209  lspsneq0  21287  lmhmeql  21330  lspdisjb  21404  lidl1el  21505  rngqiprngfulem2  21608  rngqipring1  21612  isprmidl  21619  lidldvgen  21658  islindf4  22144  mplcoe1  22346  mplcoe5  22349  selvfval  22428  m1detdiag  22912  mdetunilem9  22935  maducoeval2  22955  madugsum  22958  matunitlindflem1  22994  chpmat1dlem  23153  istopg  23213  toprntopon  23243  fiinbas  23270  topbas  23290  ppttop  23325  pptbas  23326  epttop  23327  elcls  23391  clsndisj  23393  iscldtop  23413  neiptopnei  23450  restbas  23476  restntr  23500  pnfnei  23538  mnfnei  23539  cnpimaex  23574  lmcvg  23580  iscnp4  23581  cncnpi  23596  cnconst2  23601  cnprest  23607  cnprest2  23608  cnpdis  23611  lmss  23616  lmff  23619  cnt0  23664  ist1-3  23667  cnhaus  23672  isreg2  23695  dishaus  23700  ordthauslem  23701  cmpsublem  23717  cmpsub  23718  cmpcld  23720  hauscmplem  23724  unconn  23747  conncompid  23749  conncompss  23751  1stcfb  23763  1stcrest  23771  2ndcctbss  23774  2ndcomap  23777  dis2ndc  23779  1stcelcls  23780  llyeq  23789  nllyeq  23790  restnlly  23801  islly2  23803  lly1stc  23815  dislly  23816  hauspwdom  23820  finlocfin  23839  unisngl  23846  dissnlocfin  23848  locfindis  23849  comppfsc  23851  llycmpkgen2  23869  txbas  23886  eltx  23887  ptpjopn  23931  ptclsg  23934  txcnp  23939  ptcnplem  23940  ptcnp  23941  txlly  23955  pthaus  23957  txtube  23959  txhaus  23966  txlm  23967  tx1stc  23969  txkgen  23971  xkohaus  23972  xkopt  23974  xkococnlem  23978  tgqtop  24031  kqfvima  24049  kqt0lem  24055  isr0  24056  regr1lem  24058  kqreglem1  24060  kqreglem2  24061  reghmph  24112  fbssfi  24156  isfil  24166  filuni  24204  isufil  24222  isufil2  24227  fixufil  24241  uffixfr  24242  uffixsn  24244  rnelfm  24272  flimopn  24294  flimrest  24302  flimcls  24304  txflf  24325  fclsopni  24334  fclsrest  24343  fclscf  24344  fcfnei  24354  alexsublem  24363  alexsubALTlem3  24368  alexsubALT  24370  tmdgsum2  24415  symgtgp  24425  subgntr  24426  opnsubg  24427  ghmcnp  24434  tgpt0  24438  qustgpopn  24439  tsmsi  24453  tsmssubm  24462  tsmssplit  24471  isust  24523  ustn0  24540  blssps  24743  blss  24744  blssexps  24745  blssex  24746  neibl  24820  blcld  24824  metss  24827  methaus  24839  met1stc  24840  met2ndci  24841  metrest  24843  prdsxmslem2  24848  metcnp3  24859  dscopn  24892  idnghm  25062  qdensere  25088  tgioo  25115  tgqioo  25119  zdis  25136  xrge0tsms  25154  cnheibor  25276  lmmbr  25579  bcthlem4  25648  ovolicc2lem5  25842  dyadmbllem  25920  i1fd  26002  itg11  26012  itg2gt0  26081  itgeq1f  26092  itgeq1  26093  bddmulibl  26159  ellimc2  26197  limcnlp  26198  ellimc3  26199  limcflf  26201  limciun  26214  lhop1lem  26333  ig1pdvds  26498  plycpn  26610  aannenlem2  26656  efopn  26986  xrlimcnp  27296  wilthlem2  27396  wilthlem3  27397  nodenselem8  28048  noetasuplem4  28093  noetainflem4  28097  nocvxminlem  28140  lrrecfr  28329  addsprop  28362  bdayons  28662  addonbday  28665  dfn0s2  28718  tghilberti1  29105  colline  29118  lmif  29290  islmib  29292  prlngex  29429  prlngeq  29435  incistruhgr  29657  upgr1eopALT  29695  uhgrvtxedgiedgb  29714  upgredg2vtx  29719  edglnl  29721  numedglnl  29722  uhgr2edg  29789  umgrvad2edg  29794  usgredg4  29798  usgredg2vtxeuALT  29803  uspgredg2vlem  29804  ushgredgedg  29810  nbgr1vtx  29939  nbusgredgeu0  29949  nbusgrf1o0  29950  nb3grprlem1  29961  nb3grprlem2  29962  uvtx01vtx  29978  nbupgruvtxres  29988  cplgr1vlem  30010  cplgr1v  30011  vtxd0nedgb  30069  vtxduhgr0nedg  30073  1loopgrvd2  30084  1egrvtxdg0  30092  uspgrloopvtxel  30097  vtxdginducedm1lem4  30123  wlk1walk  30219  wlkp1lem1  30252  pthdivtx  30312  0enwwlksnge1  30453  usgrwwlks2on  30547  umgrwwlks2on  30548  rusgr0edg  30565  eleclclwwlkn  30667  upgr4cycl4dv4e  30786  1conngr  30795  vdn0conngrumgrv2  30797  eupth2eucrct  30818  eupth2lem1  30819  frgrncvvdeqlem7  30906  frgrncvvdeqlem9  30908  frgrwopregasn  30917  frgrwopregbsn  30918  l2p  31081  lpni  31082  issh  31810  pjoc1  32036  h1dn0  32154  spansneleqi  32171  nonbooli  32253  pjch  32296  pjnel  32328  cdjreui  33034  rexunirn  33088  rabsnel  33096  nelun  33109  iinabrex  33163  opabdm  33205  opabrn  33206  fpwrelmapffslem  33324  fpwrelmap  33325  fz1nntr  33394  xrge0tsmsd  33634  nsgqusf1olem3  33966  elrspunidl  33978  constrmon  34376  reff  34471  tpr2rico  34544  lmxrge0  34584  issiga  34744  isrnsiga  34745  isldsys  34789  isros  34801  issros  34808  ddeval1  34867  ddeval0  34868  ismbfm  34884  dya2icoseg  34909  dya2iocnrect  34913  ballotlem7  35168  bnj216  35363  bnj563  35374  bnj956  35407  bnj545  35525  bnj548  35527  bnj570  35535  bnj900  35559  bnj929  35566  bnj964  35573  bnj983  35581  bnj1001  35589  bnj1145  35623  bnj1398  35664  bnj1498  35691  fineqvnttrclselem2  35790  fineqvnttrclse  35792  fineqvinfep  35793  wevgblacfn  35890  erdszelem1  35956  kur14lem9  35979  cnllysconn  36010  cvmsss2  36039  cvmcov2  36040  cvmsiota  36042  cvmopnlem  36043  cvmliftlem15  36063  satfv1  36128  satfdmlem  36133  mclsssvlem  36327  mclsind  36335  untelirr  36473  untsucf  36475  elintfv  36530  dfon2lem4  36548  dfon2lem7  36551  dfon2lem9  36553  dfiota3  36685  funpartlem  36706  funpartfun  36707  linethru  36918  hilbert1.1  36919  ltnadd  36967  neibastop2lem  37148  regsfromregtco  37326  regsfromunir1  37328  bj-sepg  37836  bj-cleq  37875  bj-snsetex  37876  bj-clel3gALT  37963  bj-nuliota  37972  bj-isrvec  38215  mptsnunlem  38261  isbasisrelowllem1  38278  isbasisrelowllem2  38279  relowlssretop  38286  relowlpssretop  38287  exrecfnlem  38302  finxpeq1  38309  finxpreclem5  38318  finxpreclem6  38319  nlpineqsn  38331  fvineqsneq  38335  pibt2  38340  unccur  38526  fin2so  38530  ptrecube  38538  poimirlem9  38547  poimirlem30  38568  poimir  38571  heicant  38573  mblfinlem1  38575  ftc1anc  38619  ftc2nc  38620  cover2  38649  isbnd2  38717  prdstotbnd  38728  heibor1lem  38743  grpokerinj  38827  rngoueqz  38874  isidl  38948  1idl  38960  0rngo  38961  ispridl  38968  smprngopr  38986  isfldidl  39002  isdmn3  39008  mpobi123f  39094  iineq12f  39096  mptbi12f  39098  dfsuccl4  39406  eqvrelqsel  39632  n0eldmqseq  39666  dmqseqim2  39674  suceldisj  39750  disjlem17  39834  lsateln0  40052  ispsubsp  40802  linepsubN  40809  elpcliN  40950  dvh3dim3N  42506  dochsnnz  42507  mapdindp3  42779  sn-iotalem  43275  prjspval  43631  elmzpcl  43736  diophren  43819  dford3lem2  44033  ttac  44042  pw2f1ocnv  44043  wepwsolem  44048  kelac1  44064  onexgt  44241  onexlimgt  44244  ordnexbtwnsuc  44268  oaordnr  44297  omnord1  44306  nnoeomeqom  44313  oenord1  44317  succlg  44329  oacl2g  44331  omabs2  44333  omcl2  44334  omcl3g  44335  naddwordnexlem4  44402  nlimsuc  44441  intabssd  44519  elmapintrab  44576  eliunov2  44678  gneispaceel2  45143  mnuop23d  45249  mnuunid  45260  mnurndlem1  45264  expgrowthi  45316  dvconstbi  45317  tratrb  45518  suctrALT2VD  45817  suctrALT2  45818  en3lplem1VD  45824  en3lpVD  45826  tratrbVD  45842  suctrALTcf  45903  suctrALTcfVD  45904  suctrALT3  45905  unisnALT  45907  0elaxnul  45972  pwclaxpow  45973  prclaxpr  45974  uniclaxun  45975  omssaxinf2  45977  wfaxrep  45983  restuni3  46132  supminfxr  46473  xlimxrre  46840  xlimmnfvlem1  46841  xlimpnfvlem1  46845  icccncfext  46896  stoweidlem27  47036  stoweidlem35  47044  stoweidlem46  47055  stoweidlem52  47061  ioorrnopnlem  47313  ioorrnopnxrlem  47315  issal  47323  intsaluni  47338  salgencntex  47352  smfresal  47797  tannpoly  47939  funressnfv  48112  fnbrafvb  48223  afvco2  48245  ndmaovg  48253  aovmpt4g  48270  fafv2elrnb  48304  fvelsetpreimafv  48468  elsetpreimafvbi  48472  sprsymrelf1lem  48572  paireqne  48592  fpprbasnn  48826  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  dfclnbgr6  48953  dfsclnbgr6  48955  grtri  49037  stgrvtx0  49059  stgrnbgr0  49061  isubgr3stgrlem3  49065  gpgvtx0  49150  gpgvtx1  49151  gpg3kgrtriex  49186  pgnbgreunbgrlem3  49215  pgnbgreunbgrlem6  49221  rngccatidALTV  49368  ringccatidALTV  49402  prmringnzring  49433  isidom3  49441  ldepspr  49584  mosn  49922  indthinc  50569  indthincALT  50570