Theorem eleq2i 2833

Description: Inference from equality to equivalence of membership. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2830	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ 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 2708

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

This theorem is referenced by:  eleq12i  2834  eleqtri  2839  eleq2s  2859  hbxfreq  2872  nfceqi  2902  raleqbii  3344  rexeqbii  3345  rabeqi  3450  rabrabi  3456  reqabi  3460  elab2gw  3678  elab2g  3680  elrabf  3688  elrab3t  3691  elrab2  3695  cbvsbcw  3821  cbvsbcvw  3822  cbvsbc  3823  elin2  4203  elsymdif  4258  noel  4338  eltpg  4686  elunirab  4922  elintrab  4960  disjxiun  5140  exss  5468  otiunsndisj  5525  brabsb  5536  brabga  5539  epelg  5585  pofun  5610  elxp  5708  opeliunxp  5752  opeliun2xp  5753  bropaex12  5777  brab2a  5779  elcnv  5887  dmopabelb  5927  elrnmptg  5972  elres  6038  elimampt  6061  elrid  6064  rninxp  6199  elid  6219  elsuci  6451  elsucg  6452  elsuc2g  6453  elfv  6904  0fv  6950  opabiota  6991  dffv2  7004  fvopab3g  7011  fvmptex  7030  fvopab5  7049  fvn0ssdmfun  7094  fveqressseq  7099  f0cli  7118  fmptco  7149  fvrnressn  7181  funfvima  7250  elunirnALT  7272  fliftel  7329  eloprabga  7542  elrnmpo  7569  elimampo  7570  ovid  7574  offval  7706  sucexeloniOLD  7830  suceloniOLD  7832  1st2val  8042  2nd2val  8043  bropopvvv  8115  bropfvvvv  8117  fsplit  8142  xporderlem  8152  frpoins3xpg  8165  frpoins3xp3g  8166  brtpos2  8257  frrlem8  8318  frrlem9  8319  frrlem10  8320  fprresex  8335  wfrdmclOLD  8357  wfrfunOLD  8359  wfrlem12OLD  8360  wfrlem17OLD  8365  wfr2OLD  8368  issmo  8388  smores3  8393  tfrlem7  8423  tfrlem9  8425  tfrlem9a  8426  tfr2b  8436  tfr2  8438  rdgsuc  8464  frsucmptn  8479  tz7.48-2  8482  el1o  8533  ord2eln012  8535  dif1o  8538  ondif2  8540  oawordeulem  8592  elecg  8789  brecop  8850  erovlem  8853  eceqoveq  8862  mapsncnv  8933  mptelixpg  8975  brsdom  9015  isfi  9016  enssdom  9017  brdom2  9022  xpcomco  9102  brsdom2  9137  en3lplem2  9653  cnfcom2lem  9741  brttrcl2  9754  ttrcltr  9756  rnttrcl  9762  epfrs  9771  r1limg  9811  r1ord  9820  r1ord3  9822  tz9.12lem3  9829  rankvaln  9839  r1elss  9846  rankpwi  9863  ssrankr1  9875  r1val3  9878  r1pw  9885  rankr1b  9904  djur  9959  djuunxp  9961  eldju2ndl  9964  eldju2ndr  9965  isnum2  9985  cardprclem  10019  infxpenlem  10053  alephcard  10110  alephnbtwn  10111  alephnbtwn2  10112  alephord2  10116  alephsdom  10126  dfac3  10161  dfac5lem2  10164  dfac5lem3  10165  dfac5lem5  10167  pwsdompw  10243  cfub  10289  cardcf  10292  cflecard  10293  cfle  10294  cflim2  10303  cofsmo  10309  cfidm  10315  isfin3  10336  isfin5  10339  isfin6  10340  sdom2en01  10342  fin23lem26  10365  fin23lem30  10382  isf32lem5  10397  itunitc1  10460  ituniiun  10462  axdc3lem3  10492  axcclem  10497  axdclem  10559  iunfo  10579  iundom2g  10580  cardidg  10588  konigthlem  10608  alephadd  10617  alephreg  10622  pwcfsdom  10623  cfpwsdom  10624  elgch  10662  fpwwe2lem11  10681  canth4  10687  wunex2  10778  r1tskina  10822  elni  10916  nlt1pi  10946  adderpq  10996  mulerpq  10997  recmulnq  11004  addsrpr  11115  mulsrpr  11116  opelcn  11169  opelreal  11170  elreal  11171  elreal2  11172  0ncn  11173  addcnsr  11175  mulcnsr  11176  xrlenlt  11326  elnn0  12528  elnnne0  12540  un0addcl  12559  un0mulcl  12560  elxnn0  12601  uztrn2  12897  elnnuz  12922  elnn0uz  12923  elq  12992  elxr  13158  elfzm1b  13642  elfz0lmr  13821  uzrdgfni  13999  fzennn  14009  ser0  14095  hash2pwpr  14515  iswrd  14554  pfxccatpfx1  14774  s3iunsndisj  15007  sumz  15758  sumss  15760  fsumcvg3  15765  abscvgcvg  15855  isumshft  15875  prodf1  15927  prodeq1i  15952  zprod  15973  prod1  15980  prodss  15983  prodsn  15998  prodsnf  16000  bpolydiflem  16090  bpoly2  16093  bpoly3  16094  bpoly4  16095  ruclem6  16271  divides  16292  dvdsflip  16354  pwp1fsum  16428  sadc0  16491  eulerthlem2  16819  prm23lt5  16852  4sqlem2  16987  4sqlem12  16994  vdwpc  17018  xpscf  17610  cidpropd  17753  oppcsect  17822  funcpropd  17947  natpropd  18024  dfinito2  18048  dftermo2  18049  initoeu2lem0  18058  arwhoma  18090  eldmcoa  18110  pospo  18390  psss  18625  ismgmn0  18655  gsumpropd2lem  18692  elefmndbas  18886  smndex1basss  18918  smndex1mgm  18920  pwmnd  18950  dfgrp2e  18981  mulgfval  19087  eqg0subg  19214  cycsubmel  19218  ghmeqker  19261  elcntr  19348  cntri  19350  cntzsgrpcl  19352  oppgsubg  19382  fvcosymgeq  19447  symgfixels  19452  pmtrfrn  19476  efgsfo  19757  efgrelexlemb  19768  lt6abl  19913  dmdprd  20018  dprdval  20023  dprdw  20030  srgbinomlem4  20226  isnirred  20420  isrhm  20478  issrng  20845  lspexchn2  21133  lspindp2l  21136  lspindp2  21137  lbsextlem2  21161  rnglidl1  21242  df2idl2  21267  2idlss  21272  rngqiprngimfo  21311  cnfldfun  21378  cnfldfunOLD  21391  pzriprnglem3  21494  pzriprnglem4  21495  pzriprnglem7  21498  pzriprnglem8  21499  pzriprnglem9  21500  pzriprnglem12  21503  pzriprnglem14  21505  dsmmelbas  21759  frlmbas3  21796  lindsind2  21839  islindf4  21858  psrbagf  21938  evlslem4  22100  psdmul  22170  ply1bascl2  22206  cply1mul  22300  lply1binom  22314  matsubgcell  22440  matinvgcell  22441  matvscacell  22442  matepmcl  22468  matepm2cl  22469  scmatscm  22519  smatvscl  22530  marrepcl  22570  marepvcl  22575  mulmarep1el  22578  mulmarep1gsum1  22579  mulmarep1gsum2  22580  submabas  22584  m1detdiag  22603  mdetdiag  22605  m2detleib  22637  gsummatr01lem3  22663  gsummatr01  22665  smadiadetlem4  22675  slesolinv  22686  slesolinvbi  22687  slesolex  22688  cramerimplem2  22690  pmatcoe1fsupp  22707  mat2pmatbas  22732  mat2pmatmul  22737  mat2pmatlin  22741  decpmatmul  22778  monmatcollpw  22785  pm2mpf1  22805  pm2mpghm  22822  istps  22940  mretopd  23100  neiptopuni  23138  lpdifsn  23151  restcls  23189  perfopn  23193  pnfnei  23228  mnfnei  23229  lmss  23306  hauscmplem  23414  is2ndc  23454  2ndcdisj  23464  hausnlly  23501  txuni2  23573  ptpjpre1  23579  elpt  23580  dfac14  23626  xkococn  23668  fbasrn  23892  fin1aufil  23940  elfm2  23956  elfm3  23958  fbflim  23984  flffbas  24003  cnpflf2  24008  fclsbas  24029  efmndtmd  24109  tsmssubm  24151  iscusp2  24311  imasdsf1olem  24383  metustel  24563  metuel2  24578  isnghm  24744  opnreen  24853  iccpnfcnv  24975  ehleudisval  25453  ehl1eudis  25454  ehl2eudis  25456  minveclem3b  25462  ovoliunlem1  25537  ioombl1lem4  25596  subopnmbl  25639  vitalilem2  25644  vitalilem3  25645  mbfimaopnlem  25690  mbfimaopn2  25692  itg2l  25764  dvply1  26325  vieta1lem1  26352  vieta1lem2  26353  elaa  26358  taylthlem2  26416  taylthlem2OLD  26417  abelthlem6  26480  abelthlem9  26484  sinq34lt0t  26551  ellogrn  26601  dvrelog  26679  ellogdm  26681  logtayl2  26704  cxpcn3lem  26790  cxpcn3  26791  1cubr  26885  atandm  26919  atanf  26923  reasinsin  26939  atans2  26974  dmarea  27000  xrlimcnp  27011  amgmlem  27033  ppiublem1  27246  lgsdir2lem2  27370  gausslemma2dlem1a  27409  lgsquadlem1  27424  lgsquadlem2  27425  2sqlem1  27461  rpvmasum2  27556  madeval2  27892  newval  27894  leftval  27902  rightval  27903  lltropt  27911  madess  27915  oldssmade  27916  lrold  27935  addsproplem2  28003  addsproplem4  28005  addsproplem6  28007  negsproplem4  28063  negsproplem6  28065  precsexlem10  28240  precsexlem11  28241  sltonold  28283  elnns  28343  elzs  28370  edgiedgb  29071  isuhgr  29077  isushgr  29078  isupgr  29101  isumgr  29112  umgredg  29155  umgrpredgv  29157  umgredgne  29162  umgredgnlp  29164  isuspgr  29169  isusgr  29170  ausgrusgri  29185  usgredgppr  29213  edgssv2  29215  uspgredg2vlem  29240  uspgredg2v  29241  ushgredgedg  29246  ushgredgedgloop  29248  griedg0ssusgr  29282  uhgrissubgr  29292  subumgredg2  29302  uhgrspansubgrlem  29307  umgrres1lem  29327  upgrres1  29330  nbgrcl  29352  nbuhgr  29360  nbuhgr2vtx1edgblem  29368  nbupgrres  29381  edgnbusgreu  29384  nbusgredgeu0  29385  nbusgrf1o0  29386  hashnbusgrnn0  29393  nbupgruvtxres  29424  cffldtocusgr  29464  cffldtocusgrOLD  29465  cusgrfilem2  29474  vtxdg0v  29491  vtxduhgr0nedg  29510  uhgrvd00  29552  vtxdginducedm1  29561  finsumvtxdg2ssteplem4  29566  wlk1walk  29657  wlkp1lem6  29696  iswwlks  29856  wwlknllvtx  29866  wwlksonvtx  29875  wspthnonp  29879  wlkiswwlksupgr2  29897  wwlksnwwlksnon  29935  2pthon3v  29963  umgr2wlk  29969  elwwlks2s3  29971  wwlks2onv  29973  elwwlks2ons3im  29974  isclwwlk  30003  clwwlkccatlem  30008  clwlkclwwlk  30021  wwlksext2clwwlk  30076  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknon1  30116  clwwlknon1nloop  30118  clwwlknon2x  30122  1pthon2v  30172  uhgr3cyclex  30201  isconngr  30208  isconngr1  30209  eucrctshift  30262  frgrnbnb  30312  frgrncvvdeqlem1  30318  frgrncvvdeqlem2  30319  frgrncvvdeqlem3  30320  frgrncvvdeqlem9  30326  fusgreghash2wspv  30354  extwwlkfab  30371  numclwwlk1lem2foa  30373  numclwwlk1lem2fo  30377  clwlknon2num  30387  numclwlk2lem2f1o  30398  numclwwlk5lem  30406  topnfbey  30488  isvclem  30596  isnvlem  30629  vsfval  30652  h2hlm  30999  hhcmpl  31219  hhcms  31222  elch0  31273  omlsilem  31421  h1de2ctlem  31574  elspansni  31577  nonbooli  31670  spansncvi  31671  adjeq  31954  cnlnssadj  32099  cnvbraval  32129  brabgaf  32620  2ndresdju  32659  fmptdF  32666  fmptcof2  32667  acunirnmpt  32669  acunirnmpt2  32670  ofpreima  32675  fcnvgreu  32683  fdifsuppconst  32698  1stpreima  32716  2ndpreima  32717  fz2ssnn0  32787  elxrge02  32914  ccatws1f1o  32936  gsumwrd2dccatlem  33069  psgnfzto1stlem  33120  cycpmgcl  33173  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem1  33251  nsgqusf1olem2  33442  nsgqusf1olem3  33443  prmidl0  33478  crngmxidl  33497  opprnsg  33512  rprmirredb  33560  zringfrac  33582  evl1deg2  33602  evl1deg3  33603  ply1degltel  33615  ply1degleel  33616  fldextrspunlsplem  33723  isconstr  33777  constrsuc  33779  constrconj  33786  submatres  33805  lmat22lem  33816  crefdf  33847  cmppcmp  33857  rspectopn  33866  prsdm  33913  prsrn  33914  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  pnfneige0  33950  qqhre  34021  rrhre  34022  esumnul  34049  esumcvgsum  34089  ldgenpisyslem1  34164  measvuni  34215  cntnevol  34229  dya2iocnrect  34283  sibf0  34336  oddpwdc  34356  eulerpartlemd  34368  eulerpartgbij  34374  eulerpartlemgh  34380  isrrvv  34445  coinfliprv  34485  ballotlem7  34538  signswch  34576  hashreprin  34635  chtvalz  34644  circlemethhgt  34658  hgt750lemb  34671  tgoldbachgt  34678  bnj23  34732  bnj158  34743  bnj168  34744  bnj1138  34802  bnj1143  34804  bnj1454  34856  bnj110  34872  bnj882  34940  bnj893  34942  bnj916  34947  bnj970  34961  bnj983  34965  bnj984  34966  bnj1137  35009  bnj1174  35017  bnj1388  35047  bnj1398  35048  loop1cycl  35142  subfacp1lem5  35189  satfv1  35368  satfrnmapom  35375  satf0op  35382  satf0n0  35383  fmlafvel  35390  fmlaomn0  35395  fmlan0  35396  satffunlem2lem2  35411  satfv0fvfmla0  35418  satefvfmla0  35423  mrsub0  35521  mrsubccat  35523  mrsubcn  35524  elmrsubrn  35525  msubco  35536  msubvrs  35565  elmthm  35581  mthmblem  35585  ellcsrspsn  35646  elrn3  35762  dfon2lem7  35790  brsset  35890  eltrans  35892  elfix  35904  ellimits  35911  elfuns  35916  elsingles  35919  fvtransport  36033  brcolinear2  36059  fvray  36142  linedegen  36144  fvline  36145  ellines  36153  fwddifn0  36165  elhf  36175  hfninf  36187  rmoeqi  36188  rmoeqbii  36189  reueqi  36190  reueqbii  36191  rabeqbii  36195  iuneq12i  36196  iineq1i  36197  iineq12i  36198  riotaeqbii  36199  ixpeq1i  36201  itgeq12i  36207  cbvprodvw2  36248  fnessref  36358  bj-ififc  36583  bj-csbsnlem  36904  bj-elgab  36940  currysetlem1  36948  bj-eltag  36978  bj-sngltag  36984  bj-projun  36995  bj-velpwALT  37054  bj-0nelmpt  37117  bj-opelidres  37162  bj-inftyexpitaudisj  37206  bj-elccinfty  37215  f1omptsnlem  37337  icoreelrnab  37355  relowlpssretop  37365  rdgssun  37379  exrecfnlem  37380  finxpnom  37402  uncov  37608  tan2h  37619  ptrecube  37627  poimirlem25  37652  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  cnambfre  37675  ftc1cnnc  37699  sdclem2  37749  sdclem1  37750  fdc  37752  caushft  37768  issmgrpOLD  37870  ismndo  37879  isrngo  37904  isdivrngo  37957  csbcom2fi  38135  elecALTV  38267  brrabga  38342  eldmcoss  38459  coss0  38480  elrels2  38487  dath  39738  diclspsn  41196  dvh4dimlem  41445  dvh2dim  41447  dvh3dim3N  41451  lcfrvalsnN  41543  mapdh6eN  41742  mapdh7dN  41752  mapdh8b  41782  hdmap1l6e  41816  lcmfunnnd  42013  3factsumint1  42022  primrootsunit1  42098  primrootscoprmpow  42100  aks6d1c2lem4  42128  sticksstones2  42148  sticksstones3  42149  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem2  42172  aks6d1c6lem3  42173  redvmptabs  42390  readvrec2  42391  readvrec  42392  frlmfielbas  42510  mhpind  42604  pellex  42846  rmspecnonsq  42918  islmodfg  43081  aaitgo  43174  areaquad  43228  ordeldif1o  43273  naddwordnexlem4  43414  fpwfvss  43425  finona1cl  43466  elcnvcnvintab  43595  elnonrel  43598  elcnvcnvlem  43612  cnvcnvintabd  43613  brfvrcld2  43705  grur1cld  44251  dvgrat  44331  cvgdvgrat  44332  radcnvrat  44333  nznngen  44335  uzmptshftfval  44365  binomcxplemcvg  44373  binomcxplemnotnn0  44375  tpid3gVD  44862  en3lplem2VD  44864  wfaxrep  45011  wfaxsep  45012  wfaxpow  45014  wfaxpr  45015  wfaxun  45016  wfac8prim  45019  iuneq1i  45090  rexanuz3  45101  eliuniin  45104  eliuniin2  45125  disjinfi  45197  fsneq  45211  iuneqfzuzlem  45345  allbutfi  45404  eluzelz2  45414  uz0  45423  uzublem  45441  uzid3  45446  elicores  45546  uzinico  45573  climsuselem1  45622  climsuse  45623  islptre  45634  fnlimfvre  45689  limsupresico  45715  limsupvaluz  45723  limsupubuzlem  45727  limsupequzmptlem  45743  liminfresico  45786  cnrefiisplem  45844  stoweidlem14  46029  stoweidlem39  46054  stoweidlem48  46063  stoweidlem51  46066  stoweidlem59  46074  stoweidlem62  46077  wallispilem3  46082  fourierdlem42  46164  fourierdlem62  46183  fourierdlem80  46201  fourierdlem103  46224  fourierdlem104  46225  etransclem26  46275  rrxsnicc  46315  ioorrnopn  46320  ioorrnopnxr  46322  sge00  46391  sge0fodjrnlem  46431  sge0isum  46442  sge0seq  46461  meadjiunlem  46480  carageneld  46517  volicorescl  46568  hoidmv1lelem1  46606  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem3  46612  ovnhoilem2  46617  hoiqssbllem2  46638  opnvonmbllem2  46648  ovolval4lem1  46664  iinhoiicc  46689  vonioolem1  46695  smflimlem1  46786  smflimlem2  46787  smflim  46792  nsssmfmbf  46794  smfresal  46803  smfrec  46804  smfdiv  46812  smfpimbor1lem2  46814  smflim2  46821  smflimmpt  46825  smfinflem  46832  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem5  46839  smflimsuplem6  46840  smflimsup  46843  smflimsupmpt  46844  smfliminfmpt  46847  fcores  47079  ndmaovcl  47215  ndmaovcom  47217  ndmaovass  47218  ndmaovdistr  47219  dfatco  47268  otiunsndisjX  47291  fvmptrabdm  47305  elsetpreimafvb  47371  sprsymrelfolem2  47480  sprsymrelf  47482  sprsymrelf1  47483  prpair  47488  prproropf1olem0  47489  paireqne  47498  fmtno4prmfac  47559  dfodd5  47647  sbgoldbo  47774  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  clnbgrcl  47808  clnbgredg  47826  sclnbgrel  47833  isubgredg  47852  isuspgrim0  47872  isuspgrimlem  47874  gricushgr  47886  clnbgrgrimlem  47901  grimedg  47903  usgrgrtrirex  47917  stgrnbgr0  47931  isubgr3stgrlem3  47935  isubgr3stgrlem4  47936  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  uspgrlimlem2  47956  uspgrlimlem3  47957  grlimgrtrilem1  47961  grlimgrtrilem2  47962  usgrexmpl2trifr  47996  gpgvtxel  48005  gpgedgel  48007  gpgusgralem  48011  gpg5order  48014  ceilhalfelfzo1  48016  gpgvtxedg0  48021  gpgvtxedg1  48022  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  gpg3nbgrvtx1  48034  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpgvtxdg3  48038  gpg5gricstgr3  48046  uspgrsprf  48062  uspgrsprf1  48063  uspgrsprfo  48064  ply1sclrmsm  48300  lcoop  48328  lincfsuppcl  48330  linccl  48331  lincvalsng  48333  lincvalpr  48335  lincvalsc0  48338  linc0scn0  48340  lincdifsn  48341  linc1  48342  lincsum  48346  lincscm  48347  lspsslco  48354  snlindsntor  48388  lincresunit3lem2  48397  ldepsnlinclem1  48422  ldepsnlinclem2  48423  prelrrx2  48634  prelrrx2b  48635  rrx2xpref1o  48639  rrx2plord  48641  rrx2linesl  48664  oppcthin  49087  indthinc  49109  prsthinc  49111  elpglem3  49232