Theorem eleq2i 2831

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  eleq12i  2832  eleqtri  2838  eleq2s  2858  hbxfreq  2870  nfceqi  2905  raleqbii  3164  rexeqbii  3261  rabeqi  3417  rabeq2i  3423  rabrabi  3428  elab2g  3612  elrabf  3621  elrab3t  3624  elrab2  3628  cbvsbcw  3751  cbvsbcvw  3752  cbvsbc  3753  elin2  4132  elsymdif  4182  noel  4265  noelOLD  4266  eltpg  4622  elunirab  4856  elintrab  4892  disjxiun  5072  exss  5379  otiunsndisj  5435  brabsb  5445  brabga  5448  epelg  5497  pofun  5522  elxp  5613  opeliunxp  5655  bropaex12  5679  brab2a  5681  elcnv  5788  dmopabelb  5828  elrnmptg  5871  elres  5933  elrid  5956  rninxp  6087  elid  6107  elsuci  6336  elsucg  6337  elsuc2g  6338  elfv  6781  0fv  6822  opabiota  6860  dffv2  6872  fvopab3g  6879  fvmptex  6898  fvopab5  6916  fvn0ssdmfun  6961  fveqressseq  6966  f0cli  6983  fmptco  7010  fvrnressn  7042  funfvima  7115  elunirnALT  7134  fliftel  7189  eloprabga  7391  eloprabgaOLD  7392  elrnmpo  7419  ovid  7423  offval  7551  sucexeloni  7667  suceloniOLD  7669  1st2val  7868  2nd2val  7869  bropopvvv  7939  bropfvvvv  7941  fsplit  7966  fsplitOLD  7967  xporderlem  7977  brtpos2  8057  frrlem8  8118  frrlem9  8119  frrlem10  8120  fprresex  8135  wfrdmclOLD  8157  wfrfunOLD  8159  wfrlem12OLD  8160  wfrlem17OLD  8165  wfr2OLD  8168  issmo  8188  smores3  8193  tfrlem7  8223  tfrlem9  8225  tfrlem9a  8226  tfr2b  8236  tfr2  8238  rdgsuc  8264  frsucmptn  8279  tz7.48-2  8282  el1o  8334  ord2eln012  8336  dif1o  8339  ondif2  8341  oawordeulem  8394  elecg  8550  brecop  8608  erovlem  8611  eceqoveq  8620  mapsncnv  8690  mptelixpg  8732  brsdom  8772  isfi  8773  enssdom  8774  brdom2  8779  xpcomco  8858  brsdom2  8893  en3lplem2  9380  cnfcom2lem  9468  brttrcl2  9481  ttrcltr  9483  rnttrcl  9489  epfrs  9498  r1limg  9538  r1ord  9547  r1ord3  9549  tz9.12lem3  9556  rankvaln  9566  r1elss  9573  rankpwi  9590  ssrankr1  9602  r1val3  9605  r1pw  9612  rankr1b  9631  djur  9686  djuunxp  9688  eldju2ndl  9691  eldju2ndr  9692  isnum2  9712  cardprclem  9746  infxpenlem  9778  alephcard  9835  alephnbtwn  9836  alephnbtwn2  9837  alephord2  9841  alephsdom  9851  dfac3  9886  dfac5lem2  9889  dfac5lem3  9890  dfac5lem5  9892  pwsdompw  9969  cfub  10014  cardcf  10017  cflecard  10018  cfle  10019  cflim2  10028  cofsmo  10034  cfidm  10040  isfin3  10061  isfin5  10064  isfin6  10065  sdom2en01  10067  fin23lem26  10090  fin23lem30  10107  isf32lem5  10122  itunitc1  10185  ituniiun  10187  axdc3lem3  10217  axcclem  10222  axdclem  10284  iunfo  10304  iundom2g  10305  cardidg  10313  konigthlem  10333  alephadd  10342  alephreg  10347  pwcfsdom  10348  cfpwsdom  10349  elgch  10387  fpwwe2lem11  10406  canth4  10412  wunex2  10503  r1tskina  10547  elni  10641  nlt1pi  10671  adderpq  10721  mulerpq  10722  recmulnq  10729  addsrpr  10840  mulsrpr  10841  opelcn  10894  opelreal  10895  elreal  10896  elreal2  10897  0ncn  10898  addcnsr  10900  mulcnsr  10901  xrlenlt  11049  elnn0  12244  elnnne0  12256  un0addcl  12275  un0mulcl  12276  elxnn0  12316  uztrn2  12610  elnnuz  12631  elnn0uz  12632  elq  12699  elxr  12861  elfzm1b  13343  elfz0lmr  13511  uzrdgfni  13687  fzennn  13697  ser0  13784  hash2pwpr  14199  iswrd  14228  pfxccatpfx1  14458  s3iunsndisj  14688  sumz  15443  sumss  15445  fsumcvg3  15450  abscvgcvg  15540  isumshft  15560  prodf1  15612  zprod  15656  prod1  15663  prodss  15666  prodsn  15681  prodsnf  15683  bpolydiflem  15773  bpoly2  15776  bpoly3  15777  bpoly4  15778  ruclem6  15953  divides  15974  dvdsflip  16035  pwp1fsum  16109  sadc0  16170  eulerthlem2  16492  prm23lt5  16524  4sqlem2  16659  4sqlem12  16666  vdwpc  16690  xpscf  17285  cidpropd  17428  oppcsect  17499  funcpropd  17625  natpropd  17703  dfinito2  17727  dftermo2  17728  initoeu2lem0  17737  arwhoma  17769  eldmcoa  17789  pospo  18072  psss  18307  ismgmn0  18337  gsumpropd2lem  18372  elefmndbas  18521  smndex1basss  18553  smndex1mgm  18555  pwmnd  18585  dfgrp2e  18614  mulgfval  18711  cycsubmel  18828  ghmeqker  18870  cntri  18946  oppgsubg  18979  fvcosymgeq  19046  symgfixels  19051  pmtrfrn  19075  efgsfo  19354  efgrelexlemb  19365  lt6abl  19505  dmdprd  19610  dprdval  19615  dprdw  19622  srgbinomlem4  19788  isnirred  19951  isrhm  19974  issrng  20119  lspexchn2  20402  lspindp2l  20405  lspindp2  20406  lbsextlem2  20430  cnfldfun  20618  dsmmelbas  20955  frlmbas3  20992  lindsind2  21035  islindf4  21054  psrbagf  21130  evlslem4  21293  ply1bascl2  21384  cply1mul  21474  lply1binom  21486  matsubgcell  21592  matinvgcell  21593  matvscacell  21594  matepmcl  21620  matepm2cl  21621  scmatscm  21671  smatvscl  21682  marrepcl  21722  marepvcl  21727  mulmarep1el  21730  mulmarep1gsum1  21731  mulmarep1gsum2  21732  submabas  21736  m1detdiag  21755  mdetdiag  21757  m2detleib  21789  gsummatr01lem3  21815  gsummatr01  21817  smadiadetlem4  21827  slesolinv  21838  slesolinvbi  21839  slesolex  21840  cramerimplem2  21842  pmatcoe1fsupp  21859  mat2pmatbas  21884  mat2pmatmul  21889  mat2pmatlin  21893  decpmatmul  21930  monmatcollpw  21937  pm2mpf1  21957  pm2mpghm  21974  istps  22092  mretopd  22252  neiptopuni  22290  lpdifsn  22303  restcls  22341  perfopn  22345  pnfnei  22380  mnfnei  22381  lmss  22458  hauscmplem  22566  is2ndc  22606  2ndcdisj  22616  hausnlly  22653  txuni2  22725  ptpjpre1  22731  elpt  22732  dfac14  22778  xkococn  22820  fbasrn  23044  fin1aufil  23092  elfm2  23108  elfm3  23110  fbflim  23136  flffbas  23155  cnpflf2  23160  fclsbas  23181  efmndtmd  23261  tsmssubm  23303  iscusp2  23463  imasdsf1olem  23535  metustel  23715  metuel2  23730  isnghm  23896  opnreen  24003  iccpnfcnv  24116  ehleudisval  24592  ehl1eudis  24593  ehl2eudis  24595  minveclem3b  24601  ovoliunlem1  24675  ioombl1lem4  24734  subopnmbl  24777  vitalilem2  24782  vitalilem3  24783  mbfimaopnlem  24828  mbfimaopn2  24830  itg2l  24903  dvply1  25453  vieta1lem1  25479  vieta1lem2  25480  elaa  25485  taylthlem2  25542  abelthlem6  25604  abelthlem9  25608  sinq34lt0t  25675  ellogrn  25724  dvrelog  25801  ellogdm  25803  logtayl2  25826  cxpcn3lem  25909  cxpcn3  25910  1cubr  26001  atandm  26035  atanf  26039  reasinsin  26055  atans2  26090  dmarea  26116  xrlimcnp  26127  amgmlem  26148  ppiublem1  26359  lgsdir2lem2  26483  gausslemma2dlem1a  26522  lgsquadlem1  26537  lgsquadlem2  26538  2sqlem1  26574  rpvmasum2  26669  edgiedgb  27433  isuhgr  27439  isushgr  27440  isupgr  27463  isumgr  27474  umgredg  27517  umgrpredgv  27519  umgredgne  27524  umgredgnlp  27526  isuspgr  27531  isusgr  27532  ausgrusgri  27547  usgredgppr  27572  edgssv2  27574  uspgredg2vlem  27599  uspgredg2v  27600  ushgredgedg  27605  ushgredgedgloop  27607  griedg0ssusgr  27641  uhgrissubgr  27651  subumgredg2  27661  uhgrspansubgrlem  27666  umgrres1lem  27686  upgrres1  27689  nbgrcl  27711  nbuhgr  27719  nbuhgr2vtx1edgblem  27727  nbupgrres  27740  edgnbusgreu  27743  nbusgredgeu0  27744  nbusgrf1o0  27745  hashnbusgrnn0  27752  nbupgruvtxres  27783  cffldtocusgr  27823  cusgrfilem2  27832  vtxdg0v  27849  vtxduhgr0nedg  27868  uhgrvd00  27910  vtxdginducedm1  27919  finsumvtxdg2ssteplem4  27924  wlk1walk  28015  wlkp1lem6  28055  iswwlks  28210  wwlknllvtx  28220  wwlksonvtx  28229  wspthnonp  28233  wlkiswwlksupgr2  28251  wwlksnwwlksnon  28289  2pthon3v  28317  umgr2wlk  28323  elwwlks2s3  28325  wwlks2onv  28327  elwwlks2ons3im  28328  isclwwlk  28357  clwwlkccatlem  28362  clwlkclwwlk  28375  wwlksext2clwwlk  28430  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknon1  28470  clwwlknon1nloop  28472  clwwlknon2x  28476  1pthon2v  28526  uhgr3cyclex  28555  isconngr  28562  isconngr1  28563  eucrctshift  28616  frgrnbnb  28666  frgrncvvdeqlem1  28672  frgrncvvdeqlem2  28673  frgrncvvdeqlem3  28674  frgrncvvdeqlem9  28680  fusgreghash2wspv  28708  extwwlkfab  28725  numclwwlk1lem2foa  28727  numclwwlk1lem2fo  28731  clwlknon2num  28741  numclwlk2lem2f1o  28752  numclwwlk5lem  28760  topnfbey  28842  isvclem  28948  isnvlem  28981  vsfval  29004  h2hlm  29351  hhcmpl  29571  hhcms  29574  elch0  29625  omlsilem  29773  h1de2ctlem  29926  elspansni  29929  nonbooli  30022  spansncvi  30023  adjeq  30306  cnlnssadj  30451  cnvbraval  30481  brabgaf  30957  elimampt  30982  2ndresdju  30995  fmptdF  31002  fmptcof2  31003  acunirnmpt  31005  acunirnmpt2  31006  ofpreima  31011  fcnvgreu  31019  fdifsuppconst  31032  1stpreima  31048  2ndpreima  31049  fz2ssnn0  31115  elxrge02  31215  psgnfzto1stlem  31376  cycpmgcl  31429  nsgqusf1olem2  31608  nsgqusf1olem3  31609  prmidl0  31635  submatres  31765  lmat22lem  31776  crefdf  31807  cmppcmp  31817  rspectopn  31826  prsdm  31873  prsrn  31874  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  pnfneige0  31910  qqhre  31979  rrhre  31980  esumnul  32025  esumcvgsum  32065  ldgenpisyslem1  32140  measvuni  32191  cntnevol  32205  dya2iocnrect  32257  sibf0  32310  oddpwdc  32330  eulerpartlemd  32342  eulerpartgbij  32348  eulerpartlemgh  32354  isrrvv  32419  coinfliprv  32458  ballotlem7  32511  signswch  32549  hashreprin  32609  chtvalz  32618  circlemethhgt  32632  hgt750lemb  32645  tgoldbachgt  32652  bnj23  32706  bnj158  32717  bnj168  32718  bnj1138  32777  bnj1143  32779  bnj1454  32831  bnj110  32847  bnj882  32915  bnj893  32917  bnj916  32922  bnj970  32936  bnj983  32940  bnj984  32941  bnj1137  32984  bnj1174  32992  bnj1388  33022  bnj1398  33023  loop1cycl  33108  subfacp1lem5  33155  satfv1  33334  satfrnmapom  33341  satf0op  33348  satf0n0  33349  fmlafvel  33356  fmlaomn0  33361  fmlan0  33362  satffunlem2lem2  33377  satfv0fvfmla0  33384  satefvfmla0  33389  mrsub0  33487  mrsubccat  33489  mrsubcn  33490  elmrsubrn  33491  msubco  33502  msubvrs  33531  elmthm  33547  mthmblem  33551  elrn3  33738  dfon2lem7  33774  frpoins3xpg  33796  frpoins3xp3g  33797  madeval2  34046  newval  34048  leftval  34056  rightval  34057  madess  34068  oldssmade  34069  lrold  34086  brsset  34200  eltrans  34202  elfix  34214  ellimits  34221  elfuns  34226  elsingles  34229  fvtransport  34343  brcolinear2  34369  fvray  34452  linedegen  34454  fvline  34455  ellines  34463  fwddifn0  34475  elhf  34485  hfninf  34497  fnessref  34555  bj-ififc  34772  bj-csbsnlem  35097  bj-elgab  35136  currysetlem1  35145  bj-eltag  35176  bj-sngltag  35182  bj-projun  35193  bj-0nelmpt  35296  bj-opelidres  35341  bj-inftyexpitaudisj  35385  bj-elccinfty  35394  f1omptsnlem  35516  icoreelrnab  35534  relowlpssretop  35544  rdgssun  35558  exrecfnlem  35559  finxpnom  35581  uncov  35767  tan2h  35778  ptrecube  35786  poimirlem25  35811  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  cnambfre  35834  ftc1cnnc  35858  sdclem2  35909  sdclem1  35910  fdc  35912  caushft  35928  issmgrpOLD  36030  ismndo  36039  isrngo  36064  isdivrngo  36117  csbcom2fi  36295  elecALTV  36413  brrabga  36483  eldmcoss  36583  coss0  36604  elrels2  36611  dath  37757  diclspsn  39215  dvh4dimlem  39464  dvh2dim  39466  dvh3dim3N  39470  lcfrvalsnN  39562  mapdh6eN  39761  mapdh7dN  39771  mapdh8b  39801  hdmap1l6e  39835  lcmfunnnd  40027  3factsumint1  40036  sticksstones2  40110  sticksstones3  40111  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  elab2gw  40173  frlmfielbas  40238  mhpind  40290  prjcrv0  40477  pellex  40664  rmspecnonsq  40736  islmodfg  40901  aaitgo  40994  areaquad  41054  finona1cl  41067  elcnvcnvintab  41197  elnonrel  41200  elcnvcnvlem  41214  cnvcnvintabd  41215  brfvrcld2  41307  grur1cld  41857  dvgrat  41937  cvgdvgrat  41938  radcnvrat  41939  nznngen  41941  uzmptshftfval  41971  binomcxplemcvg  41979  binomcxplemnotnn0  41981  tpid3gVD  42469  en3lplem2VD  42471  rexanuz3  42653  eliuniin  42656  eliuniin2  42676  disjinfi  42738  fsneq  42753  iuneqfzuzlem  42880  allbutfi  42940  eluzelz2  42950  uz0  42959  uzublem  42977  uzid3  42982  elicores  43078  uzinico  43105  climsuselem1  43155  climsuse  43156  islptre  43167  fnlimfvre  43222  limsupresico  43248  limsupvaluz  43256  limsupubuzlem  43260  limsupequzmptlem  43276  liminfresico  43319  cnrefiisplem  43377  stoweidlem14  43562  stoweidlem39  43587  stoweidlem48  43596  stoweidlem51  43599  stoweidlem59  43607  stoweidlem62  43610  wallispilem3  43615  fourierdlem42  43697  fourierdlem62  43716  fourierdlem80  43734  fourierdlem103  43757  fourierdlem104  43758  etransclem26  43808  rrxsnicc  43848  ioorrnopn  43853  ioorrnopnxr  43855  sge00  43921  sge0fodjrnlem  43961  sge0isum  43972  sge0seq  43991  meadjiunlem  44010  carageneld  44047  volicorescl  44098  hoidmv1lelem1  44136  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem3  44142  ovnhoilem2  44147  hoiqssbllem2  44168  opnvonmbllem2  44178  ovolval4lem1  44194  iinhoiicc  44219  vonioolem1  44225  smflimlem1  44316  smflimlem2  44317  smflim  44322  nsssmfmbf  44324  smfresal  44333  smfrec  44334  smfdiv  44342  smfpimbor1lem2  44344  smflim2  44350  smflimmpt  44354  smfinflem  44361  smfinfmpt  44363  smflimsuplem1  44364  smflimsuplem2  44365  smflimsuplem3  44366  smflimsuplem5  44368  smflimsuplem6  44369  smflimsup  44372  smflimsupmpt  44373  smfliminfmpt  44376  fcores  44572  ndmaovcl  44706  ndmaovcom  44708  ndmaovass  44709  ndmaovdistr  44710  dfatco  44759  otiunsndisjX  44782  fvmptrabdm  44796  elsetpreimafvb  44847  sprsymrelfolem2  44956  sprsymrelf  44958  sprsymrelf1  44959  prpair  44964  prproropf1olem0  44965  paireqne  44974  fmtno4prmfac  45035  dfodd5  45123  sbgoldbo  45250  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  isomushgr  45289  isomuspgrlem2c  45293  uspgrsprf  45319  uspgrsprf1  45320  uspgrsprfo  45321  opeliun2xp  45679  ply1sclrmsm  45735  lcoop  45763  lincfsuppcl  45765  linccl  45766  lincvalsng  45768  lincvalpr  45770  lincvalsc0  45773  linc0scn0  45775  lincdifsn  45776  linc1  45777  lincsum  45781  lincscm  45782  lspsslco  45789  snlindsntor  45823  lincresunit3lem2  45832  ldepsnlinclem1  45857  ldepsnlinclem2  45858  prelrrx2  46070  prelrrx2b  46071  rrx2xpref1o  46075  rrx2plord  46077  rrx2linesl  46100  oppcthin  46331  indthinc  46344  prsthinc  46346  elpglem3  46429