Theorem eleq2i 2822

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 2819	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 209   = wceq 1543   ∈ wcel 2112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809

This theorem is referenced by:  eleq12i  2823  eleqtri  2829  eleq2s  2849  hbxfreq  2859  nfceqi  2894  raleqbii  3146  rexeqbii  3235  rabeqi  3382  rabeq2i  3388  rabrabi  3393  elab2g  3578  elrabf  3587  elrab3t  3590  elrab2  3594  cbvsbcw  3717  cbvsbcvw  3718  cbvsbc  3719  elin2  4097  elsymdif  4148  noel  4231  noelOLD  4232  eltpg  4587  elunirab  4821  elintrab  4857  disjxiun  5036  exss  5332  otiunsndisj  5388  brabsb  5397  brabga  5400  epelg  5446  pofun  5471  elxp  5559  opeliunxp  5601  bropaex12  5624  brab2a  5626  elcnv  5730  dmopabelb  5770  elrnmptg  5813  elres  5875  elrid  5898  rninxp  6022  elid  6042  elsuci  6257  elsucg  6258  elsuc2g  6259  elfv  6693  0fv  6734  opabiota  6772  dffv2  6784  fvopab3g  6791  fvmptex  6810  fvopab5  6828  fvn0ssdmfun  6873  fveqressseq  6878  f0cli  6895  fmptco  6922  fvrnressn  6954  funfvima  7024  elunirnALT  7043  fliftel  7096  eloprabga  7296  eloprabgaOLD  7297  elrnmpo  7324  ovid  7328  offval  7455  suceloni  7570  1st2val  7767  2nd2val  7768  bropopvvv  7836  bropfvvvv  7838  fsplit  7863  fsplitOLD  7864  xporderlem  7872  brtpos2  7952  frrlem8  8012  frrlem9  8013  frrlem10  8014  wfrdmcl  8041  wfrfun  8043  wfrlem12  8044  wfrlem17  8049  wfr2  8052  issmo  8063  smores3  8068  tfrlem7  8097  tfrlem9  8099  tfrlem9a  8100  tfr2b  8110  tfr2  8112  rdgsuc  8138  frsucmptn  8152  tz7.48-2  8156  el1o  8204  dif1o  8205  ondif2  8207  oawordeulem  8260  elecg  8412  brecop  8470  erovlem  8473  eceqoveq  8482  mapsncnv  8552  mptelixpg  8594  brsdom  8629  isfi  8630  enssdom  8631  brdom2  8636  xpcomco  8713  brsdom2  8748  en3lplem2  9206  cnfcom2lem  9294  eltrpred  9309  epfrs  9325  r1limg  9352  r1ord  9361  r1ord3  9363  tz9.12lem3  9370  rankvaln  9380  r1elss  9387  rankpwi  9404  ssrankr1  9416  r1val3  9419  r1pw  9426  rankr1b  9445  djur  9500  djuunxp  9502  eldju2ndl  9505  eldju2ndr  9506  isnum2  9526  cardprclem  9560  infxpenlem  9592  alephcard  9649  alephnbtwn  9650  alephnbtwn2  9651  alephord2  9655  alephsdom  9665  dfac3  9700  dfac5lem2  9703  dfac5lem3  9704  dfac5lem5  9706  pwsdompw  9783  cfub  9828  cardcf  9831  cflecard  9832  cfle  9833  cflim2  9842  cofsmo  9848  cfidm  9854  isfin3  9875  isfin5  9878  isfin6  9879  sdom2en01  9881  fin23lem26  9904  fin23lem30  9921  isf32lem5  9936  itunitc1  9999  ituniiun  10001  axdc3lem3  10031  axcclem  10036  axdclem  10098  iunfo  10118  iundom2g  10119  cardidg  10127  konigthlem  10147  alephadd  10156  alephreg  10161  pwcfsdom  10162  cfpwsdom  10163  elgch  10201  fpwwe2lem11  10220  canth4  10226  wunex2  10317  r1tskina  10361  elni  10455  nlt1pi  10485  adderpq  10535  mulerpq  10536  recmulnq  10543  addsrpr  10654  mulsrpr  10655  opelcn  10708  opelreal  10709  elreal  10710  elreal2  10711  0ncn  10712  addcnsr  10714  mulcnsr  10715  xrlenlt  10863  elnn0  12057  elnnne0  12069  un0addcl  12088  un0mulcl  12089  elxnn0  12129  uztrn2  12422  elnnuz  12443  elnn0uz  12444  elq  12511  elxr  12673  elfzm1b  13155  elfz0lmr  13322  uzrdgfni  13496  fzennn  13506  ser0  13593  hash2pwpr  14007  iswrd  14036  pfxccatpfx1  14266  s3iunsndisj  14496  sumz  15251  sumss  15253  fsumcvg3  15258  abscvgcvg  15346  isumshft  15366  prodf1  15418  zprod  15462  prod1  15469  prodss  15472  prodsn  15487  prodsnf  15489  bpolydiflem  15579  bpoly2  15582  bpoly3  15583  bpoly4  15584  ruclem6  15759  divides  15780  dvdsflip  15841  pwp1fsum  15915  sadc0  15976  eulerthlem2  16298  prm23lt5  16330  4sqlem2  16465  4sqlem12  16472  vdwpc  16496  xpscf  17024  cidpropd  17167  oppcsect  17237  funcpropd  17361  natpropd  17439  dfinito2  17463  dftermo2  17464  initoeu2lem0  17473  arwhoma  17505  eldmcoa  17525  pospo  17805  psss  18040  ismgmn0  18070  gsumpropd2lem  18105  elefmndbas  18254  smndex1basss  18286  smndex1mgm  18288  pwmnd  18318  dfgrp2e  18347  mulgfval  18444  cycsubmel  18561  ghmeqker  18603  cntri  18679  oppgsubg  18709  fvcosymgeq  18775  symgfixels  18780  pmtrfrn  18804  efgsfo  19083  efgrelexlemb  19094  lt6abl  19234  dmdprd  19339  dprdval  19344  dprdw  19351  srgbinomlem4  19512  isnirred  19672  isrhm  19695  issrng  19840  lspexchn2  20122  lspindp2l  20125  lspindp2  20126  lbsextlem2  20150  cnfldfunALT  20330  dsmmelbas  20655  frlmbas3  20692  lindsind2  20735  islindf4  20754  psrbagf  20831  evlslem4  20988  ply1bascl2  21079  cply1mul  21169  lply1binom  21181  matsubgcell  21285  matinvgcell  21286  matvscacell  21287  matepmcl  21313  matepm2cl  21314  scmatscm  21364  smatvscl  21375  marrepcl  21415  marepvcl  21420  mulmarep1el  21423  mulmarep1gsum1  21424  mulmarep1gsum2  21425  submabas  21429  m1detdiag  21448  mdetdiag  21450  m2detleib  21482  gsummatr01lem3  21508  gsummatr01  21510  smadiadetlem4  21520  slesolinv  21531  slesolinvbi  21532  slesolex  21533  cramerimplem2  21535  pmatcoe1fsupp  21552  mat2pmatbas  21577  mat2pmatmul  21582  mat2pmatlin  21586  decpmatmul  21623  monmatcollpw  21630  pm2mpf1  21650  pm2mpghm  21667  istps  21785  mretopd  21943  neiptopuni  21981  lpdifsn  21994  restcls  22032  perfopn  22036  pnfnei  22071  mnfnei  22072  lmss  22149  hauscmplem  22257  is2ndc  22297  2ndcdisj  22307  hausnlly  22344  txuni2  22416  ptpjpre1  22422  elpt  22423  dfac14  22469  xkococn  22511  fbasrn  22735  fin1aufil  22783  elfm2  22799  elfm3  22801  fbflim  22827  flffbas  22846  cnpflf2  22851  fclsbas  22872  efmndtmd  22952  tsmssubm  22994  iscusp2  23153  imasdsf1olem  23225  metustel  23402  metuel2  23417  isnghm  23575  opnreen  23682  iccpnfcnv  23795  ehleudisval  24270  ehl1eudis  24271  ehl2eudis  24273  minveclem3b  24279  ovoliunlem1  24353  ioombl1lem4  24412  subopnmbl  24455  vitalilem2  24460  vitalilem3  24461  mbfimaopnlem  24506  mbfimaopn2  24508  itg2l  24581  dvply1  25131  vieta1lem1  25157  vieta1lem2  25158  elaa  25163  taylthlem2  25220  abelthlem6  25282  abelthlem9  25286  sinq34lt0t  25353  ellogrn  25402  dvrelog  25479  ellogdm  25481  logtayl2  25504  cxpcn3lem  25587  cxpcn3  25588  1cubr  25679  atandm  25713  atanf  25717  reasinsin  25733  atans2  25768  dmarea  25794  xrlimcnp  25805  amgmlem  25826  ppiublem1  26037  lgsdir2lem2  26161  gausslemma2dlem1a  26200  lgsquadlem1  26215  lgsquadlem2  26216  2sqlem1  26252  rpvmasum2  26347  edgiedgb  27099  isuhgr  27105  isushgr  27106  isupgr  27129  isumgr  27140  umgredg  27183  umgrpredgv  27185  umgredgne  27190  umgredgnlp  27192  isuspgr  27197  isusgr  27198  ausgrusgri  27213  usgredgppr  27238  edgssv2  27240  uspgredg2vlem  27265  uspgredg2v  27266  ushgredgedg  27271  ushgredgedgloop  27273  griedg0ssusgr  27307  uhgrissubgr  27317  subumgredg2  27327  uhgrspansubgrlem  27332  umgrres1lem  27352  upgrres1  27355  nbgrcl  27377  nbuhgr  27385  nbuhgr2vtx1edgblem  27393  nbupgrres  27406  edgnbusgreu  27409  nbusgredgeu0  27410  nbusgrf1o0  27411  hashnbusgrnn0  27418  nbupgruvtxres  27449  cffldtocusgr  27489  cusgrfilem2  27498  vtxdg0v  27515  vtxduhgr0nedg  27534  uhgrvd00  27576  vtxdginducedm1  27585  finsumvtxdg2ssteplem4  27590  wlk1walk  27680  wlkp1lem6  27720  iswwlks  27874  wwlknllvtx  27884  wwlksonvtx  27893  wspthnonp  27897  wlkiswwlksupgr2  27915  wwlksnwwlksnon  27953  2pthon3v  27981  umgr2wlk  27987  elwwlks2s3  27989  wwlks2onv  27991  elwwlks2ons3im  27992  isclwwlk  28021  clwwlkccatlem  28026  clwlkclwwlk  28039  wwlksext2clwwlk  28094  hashecclwwlkn1  28114  umgrhashecclwwlk  28115  clwwlknon1  28134  clwwlknon1nloop  28136  clwwlknon2x  28140  1pthon2v  28190  uhgr3cyclex  28219  isconngr  28226  isconngr1  28227  eucrctshift  28280  frgrnbnb  28330  frgrncvvdeqlem1  28336  frgrncvvdeqlem2  28337  frgrncvvdeqlem3  28338  frgrncvvdeqlem9  28344  fusgreghash2wspv  28372  extwwlkfab  28389  numclwwlk1lem2foa  28391  numclwwlk1lem2fo  28395  clwlknon2num  28405  numclwlk2lem2f1o  28416  numclwwlk5lem  28424  topnfbey  28506  isvclem  28612  isnvlem  28645  vsfval  28668  h2hlm  29015  hhcmpl  29235  hhcms  29238  elch0  29289  omlsilem  29437  h1de2ctlem  29590  elspansni  29593  nonbooli  29686  spansncvi  29687  adjeq  29970  cnlnssadj  30115  cnvbraval  30145  brabgaf  30621  elimampt  30646  2ndresdju  30659  fmptdF  30667  fmptcof2  30668  acunirnmpt  30670  acunirnmpt2  30671  ofpreima  30676  fcnvgreu  30684  fdifsuppconst  30697  1stpreima  30713  2ndpreima  30714  fz2ssnn0  30780  elxrge02  30880  psgnfzto1stlem  31040  cycpmgcl  31093  nsgqusf1olem2  31267  nsgqusf1olem3  31268  prmidl0  31294  submatres  31424  lmat22lem  31435  crefdf  31466  cmppcmp  31476  rspectopn  31485  prsdm  31532  prsrn  31533  xrge0iifcnv  31551  xrge0iifiso  31553  xrge0iifhom  31555  pnfneige0  31569  qqhre  31636  rrhre  31637  esumnul  31682  esumcvgsum  31722  ldgenpisyslem1  31797  measvuni  31848  cntnevol  31862  dya2iocnrect  31914  sibf0  31967  oddpwdc  31987  eulerpartlemd  31999  eulerpartgbij  32005  eulerpartlemgh  32011  isrrvv  32076  coinfliprv  32115  ballotlem7  32168  signswch  32206  hashreprin  32266  chtvalz  32275  circlemethhgt  32289  hgt750lemb  32302  tgoldbachgt  32309  bnj23  32363  bnj158  32374  bnj168  32375  bnj1138  32435  bnj1143  32437  bnj1454  32489  bnj110  32505  bnj882  32573  bnj893  32575  bnj916  32580  bnj970  32594  bnj983  32598  bnj984  32599  bnj1137  32642  bnj1174  32650  bnj1388  32680  bnj1398  32681  loop1cycl  32766  subfacp1lem5  32813  satfv1  32992  satfrnmapom  32999  satf0op  33006  satf0n0  33007  fmlafvel  33014  fmlaomn0  33019  fmlan0  33020  satffunlem2lem2  33035  satfv0fvfmla0  33042  satefvfmla0  33047  mrsub0  33145  mrsubccat  33147  mrsubcn  33148  elmrsubrn  33149  msubco  33160  msubvrs  33189  elmthm  33205  mthmblem  33209  elrn3  33399  dfon2lem7  33435  frpoins3xpg  33457  frpoins3xp3g  33458  madeval2  33723  newval  33725  leftval  33733  rightval  33734  madess  33745  oldssmade  33746  lrold  33763  brsset  33877  eltrans  33879  elfix  33891  ellimits  33898  elfuns  33903  elsingles  33906  fvtransport  34020  brcolinear2  34046  fvray  34129  linedegen  34131  fvline  34132  ellines  34140  fwddifn0  34152  elhf  34162  hfninf  34174  fnessref  34232  bj-ififc  34449  bj-csbsnlem  34775  bj-elgab  34813  currysetlem1  34822  bj-eltag  34853  bj-sngltag  34859  bj-projun  34870  bj-0nelmpt  34971  bj-opelidres  35016  bj-inftyexpitaudisj  35060  bj-elccinfty  35069  f1omptsnlem  35193  icoreelrnab  35211  relowlpssretop  35221  rdgssun  35235  exrecfnlem  35236  finxpnom  35258  uncov  35444  tan2h  35455  ptrecube  35463  poimirlem25  35488  poimirlem29  35492  poimirlem30  35493  poimirlem31  35494  poimirlem32  35495  cnambfre  35511  ftc1cnnc  35535  sdclem2  35586  sdclem1  35587  fdc  35589  caushft  35605  issmgrpOLD  35707  ismndo  35716  isrngo  35741  isdivrngo  35794  csbcom2fi  35972  elecALTV  36091  brrabga  36162  eldmcoss  36262  coss0  36283  elrels2  36290  dath  37436  diclspsn  38894  dvh4dimlem  39143  dvh2dim  39145  dvh3dim3N  39149  lcfrvalsnN  39241  mapdh6eN  39440  mapdh7dN  39450  mapdh8b  39480  hdmap1l6e  39514  lcmfunnnd  39703  3factsumint1  39712  sticksstones2  39772  sticksstones3  39773  sticksstones10  39780  sticksstones12a  39782  sticksstones12  39783  elab2gw  39829  frlmfielbas  39885  mhpind  39934  pellex  40301  rmspecnonsq  40373  islmodfg  40538  aaitgo  40631  areaquad  40691  elcnvcnvintab  40807  elnonrel  40810  elcnvcnvlem  40824  cnvcnvintabd  40825  brfvrcld2  40918  grur1cld  41464  dvgrat  41544  cvgdvgrat  41545  radcnvrat  41546  nznngen  41548  uzmptshftfval  41578  binomcxplemcvg  41586  binomcxplemnotnn0  41588  tpid3gVD  42076  en3lplem2VD  42078  rexanuz3  42260  eliuniin  42263  eliuniin2  42283  disjinfi  42345  fsneq  42360  iuneqfzuzlem  42487  allbutfi  42547  eluzelz2  42557  uz0  42566  uzublem  42584  uzid3  42589  elicores  42687  uzinico  42714  climsuselem1  42766  climsuse  42767  islptre  42778  fnlimfvre  42833  limsupresico  42859  limsupvaluz  42867  limsupubuzlem  42871  limsupequzmptlem  42887  liminfresico  42930  cnrefiisplem  42988  stoweidlem14  43173  stoweidlem39  43198  stoweidlem48  43207  stoweidlem51  43210  stoweidlem59  43218  stoweidlem62  43221  wallispilem3  43226  fourierdlem42  43308  fourierdlem62  43327  fourierdlem80  43345  fourierdlem103  43368  fourierdlem104  43369  etransclem26  43419  rrxsnicc  43459  ioorrnopn  43464  ioorrnopnxr  43466  sge00  43532  sge0fodjrnlem  43572  sge0isum  43583  sge0seq  43602  meadjiunlem  43621  carageneld  43658  volicorescl  43709  hoidmv1lelem1  43747  hoidmv1le  43750  hoidmvlelem1  43751  hoidmvlelem3  43753  ovnhoilem2  43758  hoiqssbllem2  43779  opnvonmbllem2  43789  ovolval4lem1  43805  iinhoiicc  43830  vonioolem1  43836  smflimlem1  43921  smflimlem2  43922  smflim  43927  nsssmfmbf  43929  smfresal  43937  smfrec  43938  smfdiv  43946  smfpimbor1lem2  43948  smflim2  43954  smflimmpt  43958  smfsupmpt  43963  smfinflem  43965  smfinfmpt  43967  smflimsuplem1  43968  smflimsuplem2  43969  smflimsuplem3  43970  smflimsuplem5  43972  smflimsuplem6  43973  smflimsup  43976  smflimsupmpt  43977  smfliminfmpt  43980  fcores  44176  ndmaovcl  44310  ndmaovcom  44312  ndmaovass  44313  ndmaovdistr  44314  dfatco  44363  otiunsndisjX  44386  fvmptrabdm  44400  elsetpreimafvb  44452  sprsymrelfolem2  44561  sprsymrelf  44563  sprsymrelf1  44564  prpair  44569  prproropf1olem0  44570  paireqne  44579  fmtno4prmfac  44640  dfodd5  44728  sbgoldbo  44855  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  isomushgr  44894  isomuspgrlem2c  44898  uspgrsprf  44924  uspgrsprf1  44925  uspgrsprfo  44926  opeliun2xp  45284  ply1sclrmsm  45340  lcoop  45368  lincfsuppcl  45370  linccl  45371  lincvalsng  45373  lincvalpr  45375  lincvalsc0  45378  linc0scn0  45380  lincdifsn  45381  linc1  45382  lincsum  45386  lincscm  45387  lspsslco  45394  snlindsntor  45428  lincresunit3lem2  45437  ldepsnlinclem1  45462  ldepsnlinclem2  45463  prelrrx2  45675  prelrrx2b  45676  rrx2xpref1o  45680  rrx2plord  45682  rrx2linesl  45705  oppcthin  45936  indthinc  45949  prsthinc  45951  elpglem3  46032