Theorem eleq2 2817

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eleq12  2818  eleq2i  2820  nelneq2  2853  dvelimdc  2916  raleqf  3329  rexeqfOLD  3331  rmoeq1OLD  3389  reueq1OLD  3390  rmoeq1f  3395  rabeq  3420  rabeqd  3434  rabeqf  3440  clel3g  3627  clel4g  3629  sbcbi2  3812  sbcel2gv  3820  csbeq2  3867  difeq2  4083  uneq1  4124  unineq  4251  nel02  4302  n0i  4303  sbnfc2  4402  disjel  4420  elif  4532  exsnrex  4644  elinsn  4674  sneqrg  4803  preq1b  4810  preq12b  4814  elpreqprb  4832  elunii  4876  elinti  4919  intss1  4927  intmin  4932  intab  4942  iuneqconst  4967  iineq2  4976  dfiun2g  4994  dfiin2g  4996  breq  5109  zfrepclf  5246  zfauscl  5253  sseliALT  5264  inuni  5305  selsALT  5399  rext  5408  intidg  5417  intidOLD  5418  elopg  5426  opth1  5435  opthwiener  5474  xpeq1  5652  xpeq2  5659  0nelelxp  5673  opthprc  5702  ordtri1  6365  ordtri3  6368  nsuceq0  6417  suctr  6420  ordnbtwn  6427  funopg  6550  dffv2  6956  fveqdmss  7050  dffo4  7075  funopdmsn  7122  fnsnbOLD  7140  elunirn  7225  f1oiso  7326  canth  7341  eusvobj2  7379  mpoeq123  7461  ndmovg  7572  uniuni  7738  iunpw  7747  oneqmin  7776  onuninsuci  7816  nlimsucg  7818  limomss  7847  nnlim  7856  peano5  7869  unielxp  8006  cnvf1o  8090  soseq  8138  smoel  8329  smo11  8333  tz7.44-2  8375  nlim2  8454  ord1eln01  8460  ord2eln012  8461  oawordeulem  8518  oaordex  8522  omordi  8530  oneo  8545  oeordi  8551  oeoa  8561  oeoe  8563  nnmordi  8595  nnaordex  8602  nnaordex2  8603  omabs  8615  nnneo  8619  omsmolem  8621  elqsn0  8757  qsel  8769  mapsnd  8859  undifixp  8907  boxriin  8913  boxcutc  8914  pssnn  9132  fineqvlem  9209  fineqv  9210  en1eqsn  9219  fissuni  9308  dffi2  9374  inficl  9376  dffi3  9382  wofib  9498  zfregcl  9547  en3lplem1  9565  en3lp  9567  suc11reg  9572  inf0  9574  inf3lem2  9582  inf3lem3  9583  infeq5i  9589  axinf2  9593  dfom3  9600  elom3  9601  cantnfle  9624  oemapvali  9637  cantnflem1  9642  tc2  9695  r1sdom  9727  rankwflemb  9746  rankval3b  9779  rankunb  9803  rankuni2b  9806  cardlim  9925  cardprclem  9932  infxpenlem  9966  alephnbtwn  10024  alephordi  10027  cardaleph  10042  alephfp  10061  alephval3  10063  dfac3  10074  dfac5lem2  10077  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  kmlem2  10105  coflim  10214  cfsmolem  10223  fin23lem30  10295  isf34lem4  10330  axdc2lem  10401  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  zorn2lem7  10455  axdclem  10472  brdom7disj  10484  brdom6disj  10485  axpowndlem3  10552  winainflem  10646  iswun  10657  eltskg  10703  inar1  10728  elgrug  10745  inaprc  10789  eltskm  10796  addnidpi  10854  indpi  10860  nqereu  10882  elnp  10940  elnpi  10941  genpnnp  10958  ltaddpr  10987  dfnn2  12199  dfnn3  12200  dfuzi  12625  uz11  12818  elfzonlteqm1  13702  fzoopth  13723  om2uzlti  13915  axdc4uz  13949  hashrabsn1  14339  hashbclem  14417  hashf1lem2  14421  hash2prb  14437  hash2prd  14440  hash3tpb  14460  wrdsymb0  14514  lsw0  14530  swrdwrdsymb  14627  rtrclreclem3  15026  prodeq1f  15872  prodeq1  15873  rpnnen2lem1  16182  rpnnen2lem2  16183  lcmfval  16591  lcmf0val  16592  ismre  17551  isacs  17612  initoid  17963  termoid  17964  initoeu2lem1  17976  clatl  18467  mreclatBAD  18522  issubmgm  18629  issubm  18730  dfgrp2e  18895  isnsg  19087  cycsubg  19140  resghm  19164  ghmeql  19171  gsmsymgreq  19362  f1otrspeq  19377  pmtrval  19381  pmtrdifellem4  19409  pmtrprfval  19417  gsumzsplit  19857  pgpfac1lem1  20006  pgpfac1lem5  20011  pgpfac1  20012  ablsimpnosubgd  20036  c0snmgmhm  20371  c0snmhm  20372  0ring01eq  20438  issubrg  20480  lmodfopnelem2  20805  islss  20840  lspsneq0  20918  lmhmeql  20962  lspdisjb  21036  lidl1el  21136  rngqiprngfulem2  21222  rngqipring1  21226  lidldvgen  21244  islindf4  21747  mplcoe1  21944  mplcoe5  21947  selvfval  22021  m1detdiag  22484  mdetunilem9  22507  maducoeval2  22527  madugsum  22530  chpmat1dlem  22722  istopg  22782  toprntopon  22812  fiinbas  22839  topbas  22859  ppttop  22894  pptbas  22895  epttop  22896  elcls  22960  clsndisj  22962  iscldtop  22982  neiptopnei  23019  restbas  23045  restntr  23069  pnfnei  23107  mnfnei  23108  cnpimaex  23143  lmcvg  23149  iscnp4  23150  cncnpi  23165  cnconst2  23170  cnprest  23176  cnprest2  23177  cnpdis  23180  lmss  23185  lmff  23188  cnt0  23233  ist1-3  23236  cnhaus  23241  isreg2  23264  dishaus  23269  ordthauslem  23270  cmpsublem  23286  cmpsub  23287  cmpcld  23289  hauscmplem  23293  unconn  23316  conncompid  23318  conncompss  23320  1stcfb  23332  1stcrest  23340  2ndcctbss  23342  2ndcomap  23345  dis2ndc  23347  1stcelcls  23348  llyeq  23357  nllyeq  23358  restnlly  23369  islly2  23371  lly1stc  23383  dislly  23384  hauspwdom  23388  finlocfin  23407  unisngl  23414  dissnlocfin  23416  locfindis  23417  comppfsc  23419  llycmpkgen2  23437  txbas  23454  eltx  23455  ptpjopn  23499  ptclsg  23502  txcnp  23507  ptcnplem  23508  ptcnp  23509  txlly  23523  pthaus  23525  txtube  23527  txhaus  23534  txlm  23535  tx1stc  23537  txkgen  23539  xkohaus  23540  xkopt  23542  xkococnlem  23546  tgqtop  23599  kqfvima  23617  kqt0lem  23623  isr0  23624  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  reghmph  23680  fbssfi  23724  isfil  23734  filuni  23772  isufil  23790  isufil2  23795  fixufil  23809  uffixfr  23810  uffixsn  23812  rnelfm  23840  flimopn  23862  flimrest  23870  flimcls  23872  txflf  23893  fclsopni  23902  fclsrest  23911  fclscf  23912  fcfnei  23922  alexsublem  23931  alexsubALTlem3  23936  alexsubALT  23938  tmdgsum2  23983  symgtgp  23993  subgntr  23994  opnsubg  23995  ghmcnp  24002  tgpt0  24006  qustgpopn  24007  tsmsi  24021  tsmssubm  24030  tsmssplit  24039  isust  24091  ustn0  24108  blssps  24312  blss  24313  blssexps  24314  blssex  24315  neibl  24389  blcld  24393  metss  24396  methaus  24408  met1stc  24409  met2ndci  24410  metrest  24412  prdsxmslem2  24417  metcnp3  24428  dscopn  24461  idnghm  24631  qdensere  24657  tgioo  24684  tgqioo  24688  zdis  24705  xrge0tsms  24723  cnheibor  24854  lmmbr  25158  bcthlem4  25227  ovolicc2lem5  25422  dyadmbllem  25500  i1fd  25582  itg11  25592  itg2gt0  25661  itgeq1f  25672  itgeq1fOLD  25673  itgeq1  25674  bddmulibl  25740  ellimc2  25778  limcnlp  25779  ellimc3  25780  limcflf  25782  limciun  25795  lhop1lem  25918  ig1pdvds  26085  plycpn  26197  aannenlem2  26237  efopn  26567  xrlimcnp  26878  wilthlem2  26979  wilthlem3  26980  nodenselem8  27603  noetasuplem4  27648  noetainflem4  27652  nocvxminlem  27689  lrrecfr  27850  addsprop  27883  bdayon  28173  dfn0s2  28224  tghilberti1  28564  colline  28576  lmif  28712  islmib  28714  incistruhgr  29006  upgr1eopALT  29044  uhgrvtxedgiedgb  29063  upgredg2vtx  29068  edglnl  29070  numedglnl  29071  uhgr2edg  29135  umgrvad2edg  29140  usgredg4  29144  usgredg2vtxeuALT  29149  uspgredg2vlem  29150  ushgredgedg  29156  nbgr1vtx  29285  nbusgredgeu0  29295  nbusgrf1o0  29296  nb3grprlem1  29307  nb3grprlem2  29308  uvtx01vtx  29324  nbupgruvtxres  29334  cplgr1vlem  29356  cplgr1v  29357  vtxd0nedgb  29416  vtxduhgr0nedg  29420  1loopgrvd2  29431  1egrvtxdg0  29439  uspgrloopvtxel  29444  vtxdginducedm1lem4  29470  wlk1walk  29567  wlkp1lem1  29601  pthdivtx  29657  0enwwlksnge1  29794  umgrwwlks2on  29887  rusgr0edg  29903  eleclclwwlkn  30005  upgr4cycl4dv4e  30114  1conngr  30123  vdn0conngrumgrv2  30125  eupth2eucrct  30146  eupth2lem1  30147  frgrncvvdeqlem7  30234  frgrncvvdeqlem9  30236  frgrwopregasn  30245  frgrwopregbsn  30246  l2p  30408  lpni  30409  issh  31137  pjoc1  31363  h1dn0  31481  spansneleqi  31498  nonbooli  31580  pjch  31623  pjnel  31655  cdjreui  32361  rexunirn  32421  rabsnel  32429  nelun  32442  iinabrex  32498  opabdm  32539  opabrn  32540  fpwrelmapffslem  32655  fpwrelmap  32656  fz1nntr  32727  indval  32776  xrge0tsmsd  33002  nsgqusf1olem3  33386  elrspunidl  33399  isprmidl  33409  constrmon  33734  reff  33829  tpr2rico  33902  lmxrge0  33942  issiga  34102  isrnsiga  34103  isldsys  34146  isros  34158  issros  34165  ddeval1  34224  ddeval0  34225  ismbfm  34241  dya2icoseg  34268  dya2iocnrect  34272  ballotlem7  34527  bnj216  34722  bnj563  34733  bnj956  34766  bnj545  34885  bnj548  34887  bnj570  34895  bnj900  34919  bnj929  34926  bnj964  34933  bnj983  34941  bnj1001  34949  bnj1145  34983  bnj1398  35024  bnj1498  35051  wevgblacfn  35096  erdszelem1  35178  kur14lem9  35201  cnllysconn  35232  cvmsss2  35261  cvmcov2  35262  cvmsiota  35264  cvmopnlem  35265  cvmliftlem15  35285  satfv1  35350  satfdmlem  35355  mclsssvlem  35549  mclsind  35557  untelirr  35695  untsucf  35697  elintfv  35752  dfon2lem4  35774  dfon2lem7  35777  dfon2lem9  35779  dfiota3  35911  funpartlem  35930  funpartfun  35931  linethru  36141  hilbert1.1  36142  rankelg  36156  elhf2  36163  neibastop2lem  36348  bj-zfauscl  36912  bj-cleq  36950  bj-snsetex  36951  bj-clel3gALT  37036  bj-nuliota  37045  bj-isrvec  37282  mptsnunlem  37326  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  relowlpssretop  37352  exrecfnlem  37367  finxpeq1  37374  finxpreclem5  37383  finxpreclem6  37384  nlpineqsn  37396  fvineqsneq  37400  pibt2  37405  unccur  37597  fin2so  37601  matunitlindflem1  37610  ptrecube  37614  poimirlem9  37623  poimirlem30  37644  poimir  37647  heicant  37649  mblfinlem1  37651  ftc1anc  37695  ftc2nc  37696  cover2  37709  isbnd2  37777  prdstotbnd  37788  heibor1lem  37803  grpokerinj  37887  rngoueqz  37934  isidl  38008  1idl  38020  0rngo  38021  ispridl  38028  smprngopr  38046  isfldidl  38062  isdmn3  38068  mpobi123f  38156  iineq12f  38158  mptbi12f  38160  eqvrelqsel  38607  n0eldmqseq  38641  dmqseqim2  38649  disjlem17  38791  lsateln0  38988  ispsubsp  39739  linepsubN  39746  elpcliN  39887  dvh3dim3N  41443  dochsnnz  41444  mapdindp3  41716  sn-iotalem  42209  prjspval  42591  elmzpcl  42714  diophren  42801  dford3lem2  43016  ttac  43025  pw2f1ocnv  43026  wepwsolem  43031  kelac1  43052  onexgt  43229  onexlimgt  43232  ordnexbtwnsuc  43256  oaordnr  43285  omnord1  43294  nnoeomeqom  43301  oenord1  43305  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  omcl3g  43323  naddwordnexlem4  43390  nlimsuc  43430  intabssd  43508  elmapintrab  43565  eliunov2  43668  gneispaceel2  44133  mnuop23d  44255  mnuunid  44266  mnurndlem1  44270  expgrowthi  44322  dvconstbi  44323  tratrb  44526  suctrALT2VD  44825  suctrALT2  44826  en3lplem1VD  44832  en3lpVD  44834  tratrbVD  44850  suctrALTcf  44911  suctrALTcfVD  44912  suctrALT3  44913  unisnALT  44915  0elaxnul  44973  pwclaxpow  44974  prclaxpr  44975  uniclaxun  44976  omssaxinf2  44978  wfaxrep  44984  restuni3  45112  supminfxr  45460  xlimxrre  45829  xlimmnfvlem1  45830  xlimpnfvlem1  45834  icccncfext  45885  stoweidlem27  46025  stoweidlem35  46033  stoweidlem46  46044  stoweidlem52  46050  ioorrnopnlem  46302  ioorrnopnxrlem  46304  issal  46312  intsaluni  46327  salgencntex  46341  smfresal  46786  tannpoly  46891  funressnfv  47044  fnbrafvb  47155  afvco2  47177  ndmaovg  47185  aovmpt4g  47202  fafv2elrnb  47236  fvelsetpreimafv  47388  elsetpreimafvbi  47392  sprsymrelf1lem  47492  paireqne  47512  fpprbasnn  47730  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  dfclnbgr6  47856  dfsclnbgr6  47858  grtri  47939  stgrvtx0  47961  stgrnbgr0  47963  isubgr3stgrlem3  47967  gpgvtx0  48044  gpgvtx1  48045  gpg3kgrtriex  48080  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  rngccatidALTV  48260  ringccatidALTV  48294  ldepspr  48462  mosn  48801  indthinc  49451  indthincALT  49452