Theorem eleq2i 2836

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleq12i  2837  eleqtri  2842  eleq2s  2862  hbxfreq  2875  nfceqi  2905  raleqbii  3352  rexeqbii  3353  rabeqi  3457  rabrabi  3463  reqabi  3467  elab2gw  3693  elab2g  3696  elrabf  3704  elrab3t  3707  elrab2  3711  cbvsbcw  3838  cbvsbcvw  3839  cbvsbc  3840  elin2  4226  elsymdif  4277  noel  4360  noelOLD  4361  eltpg  4709  elunirab  4946  elintrab  4984  disjxiun  5163  exss  5483  otiunsndisj  5539  brabsb  5550  brabga  5553  epelg  5600  pofun  5626  elxp  5723  opeliunxp  5767  bropaex12  5791  brab2a  5793  elcnv  5901  dmopabelb  5941  elrnmptg  5984  elres  6049  elimampt  6072  elrid  6075  rninxp  6210  elid  6230  elsuci  6462  elsucg  6463  elsuc2g  6464  elfv  6918  0fv  6964  opabiota  7004  dffv2  7017  fvopab3g  7024  fvmptex  7043  fvopab5  7062  fvn0ssdmfun  7108  fveqressseq  7113  f0cli  7132  fmptco  7163  fvrnressn  7195  funfvima  7267  elunirnALT  7289  fliftel  7345  eloprabga  7558  eloprabgaOLD  7559  elrnmpo  7586  elimampo  7587  ovid  7591  offval  7723  sucexeloniOLD  7846  suceloniOLD  7848  1st2val  8058  2nd2val  8059  bropopvvv  8131  bropfvvvv  8133  fsplit  8158  xporderlem  8168  frpoins3xpg  8181  frpoins3xp3g  8182  brtpos2  8273  frrlem8  8334  frrlem9  8335  frrlem10  8336  fprresex  8351  wfrdmclOLD  8373  wfrfunOLD  8375  wfrlem12OLD  8376  wfrlem17OLD  8381  wfr2OLD  8384  issmo  8404  smores3  8409  tfrlem7  8439  tfrlem9  8441  tfrlem9a  8442  tfr2b  8452  tfr2  8454  rdgsuc  8480  frsucmptn  8495  tz7.48-2  8498  el1o  8551  ord2eln012  8553  dif1o  8556  ondif2  8558  oawordeulem  8610  elecg  8807  brecop  8868  erovlem  8871  eceqoveq  8880  mapsncnv  8951  mptelixpg  8993  brsdom  9035  isfi  9036  enssdom  9037  brdom2  9042  xpcomco  9128  brsdom2  9163  en3lplem2  9682  cnfcom2lem  9770  brttrcl2  9783  ttrcltr  9785  rnttrcl  9791  epfrs  9800  r1limg  9840  r1ord  9849  r1ord3  9851  tz9.12lem3  9858  rankvaln  9868  r1elss  9875  rankpwi  9892  ssrankr1  9904  r1val3  9907  r1pw  9914  rankr1b  9933  djur  9988  djuunxp  9990  eldju2ndl  9993  eldju2ndr  9994  isnum2  10014  cardprclem  10048  infxpenlem  10082  alephcard  10139  alephnbtwn  10140  alephnbtwn2  10141  alephord2  10145  alephsdom  10155  dfac3  10190  dfac5lem2  10193  dfac5lem3  10194  dfac5lem5  10196  pwsdompw  10272  cfub  10318  cardcf  10321  cflecard  10322  cfle  10323  cflim2  10332  cofsmo  10338  cfidm  10344  isfin3  10365  isfin5  10368  isfin6  10369  sdom2en01  10371  fin23lem26  10394  fin23lem30  10411  isf32lem5  10426  itunitc1  10489  ituniiun  10491  axdc3lem3  10521  axcclem  10526  axdclem  10588  iunfo  10608  iundom2g  10609  cardidg  10617  konigthlem  10637  alephadd  10646  alephreg  10651  pwcfsdom  10652  cfpwsdom  10653  elgch  10691  fpwwe2lem11  10710  canth4  10716  wunex2  10807  r1tskina  10851  elni  10945  nlt1pi  10975  adderpq  11025  mulerpq  11026  recmulnq  11033  addsrpr  11144  mulsrpr  11145  opelcn  11198  opelreal  11199  elreal  11200  elreal2  11201  0ncn  11202  addcnsr  11204  mulcnsr  11205  xrlenlt  11355  elnn0  12555  elnnne0  12567  un0addcl  12586  un0mulcl  12587  elxnn0  12627  uztrn2  12922  elnnuz  12947  elnn0uz  12948  elq  13015  elxr  13179  elfzm1b  13662  elfz0lmr  13832  uzrdgfni  14009  fzennn  14019  ser0  14105  hash2pwpr  14525  iswrd  14564  pfxccatpfx1  14784  s3iunsndisj  15017  sumz  15770  sumss  15772  fsumcvg3  15777  abscvgcvg  15867  isumshft  15887  prodf1  15939  prodeq1i  15964  zprod  15985  prod1  15992  prodss  15995  prodsn  16010  prodsnf  16012  bpolydiflem  16102  bpoly2  16105  bpoly3  16106  bpoly4  16107  ruclem6  16283  divides  16304  dvdsflip  16365  pwp1fsum  16439  sadc0  16500  eulerthlem2  16829  prm23lt5  16861  4sqlem2  16996  4sqlem12  17003  vdwpc  17027  xpscf  17625  cidpropd  17768  oppcsect  17839  funcpropd  17967  natpropd  18046  dfinito2  18070  dftermo2  18071  initoeu2lem0  18080  arwhoma  18112  eldmcoa  18132  pospo  18415  psss  18650  ismgmn0  18680  gsumpropd2lem  18717  elefmndbas  18908  smndex1basss  18940  smndex1mgm  18942  pwmnd  18972  dfgrp2e  19003  mulgfval  19109  eqg0subg  19236  cycsubmel  19240  ghmeqker  19283  elcntr  19370  cntri  19372  cntzsgrpcl  19374  oppgsubg  19406  fvcosymgeq  19471  symgfixels  19476  pmtrfrn  19500  efgsfo  19781  efgrelexlemb  19792  lt6abl  19937  dmdprd  20042  dprdval  20047  dprdw  20054  srgbinomlem4  20256  isnirred  20446  isrhm  20504  issrng  20867  lspexchn2  21156  lspindp2l  21159  lspindp2  21160  lbsextlem2  21184  rnglidl1  21265  df2idl2  21290  2idlss  21295  rngqiprngimfo  21334  cnfldfun  21401  cnfldfunOLD  21414  pzriprnglem3  21517  pzriprnglem4  21518  pzriprnglem7  21521  pzriprnglem8  21522  pzriprnglem9  21523  pzriprnglem12  21526  pzriprnglem14  21528  dsmmelbas  21782  frlmbas3  21819  lindsind2  21862  islindf4  21881  psrbagf  21961  evlslem4  22123  psdmul  22193  ply1bascl2  22227  cply1mul  22321  lply1binom  22335  matsubgcell  22461  matinvgcell  22462  matvscacell  22463  matepmcl  22489  matepm2cl  22490  scmatscm  22540  smatvscl  22551  marrepcl  22591  marepvcl  22596  mulmarep1el  22599  mulmarep1gsum1  22600  mulmarep1gsum2  22601  submabas  22605  m1detdiag  22624  mdetdiag  22626  m2detleib  22658  gsummatr01lem3  22684  gsummatr01  22686  smadiadetlem4  22696  slesolinv  22707  slesolinvbi  22708  slesolex  22709  cramerimplem2  22711  pmatcoe1fsupp  22728  mat2pmatbas  22753  mat2pmatmul  22758  mat2pmatlin  22762  decpmatmul  22799  monmatcollpw  22806  pm2mpf1  22826  pm2mpghm  22843  istps  22961  mretopd  23121  neiptopuni  23159  lpdifsn  23172  restcls  23210  perfopn  23214  pnfnei  23249  mnfnei  23250  lmss  23327  hauscmplem  23435  is2ndc  23475  2ndcdisj  23485  hausnlly  23522  txuni2  23594  ptpjpre1  23600  elpt  23601  dfac14  23647  xkococn  23689  fbasrn  23913  fin1aufil  23961  elfm2  23977  elfm3  23979  fbflim  24005  flffbas  24024  cnpflf2  24029  fclsbas  24050  efmndtmd  24130  tsmssubm  24172  iscusp2  24332  imasdsf1olem  24404  metustel  24584  metuel2  24599  isnghm  24765  opnreen  24872  iccpnfcnv  24994  ehleudisval  25472  ehl1eudis  25473  ehl2eudis  25475  minveclem3b  25481  ovoliunlem1  25556  ioombl1lem4  25615  subopnmbl  25658  vitalilem2  25663  vitalilem3  25664  mbfimaopnlem  25709  mbfimaopn2  25711  itg2l  25784  dvply1  26343  vieta1lem1  26370  vieta1lem2  26371  elaa  26376  taylthlem2  26434  taylthlem2OLD  26435  abelthlem6  26498  abelthlem9  26502  sinq34lt0t  26569  ellogrn  26619  dvrelog  26697  ellogdm  26699  logtayl2  26722  cxpcn3lem  26808  cxpcn3  26809  1cubr  26903  atandm  26937  atanf  26941  reasinsin  26957  atans2  26992  dmarea  27018  xrlimcnp  27029  amgmlem  27051  ppiublem1  27264  lgsdir2lem2  27388  gausslemma2dlem1a  27427  lgsquadlem1  27442  lgsquadlem2  27443  2sqlem1  27479  rpvmasum2  27574  madeval2  27910  newval  27912  leftval  27920  rightval  27921  lltropt  27929  madess  27933  oldssmade  27934  lrold  27953  addsproplem2  28021  addsproplem4  28023  addsproplem6  28025  negsproplem4  28081  negsproplem6  28083  precsexlem10  28258  precsexlem11  28259  sltonold  28301  elnns  28361  elzs  28388  edgiedgb  29089  isuhgr  29095  isushgr  29096  isupgr  29119  isumgr  29130  umgredg  29173  umgrpredgv  29175  umgredgne  29180  umgredgnlp  29182  isuspgr  29187  isusgr  29188  ausgrusgri  29203  usgredgppr  29231  edgssv2  29233  uspgredg2vlem  29258  uspgredg2v  29259  ushgredgedg  29264  ushgredgedgloop  29266  griedg0ssusgr  29300  uhgrissubgr  29310  subumgredg2  29320  uhgrspansubgrlem  29325  umgrres1lem  29345  upgrres1  29348  nbgrcl  29370  nbuhgr  29378  nbuhgr2vtx1edgblem  29386  nbupgrres  29399  edgnbusgreu  29402  nbusgredgeu0  29403  nbusgrf1o0  29404  hashnbusgrnn0  29411  nbupgruvtxres  29442  cffldtocusgr  29482  cffldtocusgrOLD  29483  cusgrfilem2  29492  vtxdg0v  29509  vtxduhgr0nedg  29528  uhgrvd00  29570  vtxdginducedm1  29579  finsumvtxdg2ssteplem4  29584  wlk1walk  29675  wlkp1lem6  29714  iswwlks  29869  wwlknllvtx  29879  wwlksonvtx  29888  wspthnonp  29892  wlkiswwlksupgr2  29910  wwlksnwwlksnon  29948  2pthon3v  29976  umgr2wlk  29982  elwwlks2s3  29984  wwlks2onv  29986  elwwlks2ons3im  29987  isclwwlk  30016  clwwlkccatlem  30021  clwlkclwwlk  30034  wwlksext2clwwlk  30089  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknon1  30129  clwwlknon1nloop  30131  clwwlknon2x  30135  1pthon2v  30185  uhgr3cyclex  30214  isconngr  30221  isconngr1  30222  eucrctshift  30275  frgrnbnb  30325  frgrncvvdeqlem1  30331  frgrncvvdeqlem2  30332  frgrncvvdeqlem3  30333  frgrncvvdeqlem9  30339  fusgreghash2wspv  30367  extwwlkfab  30384  numclwwlk1lem2foa  30386  numclwwlk1lem2fo  30390  clwlknon2num  30400  numclwlk2lem2f1o  30411  numclwwlk5lem  30419  topnfbey  30501  isvclem  30609  isnvlem  30642  vsfval  30665  h2hlm  31012  hhcmpl  31232  hhcms  31235  elch0  31286  omlsilem  31434  h1de2ctlem  31587  elspansni  31590  nonbooli  31683  spansncvi  31684  adjeq  31967  cnlnssadj  32112  cnvbraval  32142  brabgaf  32630  2ndresdju  32667  fmptdF  32674  fmptcof2  32675  acunirnmpt  32677  acunirnmpt2  32678  ofpreima  32683  fcnvgreu  32691  fdifsuppconst  32701  1stpreima  32718  2ndpreima  32719  fz2ssnn0  32790  elxrge02  32896  ccatws1f1o  32918  psgnfzto1stlem  33093  cycpmgcl  33146  nsgqusf1olem2  33407  nsgqusf1olem3  33408  prmidl0  33443  crngmxidl  33462  opprnsg  33477  rprmirredb  33525  zringfrac  33547  evl1deg2  33567  evl1deg3  33568  ply1degltel  33580  ply1degleel  33581  constrsuc  33728  constrconj  33735  submatres  33752  lmat22lem  33763  crefdf  33794  cmppcmp  33804  rspectopn  33813  prsdm  33860  prsrn  33861  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  pnfneige0  33897  qqhre  33966  rrhre  33967  esumnul  34012  esumcvgsum  34052  ldgenpisyslem1  34127  measvuni  34178  cntnevol  34192  dya2iocnrect  34246  sibf0  34299  oddpwdc  34319  eulerpartlemd  34331  eulerpartgbij  34337  eulerpartlemgh  34343  isrrvv  34408  coinfliprv  34447  ballotlem7  34500  signswch  34538  hashreprin  34597  chtvalz  34606  circlemethhgt  34620  hgt750lemb  34633  tgoldbachgt  34640  bnj23  34694  bnj158  34705  bnj168  34706  bnj1138  34764  bnj1143  34766  bnj1454  34818  bnj110  34834  bnj882  34902  bnj893  34904  bnj916  34909  bnj970  34923  bnj983  34927  bnj984  34928  bnj1137  34971  bnj1174  34979  bnj1388  35009  bnj1398  35010  loop1cycl  35105  subfacp1lem5  35152  satfv1  35331  satfrnmapom  35338  satf0op  35345  satf0n0  35346  fmlafvel  35353  fmlaomn0  35358  fmlan0  35359  satffunlem2lem2  35374  satfv0fvfmla0  35381  satefvfmla0  35386  mrsub0  35484  mrsubccat  35486  mrsubcn  35487  elmrsubrn  35488  msubco  35499  msubvrs  35528  elmthm  35544  mthmblem  35548  ellcsrspsn  35609  elrn3  35724  dfon2lem7  35753  brsset  35853  eltrans  35855  elfix  35867  ellimits  35874  elfuns  35879  elsingles  35882  fvtransport  35996  brcolinear2  36022  fvray  36105  linedegen  36107  fvline  36108  ellines  36116  fwddifn0  36128  elhf  36138  hfninf  36150  rmoeqi  36151  rmoeqbii  36152  reueqi  36153  reueqbii  36154  rabeqbii  36158  iuneq12i  36159  iineq1i  36160  iineq12i  36161  riotaeqbii  36162  ixpeq1i  36164  itgeq12i  36170  cbvprodvw2  36213  fnessref  36323  bj-ififc  36548  bj-csbsnlem  36869  bj-elgab  36905  currysetlem1  36913  bj-eltag  36943  bj-sngltag  36949  bj-projun  36960  bj-velpwALT  37019  bj-0nelmpt  37082  bj-opelidres  37127  bj-inftyexpitaudisj  37171  bj-elccinfty  37180  f1omptsnlem  37302  icoreelrnab  37320  relowlpssretop  37330  rdgssun  37344  exrecfnlem  37345  finxpnom  37367  uncov  37561  tan2h  37572  ptrecube  37580  poimirlem25  37605  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  cnambfre  37628  ftc1cnnc  37652  sdclem2  37702  sdclem1  37703  fdc  37705  caushft  37721  issmgrpOLD  37823  ismndo  37832  isrngo  37857  isdivrngo  37910  csbcom2fi  38088  elecALTV  38222  brrabga  38297  eldmcoss  38414  coss0  38435  elrels2  38442  dath  39693  diclspsn  41151  dvh4dimlem  41400  dvh2dim  41402  dvh3dim3N  41406  lcfrvalsnN  41498  mapdh6eN  41697  mapdh7dN  41707  mapdh8b  41737  hdmap1l6e  41771  lcmfunnnd  41969  3factsumint1  41978  primrootsunit1  42054  primrootscoprmpow  42056  aks6d1c2lem4  42084  sticksstones2  42104  sticksstones3  42105  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem2  42128  aks6d1c6lem3  42129  frlmfielbas  42455  mhpind  42549  pellex  42791  rmspecnonsq  42863  islmodfg  43026  aaitgo  43119  areaquad  43177  ordeldif1o  43222  naddwordnexlem4  43363  fpwfvss  43374  finona1cl  43415  elcnvcnvintab  43544  elnonrel  43547  elcnvcnvlem  43561  cnvcnvintabd  43562  brfvrcld2  43654  grur1cld  44201  dvgrat  44281  cvgdvgrat  44282  radcnvrat  44283  nznngen  44285  uzmptshftfval  44315  binomcxplemcvg  44323  binomcxplemnotnn0  44325  tpid3gVD  44813  en3lplem2VD  44815  iuneq1i  44987  rexanuz3  44998  eliuniin  45001  eliuniin2  45022  disjinfi  45099  fsneq  45113  iuneqfzuzlem  45249  allbutfi  45308  eluzelz2  45318  uz0  45327  uzublem  45345  uzid3  45350  elicores  45451  uzinico  45478  climsuselem1  45528  climsuse  45529  islptre  45540  fnlimfvre  45595  limsupresico  45621  limsupvaluz  45629  limsupubuzlem  45633  limsupequzmptlem  45649  liminfresico  45692  cnrefiisplem  45750  stoweidlem14  45935  stoweidlem39  45960  stoweidlem48  45969  stoweidlem51  45972  stoweidlem59  45980  stoweidlem62  45983  wallispilem3  45988  fourierdlem42  46070  fourierdlem62  46089  fourierdlem80  46107  fourierdlem103  46130  fourierdlem104  46131  etransclem26  46181  rrxsnicc  46221  ioorrnopn  46226  ioorrnopnxr  46228  sge00  46297  sge0fodjrnlem  46337  sge0isum  46348  sge0seq  46367  meadjiunlem  46386  carageneld  46423  volicorescl  46474  hoidmv1lelem1  46512  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem3  46518  ovnhoilem2  46523  hoiqssbllem2  46544  opnvonmbllem2  46554  ovolval4lem1  46570  iinhoiicc  46595  vonioolem1  46601  smflimlem1  46692  smflimlem2  46693  smflim  46698  nsssmfmbf  46700  smfresal  46709  smfrec  46710  smfdiv  46718  smfpimbor1lem2  46720  smflim2  46727  smflimmpt  46731  smfinflem  46738  smfinfmpt  46740  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem3  46743  smflimsuplem5  46745  smflimsuplem6  46746  smflimsup  46749  smflimsupmpt  46750  smfliminfmpt  46753  fcores  46982  ndmaovcl  47118  ndmaovcom  47120  ndmaovass  47121  ndmaovdistr  47122  dfatco  47171  otiunsndisjX  47194  fvmptrabdm  47208  elsetpreimafvb  47258  sprsymrelfolem2  47367  sprsymrelf  47369  sprsymrelf1  47370  prpair  47375  prproropf1olem0  47376  paireqne  47385  fmtno4prmfac  47446  dfodd5  47534  sbgoldbo  47661  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  clnbgrcl  47695  clnbgredg  47712  sclnbgrel  47719  isuspgrim0  47756  isuspgrimlem  47758  gricushgr  47770  clnbgrgrimlem  47785  grimedg  47787  usgrgrtrirex  47799  uspgrlimlem2  47813  uspgrlimlem3  47814  grlimgrtrilem1  47818  grlimgrtrilem2  47819  usgrexmpl2trifr  47852  uspgrsprf  47869  uspgrsprf1  47870  uspgrsprfo  47871  opeliun2xp  48057  ply1sclrmsm  48112  lcoop  48140  lincfsuppcl  48142  linccl  48143  lincvalsng  48145  lincvalpr  48147  lincvalsc0  48150  linc0scn0  48152  lincdifsn  48153  linc1  48154  lincsum  48158  lincscm  48159  lspsslco  48166  snlindsntor  48200  lincresunit3lem2  48209  ldepsnlinclem1  48234  ldepsnlinclem2  48235  prelrrx2  48447  prelrrx2b  48448  rrx2xpref1o  48452  rrx2plord  48454  rrx2linesl  48477  oppcthin  48706  indthinc  48719  prsthinc  48721  elpglem3  48805