Theorem eleq2i 2830

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eleq12i  2831  eleqtri  2837  eleq2s  2857  hbxfreq  2868  nfceqi  2903  raleqbii  3160  rexeqbii  3255  rabeqi  3406  rabeq2i  3412  rabrabi  3417  elab2g  3604  elrabf  3613  elrab3t  3616  elrab2  3620  cbvsbcw  3745  cbvsbcvw  3746  cbvsbc  3747  elin2  4127  elsymdif  4178  noel  4261  noelOLD  4262  eltpg  4618  elunirab  4852  elintrab  4888  disjxiun  5067  exss  5372  otiunsndisj  5428  brabsb  5437  brabga  5440  epelg  5487  pofun  5512  elxp  5603  opeliunxp  5645  bropaex12  5668  brab2a  5670  elcnv  5774  dmopabelb  5814  elrnmptg  5857  elres  5919  elrid  5942  rninxp  6071  elid  6091  elsuci  6317  elsucg  6318  elsuc2g  6319  elfv  6754  0fv  6795  opabiota  6833  dffv2  6845  fvopab3g  6852  fvmptex  6871  fvopab5  6889  fvn0ssdmfun  6934  fveqressseq  6939  f0cli  6956  fmptco  6983  fvrnressn  7015  funfvima  7088  elunirnALT  7107  fliftel  7160  eloprabga  7360  eloprabgaOLD  7361  elrnmpo  7388  ovid  7392  offval  7520  suceloni  7635  1st2val  7832  2nd2val  7833  bropopvvv  7901  bropfvvvv  7903  fsplit  7928  fsplitOLD  7929  xporderlem  7939  brtpos2  8019  frrlem8  8080  frrlem9  8081  frrlem10  8082  fprresex  8097  wfrdmclOLD  8119  wfrfunOLD  8121  wfrlem12OLD  8122  wfrlem17OLD  8127  wfr2OLD  8130  issmo  8150  smores3  8155  tfrlem7  8185  tfrlem9  8187  tfrlem9a  8188  tfr2b  8198  tfr2  8200  rdgsuc  8226  frsucmptn  8240  tz7.48-2  8243  el1o  8291  dif1o  8292  ondif2  8294  oawordeulem  8347  elecg  8499  brecop  8557  erovlem  8560  eceqoveq  8569  mapsncnv  8639  mptelixpg  8681  brsdom  8718  isfi  8719  enssdom  8720  brdom2  8725  xpcomco  8802  brsdom2  8837  en3lplem2  9301  cnfcom2lem  9389  eltrpred  9404  epfrs  9420  r1limg  9460  r1ord  9469  r1ord3  9471  tz9.12lem3  9478  rankvaln  9488  r1elss  9495  rankpwi  9512  ssrankr1  9524  r1val3  9527  r1pw  9534  rankr1b  9553  djur  9608  djuunxp  9610  eldju2ndl  9613  eldju2ndr  9614  isnum2  9634  cardprclem  9668  infxpenlem  9700  alephcard  9757  alephnbtwn  9758  alephnbtwn2  9759  alephord2  9763  alephsdom  9773  dfac3  9808  dfac5lem2  9811  dfac5lem3  9812  dfac5lem5  9814  pwsdompw  9891  cfub  9936  cardcf  9939  cflecard  9940  cfle  9941  cflim2  9950  cofsmo  9956  cfidm  9962  isfin3  9983  isfin5  9986  isfin6  9987  sdom2en01  9989  fin23lem26  10012  fin23lem30  10029  isf32lem5  10044  itunitc1  10107  ituniiun  10109  axdc3lem3  10139  axcclem  10144  axdclem  10206  iunfo  10226  iundom2g  10227  cardidg  10235  konigthlem  10255  alephadd  10264  alephreg  10269  pwcfsdom  10270  cfpwsdom  10271  elgch  10309  fpwwe2lem11  10328  canth4  10334  wunex2  10425  r1tskina  10469  elni  10563  nlt1pi  10593  adderpq  10643  mulerpq  10644  recmulnq  10651  addsrpr  10762  mulsrpr  10763  opelcn  10816  opelreal  10817  elreal  10818  elreal2  10819  0ncn  10820  addcnsr  10822  mulcnsr  10823  xrlenlt  10971  elnn0  12165  elnnne0  12177  un0addcl  12196  un0mulcl  12197  elxnn0  12237  uztrn2  12530  elnnuz  12551  elnn0uz  12552  elq  12619  elxr  12781  elfzm1b  13263  elfz0lmr  13430  uzrdgfni  13606  fzennn  13616  ser0  13703  hash2pwpr  14118  iswrd  14147  pfxccatpfx1  14377  s3iunsndisj  14607  sumz  15362  sumss  15364  fsumcvg3  15369  abscvgcvg  15459  isumshft  15479  prodf1  15531  zprod  15575  prod1  15582  prodss  15585  prodsn  15600  prodsnf  15602  bpolydiflem  15692  bpoly2  15695  bpoly3  15696  bpoly4  15697  ruclem6  15872  divides  15893  dvdsflip  15954  pwp1fsum  16028  sadc0  16089  eulerthlem2  16411  prm23lt5  16443  4sqlem2  16578  4sqlem12  16585  vdwpc  16609  xpscf  17193  cidpropd  17336  oppcsect  17407  funcpropd  17532  natpropd  17610  dfinito2  17634  dftermo2  17635  initoeu2lem0  17644  arwhoma  17676  eldmcoa  17696  pospo  17978  psss  18213  ismgmn0  18243  gsumpropd2lem  18278  elefmndbas  18427  smndex1basss  18459  smndex1mgm  18461  pwmnd  18491  dfgrp2e  18520  mulgfval  18617  cycsubmel  18734  ghmeqker  18776  cntri  18852  oppgsubg  18885  fvcosymgeq  18952  symgfixels  18957  pmtrfrn  18981  efgsfo  19260  efgrelexlemb  19271  lt6abl  19411  dmdprd  19516  dprdval  19521  dprdw  19528  srgbinomlem4  19694  isnirred  19857  isrhm  19880  issrng  20025  lspexchn2  20308  lspindp2l  20311  lspindp2  20312  lbsextlem2  20336  cnfldfunALT  20523  dsmmelbas  20856  frlmbas3  20893  lindsind2  20936  islindf4  20955  psrbagf  21031  evlslem4  21194  ply1bascl2  21285  cply1mul  21375  lply1binom  21387  matsubgcell  21491  matinvgcell  21492  matvscacell  21493  matepmcl  21519  matepm2cl  21520  scmatscm  21570  smatvscl  21581  marrepcl  21621  marepvcl  21626  mulmarep1el  21629  mulmarep1gsum1  21630  mulmarep1gsum2  21631  submabas  21635  m1detdiag  21654  mdetdiag  21656  m2detleib  21688  gsummatr01lem3  21714  gsummatr01  21716  smadiadetlem4  21726  slesolinv  21737  slesolinvbi  21738  slesolex  21739  cramerimplem2  21741  pmatcoe1fsupp  21758  mat2pmatbas  21783  mat2pmatmul  21788  mat2pmatlin  21792  decpmatmul  21829  monmatcollpw  21836  pm2mpf1  21856  pm2mpghm  21873  istps  21991  mretopd  22151  neiptopuni  22189  lpdifsn  22202  restcls  22240  perfopn  22244  pnfnei  22279  mnfnei  22280  lmss  22357  hauscmplem  22465  is2ndc  22505  2ndcdisj  22515  hausnlly  22552  txuni2  22624  ptpjpre1  22630  elpt  22631  dfac14  22677  xkococn  22719  fbasrn  22943  fin1aufil  22991  elfm2  23007  elfm3  23009  fbflim  23035  flffbas  23054  cnpflf2  23059  fclsbas  23080  efmndtmd  23160  tsmssubm  23202  iscusp2  23362  imasdsf1olem  23434  metustel  23612  metuel2  23627  isnghm  23793  opnreen  23900  iccpnfcnv  24013  ehleudisval  24488  ehl1eudis  24489  ehl2eudis  24491  minveclem3b  24497  ovoliunlem1  24571  ioombl1lem4  24630  subopnmbl  24673  vitalilem2  24678  vitalilem3  24679  mbfimaopnlem  24724  mbfimaopn2  24726  itg2l  24799  dvply1  25349  vieta1lem1  25375  vieta1lem2  25376  elaa  25381  taylthlem2  25438  abelthlem6  25500  abelthlem9  25504  sinq34lt0t  25571  ellogrn  25620  dvrelog  25697  ellogdm  25699  logtayl2  25722  cxpcn3lem  25805  cxpcn3  25806  1cubr  25897  atandm  25931  atanf  25935  reasinsin  25951  atans2  25986  dmarea  26012  xrlimcnp  26023  amgmlem  26044  ppiublem1  26255  lgsdir2lem2  26379  gausslemma2dlem1a  26418  lgsquadlem1  26433  lgsquadlem2  26434  2sqlem1  26470  rpvmasum2  26565  edgiedgb  27327  isuhgr  27333  isushgr  27334  isupgr  27357  isumgr  27368  umgredg  27411  umgrpredgv  27413  umgredgne  27418  umgredgnlp  27420  isuspgr  27425  isusgr  27426  ausgrusgri  27441  usgredgppr  27466  edgssv2  27468  uspgredg2vlem  27493  uspgredg2v  27494  ushgredgedg  27499  ushgredgedgloop  27501  griedg0ssusgr  27535  uhgrissubgr  27545  subumgredg2  27555  uhgrspansubgrlem  27560  umgrres1lem  27580  upgrres1  27583  nbgrcl  27605  nbuhgr  27613  nbuhgr2vtx1edgblem  27621  nbupgrres  27634  edgnbusgreu  27637  nbusgredgeu0  27638  nbusgrf1o0  27639  hashnbusgrnn0  27646  nbupgruvtxres  27677  cffldtocusgr  27717  cusgrfilem2  27726  vtxdg0v  27743  vtxduhgr0nedg  27762  uhgrvd00  27804  vtxdginducedm1  27813  finsumvtxdg2ssteplem4  27818  wlk1walk  27908  wlkp1lem6  27948  iswwlks  28102  wwlknllvtx  28112  wwlksonvtx  28121  wspthnonp  28125  wlkiswwlksupgr2  28143  wwlksnwwlksnon  28181  2pthon3v  28209  umgr2wlk  28215  elwwlks2s3  28217  wwlks2onv  28219  elwwlks2ons3im  28220  isclwwlk  28249  clwwlkccatlem  28254  clwlkclwwlk  28267  wwlksext2clwwlk  28322  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknon1  28362  clwwlknon1nloop  28364  clwwlknon2x  28368  1pthon2v  28418  uhgr3cyclex  28447  isconngr  28454  isconngr1  28455  eucrctshift  28508  frgrnbnb  28558  frgrncvvdeqlem1  28564  frgrncvvdeqlem2  28565  frgrncvvdeqlem3  28566  frgrncvvdeqlem9  28572  fusgreghash2wspv  28600  extwwlkfab  28617  numclwwlk1lem2foa  28619  numclwwlk1lem2fo  28623  clwlknon2num  28633  numclwlk2lem2f1o  28644  numclwwlk5lem  28652  topnfbey  28734  isvclem  28840  isnvlem  28873  vsfval  28896  h2hlm  29243  hhcmpl  29463  hhcms  29466  elch0  29517  omlsilem  29665  h1de2ctlem  29818  elspansni  29821  nonbooli  29914  spansncvi  29915  adjeq  30198  cnlnssadj  30343  cnvbraval  30373  brabgaf  30849  elimampt  30874  2ndresdju  30887  fmptdF  30895  fmptcof2  30896  acunirnmpt  30898  acunirnmpt2  30899  ofpreima  30904  fcnvgreu  30912  fdifsuppconst  30925  1stpreima  30941  2ndpreima  30942  fz2ssnn0  31008  elxrge02  31108  psgnfzto1stlem  31269  cycpmgcl  31322  nsgqusf1olem2  31501  nsgqusf1olem3  31502  prmidl0  31528  submatres  31658  lmat22lem  31669  crefdf  31700  cmppcmp  31710  rspectopn  31719  prsdm  31766  prsrn  31767  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  pnfneige0  31803  qqhre  31870  rrhre  31871  esumnul  31916  esumcvgsum  31956  ldgenpisyslem1  32031  measvuni  32082  cntnevol  32096  dya2iocnrect  32148  sibf0  32201  oddpwdc  32221  eulerpartlemd  32233  eulerpartgbij  32239  eulerpartlemgh  32245  isrrvv  32310  coinfliprv  32349  ballotlem7  32402  signswch  32440  hashreprin  32500  chtvalz  32509  circlemethhgt  32523  hgt750lemb  32536  tgoldbachgt  32543  bnj23  32597  bnj158  32608  bnj168  32609  bnj1138  32668  bnj1143  32670  bnj1454  32722  bnj110  32738  bnj882  32806  bnj893  32808  bnj916  32813  bnj970  32827  bnj983  32831  bnj984  32832  bnj1137  32875  bnj1174  32883  bnj1388  32913  bnj1398  32914  loop1cycl  32999  subfacp1lem5  33046  satfv1  33225  satfrnmapom  33232  satf0op  33239  satf0n0  33240  fmlafvel  33247  fmlaomn0  33252  fmlan0  33253  satffunlem2lem2  33268  satfv0fvfmla0  33275  satefvfmla0  33280  mrsub0  33378  mrsubccat  33380  mrsubcn  33381  elmrsubrn  33382  msubco  33393  msubvrs  33422  elmthm  33438  mthmblem  33442  elrn3  33635  dfon2lem7  33671  brttrcl2  33700  ttrcltr  33702  rnttrcl  33708  frpoins3xpg  33714  frpoins3xp3g  33715  madeval2  33964  newval  33966  leftval  33974  rightval  33975  madess  33986  oldssmade  33987  lrold  34004  brsset  34118  eltrans  34120  elfix  34132  ellimits  34139  elfuns  34144  elsingles  34147  fvtransport  34261  brcolinear2  34287  fvray  34370  linedegen  34372  fvline  34373  ellines  34381  fwddifn0  34393  elhf  34403  hfninf  34415  fnessref  34473  bj-ififc  34690  bj-csbsnlem  35015  bj-elgab  35054  currysetlem1  35063  bj-eltag  35094  bj-sngltag  35100  bj-projun  35111  bj-0nelmpt  35214  bj-opelidres  35259  bj-inftyexpitaudisj  35303  bj-elccinfty  35312  f1omptsnlem  35434  icoreelrnab  35452  relowlpssretop  35462  rdgssun  35476  exrecfnlem  35477  finxpnom  35499  uncov  35685  tan2h  35696  ptrecube  35704  poimirlem25  35729  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  cnambfre  35752  ftc1cnnc  35776  sdclem2  35827  sdclem1  35828  fdc  35830  caushft  35846  issmgrpOLD  35948  ismndo  35957  isrngo  35982  isdivrngo  36035  csbcom2fi  36213  elecALTV  36332  brrabga  36403  eldmcoss  36503  coss0  36524  elrels2  36531  dath  37677  diclspsn  39135  dvh4dimlem  39384  dvh2dim  39386  dvh3dim3N  39390  lcfrvalsnN  39482  mapdh6eN  39681  mapdh7dN  39691  mapdh8b  39721  hdmap1l6e  39755  lcmfunnnd  39948  3factsumint1  39957  sticksstones2  40031  sticksstones3  40032  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  elab2gw  40094  frlmfielbas  40157  mhpind  40206  pellex  40573  rmspecnonsq  40645  islmodfg  40810  aaitgo  40903  areaquad  40963  elcnvcnvintab  41079  elnonrel  41082  elcnvcnvlem  41096  cnvcnvintabd  41097  brfvrcld2  41189  grur1cld  41739  dvgrat  41819  cvgdvgrat  41820  radcnvrat  41821  nznngen  41823  uzmptshftfval  41853  binomcxplemcvg  41861  binomcxplemnotnn0  41863  tpid3gVD  42351  en3lplem2VD  42353  rexanuz3  42535  eliuniin  42538  eliuniin2  42558  disjinfi  42620  fsneq  42635  iuneqfzuzlem  42763  allbutfi  42823  eluzelz2  42833  uz0  42842  uzublem  42860  uzid3  42865  elicores  42961  uzinico  42988  climsuselem1  43038  climsuse  43039  islptre  43050  fnlimfvre  43105  limsupresico  43131  limsupvaluz  43139  limsupubuzlem  43143  limsupequzmptlem  43159  liminfresico  43202  cnrefiisplem  43260  stoweidlem14  43445  stoweidlem39  43470  stoweidlem48  43479  stoweidlem51  43482  stoweidlem59  43490  stoweidlem62  43493  wallispilem3  43498  fourierdlem42  43580  fourierdlem62  43599  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  etransclem26  43691  rrxsnicc  43731  ioorrnopn  43736  ioorrnopnxr  43738  sge00  43804  sge0fodjrnlem  43844  sge0isum  43855  sge0seq  43874  meadjiunlem  43893  carageneld  43930  volicorescl  43981  hoidmv1lelem1  44019  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem3  44025  ovnhoilem2  44030  hoiqssbllem2  44051  opnvonmbllem2  44061  ovolval4lem1  44077  iinhoiicc  44102  vonioolem1  44108  smflimlem1  44193  smflimlem2  44194  smflim  44199  nsssmfmbf  44201  smfresal  44209  smfrec  44210  smfdiv  44218  smfpimbor1lem2  44220  smflim2  44226  smflimmpt  44230  smfinflem  44237  smfinfmpt  44239  smflimsuplem1  44240  smflimsuplem2  44241  smflimsuplem3  44242  smflimsuplem5  44244  smflimsuplem6  44245  smflimsup  44248  smflimsupmpt  44249  smfliminfmpt  44252  fcores  44448  ndmaovcl  44582  ndmaovcom  44584  ndmaovass  44585  ndmaovdistr  44586  dfatco  44635  otiunsndisjX  44658  fvmptrabdm  44672  elsetpreimafvb  44724  sprsymrelfolem2  44833  sprsymrelf  44835  sprsymrelf1  44836  prpair  44841  prproropf1olem0  44842  paireqne  44851  fmtno4prmfac  44912  dfodd5  45000  sbgoldbo  45127  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  isomushgr  45166  isomuspgrlem2c  45170  uspgrsprf  45196  uspgrsprf1  45197  uspgrsprfo  45198  opeliun2xp  45556  ply1sclrmsm  45612  lcoop  45640  lincfsuppcl  45642  linccl  45643  lincvalsng  45645  lincvalpr  45647  lincvalsc0  45650  linc0scn0  45652  lincdifsn  45653  linc1  45654  lincsum  45658  lincscm  45659  lspsslco  45666  snlindsntor  45700  lincresunit3lem2  45709  ldepsnlinclem1  45734  ldepsnlinclem2  45735  prelrrx2  45947  prelrrx2b  45948  rrx2xpref1o  45952  rrx2plord  45954  rrx2linesl  45977  oppcthin  46208  indthinc  46221  prsthinc  46223  elpglem3  46304