Theorem eleq2i 2852

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  eleq12i  2853  eleqtri  2858  eleq2s  2878  hbxfreq  2890  nfceqi  2919  raleqbii  3332  rexeqbii  3333  rabeqi  3425  rabrabi  3430  reqabi  3434  elab2gw  3632  elab2g  3634  elrabf  3642  elrab3t  3644  elrab2  3649  cbvsbcw  3772  cbvsbcvw  3773  cbvsbc  3774  elin2  4149  elsymdif  4204  noel  4284  eltpg  4647  elunirab  4882  elintrab  4920  disjxiun  5100  exss  5438  otiunsndisj  5497  brabsb  5509  brabga  5512  epelg  5556  pofun  5581  elxp  5678  opeliunxp  5722  opeliun2xp  5723  bropaex12  5746  brab2a  5748  elcnv  5856  cnv0  5863  dmopabelb  5900  elrnmptg  5945  elres  6013  elimampt  6039  elrid  6042  rninxp  6172  elid  6193  elsuci  6427  elsucg  6428  elsuc2g  6429  elfv  6877  0fv  6920  opabiota  6961  dffv2  6974  fvopab3g  6982  fvmptex  7002  fvopab5  7021  fsneq  7028  fvn0ssdmfun  7068  fveqressseq  7073  f0cli  7092  fmptco  7124  fvrnressn  7159  fvtp0  7200  funfvima  7230  elunirnALT  7250  fliftel  7311  eloprabga  7523  elrnmpo  7550  elimampo  7551  ovid  7555  offval  7688  1st2val  8015  2nd2val  8016  bropopvvv  8088  bropfvvvv  8090  fsplit  8115  xporderlem  8126  frpoins3xpg  8139  frpoins3xp3g  8140  brtpos2  8231  frrlem8  8293  frrlem9  8294  frrlem10  8295  fprresex  8310  issmo  8338  smores3  8343  tfrlem7  8373  tfrlem9  8375  tfrlem9a  8376  tfr2b  8386  tfr2  8388  rdgsuc  8414  frsucmptn  8429  tz7.48-2  8434  el1o  8485  ord2eln012  8487  dif1o  8490  ondif2  8492  oawordeulem  8544  elecg  8744  brecop  8813  erovlem  8816  eceqoveq  8825  uncov  8875  mapsncnv  8903  mptelixpg  8945  brsdom  8983  isfi  8984  enssdomOLD  8986  brdom2  8991  xpcomco  9068  brsdom2  9102  en3lplem2  9595  cnfcom2lem  9683  brttrcl2  9696  ttrcltr  9698  rnttrcl  9704  epfrs  9713  r1limg  9756  r1ord  9765  r1ord3  9767  tz9.12lem3  9774  rankvaln  9784  r1elss  9791  rankpwi  9808  ssrankr1  9820  r1val3  9823  r1pw  9830  rankr1b  9849  djur  9927  djuunxp  9929  eldju2ndl  9932  eldju2ndr  9933  isnum2  9953  cardprclem  9987  infxpenlem  10019  alephcard  10076  alephnbtwn  10077  alephnbtwn2  10078  alephord2  10082  alephsdom  10092  dfac3  10127  dfac5lem2  10130  dfac5lem3  10131  dfac5lem5  10133  pwsdompw  10208  cfub  10253  cardcf  10256  cflecard  10257  cfle  10258  cflim2  10268  cofsmo  10274  cfidm  10280  isfin3  10301  isfin5  10304  isfin6  10305  sdom2en01  10307  fin23lem26  10330  fin23lem30  10347  isf32lem5  10362  itunitc1  10425  ituniiun  10427  axdc3lem3  10457  axcclem  10462  axdclem  10524  iunfo  10550  iundom2g  10551  cardidg  10559  konigthlem  10580  alephadd  10589  alephreg  10594  pwcfsdom  10595  cfpwsdom  10596  elgch  10634  fpwwe2lem11  10653  canth4  10659  wunex2  10750  r1tskina  10794  elni  10888  nlt1pi  10918  adderpq  10968  mulerpq  10969  recmulnq  10976  addsrpr  11087  mulsrpr  11088  opelcn  11141  opelreal  11142  elreal  11143  elreal2  11144  0ncn  11145  addcnsr  11147  mulcnsr  11148  xrlenlt  11301  elnn0  12533  elnnne0  12545  un0addcl  12564  un0mulcl  12565  elxnn0  12606  uztrn2  12909  elnnuz  12930  elnn0uz  12931  elq  13002  elxr  13170  elfzm1b  13660  elfz0lmr  13842  uzrdgfni  14025  fzennn  14035  ser0  14121  hash2pwpr  14544  iswrd  14583  pfxccatpfx1  14808  s3iunsndisj  15044  sumz  15811  sumss  15813  fsumcvg3  15818  abscvgcvg  15909  isumshft  15931  prodf1  15983  prodeq1i  16008  zprod  16027  prod1  16034  prodss  16037  prodsn  16052  prodsnf  16054  bpolydiflem  16143  bpoly2  16146  bpoly3  16147  bpoly4  16148  ruclem6  16326  divides  16347  dvdsflip  16410  pwp1fsum  16484  sadc0  16547  eulerthlem2  16876  prm23lt5  16909  4sqlem2  17044  4sqlem12  17051  vdwpc  17075  xpscf  17654  cidpropd  17801  oppcsect  17870  funcpropd  17994  natpropd  18071  dfinito2  18095  dftermo2  18096  initoeu2lem0  18105  arwhoma  18137  eldmcoa  18157  pospo  18434  psss  18671  ex-chn1  18728  ex-chn2  18729  ismgmn0  18735  gsumpropd2lem  18784  elefmndbas  18985  smndex1basss  19020  smndex1mgm  19022  pwmnd  19059  dfgrp2e  19090  mulgfval  19195  eqg0subg  19327  cycsubmel  19331  ghmeqker  19373  elcntr  19460  cntri  19462  cntzsgrpcl  19464  oppgsubg  19493  fvcosymgeq  19559  symgfixels  19564  pmtrfrn  19588  efgsfo  19869  efgrelexlemb  19880  lt6abl  20025  dmdprd  20130  dprdval  20135  dprdw  20142  srgbinomlem4  20371  isnirred  20564  isrhm  20623  isdrng3lem1  20917  issrng  21013  lspexchn2  21321  lspindp2l  21324  lspindp2  21325  lbsextlem2  21349  rnglidl1  21424  df2idl2  21462  2idlss  21467  rngqiprngimfo  21507  prmidl0  21544  cnfldfun  21602  pzriprnglem3  21699  pzriprnglem4  21700  pzriprnglem7  21703  pzriprnglem8  21704  pzriprnglem9  21705  pzriprnglem12  21708  pzriprnglem14  21710  dsmmelbas  21955  frlmbas3  21992  lindsind2  22035  islindf4  22054  psrbagf  22136  evlslem4  22295  psdmul  22397  ply1bascl2  22432  cply1mul  22524  lply1binom  22538  matsubgcell  22659  matinvgcell  22660  matvscacell  22661  matepmcl  22687  matepm2cl  22688  scmatscm  22738  smatvscl  22749  marrepcl  22789  marepvcl  22794  mulmarep1el  22797  mulmarep1gsum1  22798  mulmarep1gsum2  22799  submabas  22803  m1detdiag  22822  mdetdiag  22824  m2detleib  22856  gsummatr01lem3  22882  gsummatr01  22884  smadiadetlem4  22894  slesolinv  22908  slesolinvbi  22909  slesolex  22910  cramerimplem2  22912  pmatcoe1fsupp  22929  mat2pmatbas  22954  mat2pmatmul  22959  mat2pmatlin  22963  decpmatmul  23000  monmatcollpw  23007  pm2mpf1  23027  pm2mpghm  23044  istps  23162  mretopd  23320  neiptopuni  23358  lpdifsn  23371  restcls  23409  perfopn  23413  pnfnei  23448  mnfnei  23449  lmss  23526  hauscmplem  23634  is2ndc  23674  2ndcdisj  23685  hausnlly  23722  txuni2  23794  ptpjpre1  23800  elpt  23801  dfac14  23847  xkococn  23889  fbasrn  24113  fin1aufil  24161  elfm2  24177  elfm3  24179  fbflim  24205  flffbas  24224  cnpflf2  24229  fclsbas  24250  efmndtmd  24330  tsmssubm  24372  iscusp2  24530  imasdsf1olem  24602  metustel  24779  metuel2  24794  isnghm  24952  opnreen  25061  iccpnfcnv  25175  ehleudisval  25650  ehl1eudis  25651  ehl2eudis  25653  minveclem3b  25659  ovoliunlem1  25733  ioombl1lem4  25792  subopnmbl  25835  vitalilem2  25840  vitalilem3  25841  mbfimaopnlem  25886  mbfimaopn2  25888  itg2l  25960  dvply1  26517  vieta1lem1  26545  vieta1lem2  26546  elaa  26551  taylthlem2  26613  abelthlem6  26675  abelthlem9  26679  sinq34lt0t  26750  ellogrn  26799  dvrelog  26877  ellogdm  26879  logtayl2  26902  cxpcn3lem  26987  cxpcn3  26988  1cubr  27082  atandm  27116  atanf  27120  reasinsin  27136  atans2  27171  dmarea  27197  xrlimcnp  27208  amgmlem  27229  ppiublem1  27441  lgsdir2lem2  27565  gausslemma2dlem1a  27604  lgsquadlem1  27619  lgsquadlem2  27620  2sqlem1  27656  rpvmasum2  27751  madeval2  28101  newval  28103  leftval  28117  rightval  28118  lltr  28130  madess  28134  oldssmade  28135  oldss  28138  lrold  28165  addsproplem2  28238  addsproplem4  28240  addsproplem6  28242  negsproplem4  28299  negsproplem6  28301  precsexlem10  28484  precsexlem11  28485  ltonold  28529  elnns  28608  elzs  28652  elcgrabasi  29257  edgiedgb  29514  isuhgr  29520  isushgr  29521  isupgr  29544  isumgr  29555  umgredg  29598  umgrpredgv  29600  umgredgne  29605  umgredgnlp  29607  isuspgr  29615  isusgr  29616  ausgrusgri  29631  usgredgppr  29659  edgssv2  29661  uspgredg2vlem  29686  uspgredg2v  29687  ushgredgedg  29692  ushgredgedgloop  29694  griedg0ssusgr  29728  uhgrissubgr  29738  subumgredg2  29748  uhgrspansubgrlem  29753  umgrres1lem  29773  upgrres1  29776  nbgrcl  29798  nbuhgr  29806  nbuhgr2vtx1edgblem  29814  nbupgrres  29827  edgnbusgreu  29830  nbusgredgeu0  29831  nbusgrf1o0  29832  hashnbusgrnn0  29839  nbupgruvtxres  29870  cffldtocusgr  29910  cusgrfilem2  29919  vtxdg0v  29936  vtxduhgr0nedg  29955  uhgrvd00  29997  vtxdginducedm1  30006  finsumvtxdg2ssteplem4  30011  wlk1walk  30101  wlkp1lem6  30139  iswwlks  30307  wwlknllvtx  30317  wwlksonvtx  30326  wspthnonp  30330  wlkiswwlksupgr2  30348  wwlksnwwlksnon  30386  2pthon3v  30414  umgr2wlk  30420  elwwlks2s3  30422  wwlks2onv  30424  elwwlks2ons3im  30425  isclwwlk  30457  clwwlkccatlem  30462  clwlkclwwlk  30475  wwlksext2clwwlk  30530  hashecclwwlkn1  30550  umgrhashecclwwlk  30551  clwwlknon1  30570  clwwlknon1nloop  30572  clwwlknon2x  30576  loop1cycl  30626  1pthon2v  30636  uhgr3cyclex  30665  isconngr  30672  isconngr1  30673  eucrctshift  30726  frgrnbnb  30776  frgrncvvdeqlem1  30782  frgrncvvdeqlem2  30783  frgrncvvdeqlem3  30784  frgrncvvdeqlem9  30790  fusgreghash2wspv  30818  extwwlkfab  30835  numclwwlk1lem2foa  30837  numclwwlk1lem2fo  30841  clwlknon2num  30851  numclwlk2lem2f1o  30862  numclwwlk5lem  30870  topnfbey  30952  isvclem  31061  isnvlem  31094  vsfval  31117  h2hlm  31464  hhcmpl  31684  hhcms  31687  elch0  31738  omlsilem  31886  h1de2ctlem  32039  elspansni  32042  nonbooli  32135  spansncvi  32136  adjeq  32419  cnlnssadj  32564  cnvbraval  32594  brabgaf  33082  2ndresdju  33125  fmptdf2  33132  fmptcof2  33133  acunirnmpt  33135  acunirnmpt2  33136  ofpreima  33141  fcnvgreu  33148  fdifsuppconst  33164  1stpreima  33182  2ndpreima  33183  fz2ssnn0  33259  elxrge02  33380  ccatws1f1o  33396  gsumwrd2dccatlem  33520  psgnfzto1stlem  33543  cycpmgcl  33596  elrgspnlem1  33685  elrgspnlem2  33686  elrgspnlem4  33688  elrgspnsubrunlem1  33690  rlocisunit  33719  domnprodeq0  33722  nsgqusf1olem2  33846  nsgqusf1olem3  33847  crngmxidl  33875  opprnsg  33889  rprmirredb  33945  zringfrac  33967  evl1deg2  33990  evl1deg3  33991  ply1degltel  34007  ply1degleel  34008  evlextv  34055  esplyfval3  34085  esplyindfv  34089  esplyfvn  34090  vietalem  34092  fldextrspunlsplem  34186  isconstr  34249  constrsuc  34251  constrconj  34258  submatres  34319  lmat22lem  34330  crefdf  34361  cmppcmp  34371  rspectopn  34380  prsdm  34427  prsrn  34428  xrge0iifcnv  34446  xrge0iifiso  34448  xrge0iifhom  34450  pnfneige0  34464  qqhre  34533  rrhre  34534  esumnul  34561  esumcvgsum  34601  ldgenpisyslem1  34677  measvuni  34728  cntnevol  34742  dya2iocnrect  34795  sibf0  34848  oddpwdc  34868  eulerpartlemd  34880  eulerpartgbij  34886  eulerpartlemgh  34892  isrrvv  34957  coinfliprv  34997  ballotlem7  35050  signswch  35072  hashreprin  35131  chtvalz  35140  circlemethhgt  35154  hgt750lemb  35167  tgoldbachgt  35174  bnj23  35231  bnj158  35242  bnj168  35243  bnj1138  35301  bnj1143  35302  bnj1454  35354  bnj110  35370  bnj882  35438  bnj893  35440  bnj916  35445  bnj970  35459  bnj983  35463  bnj984  35464  bnj1137  35507  bnj1174  35515  bnj1388  35545  bnj1398  35546  r1wf  35606  onrankid  35611  onvf1odlem4  35706  subfacp1lem5  35766  satfv1  35945  satfrnmapom  35952  satf0op  35959  satf0n0  35960  fmlafvel  35967  fmlaomn0  35972  fmlan0  35973  satffunlem2lem2  35988  satfv0fvfmla0  35995  satefvfmla0  36000  mrsub0  36098  mrsubccat  36100  mrsubcn  36101  elmrsubrn  36102  msubco  36113  msubvrs  36142  elmthm  36158  mthmblem  36162  ellcsrspsn  36223  elrn3  36344  dfon2lem7  36369  brsset  36469  eltrans  36471  elfix  36483  ellimits  36490  elfuns  36495  elsingles  36498  fvtransport  36615  brcolinear2  36641  fvray  36724  linedegen  36726  fvline  36727  ellines  36735  fwddifn0  36747  elhf  36757  hfninf  36769  rmoeqi  36810  rmoeqbii  36811  reueqi  36812  reueqbii  36813  rabeqbii  36817  iuneq12i  36818  iineq1i  36819  iineq12i  36820  riotaeqbii  36821  ixpeq1i  36823  itgeq12i  36829  cbvprodvw2  36870  fnessref  36979  ttctr  37115  bj-ififc  37286  bj-csbsnlem  37649  bj-elgab  37686  currysetlem1  37694  bj-eltag  37724  bj-sngltag  37730  bj-projun  37741  bj-velpwALT  37800  bj-0nelmpt  37869  bj-opelidres  37916  bj-inftyexpitaudisj  37960  bj-elccinfty  37969  f1omptsnlem  38093  icoreelrnab  38111  relowlpssretop  38121  rdgssun  38135  exrecfnlem  38136  finxpnom  38158  tan2h  38369  ptrecube  38372  poimirlem25  38397  poimirlem29  38401  poimirlem30  38402  poimirlem31  38403  poimirlem32  38404  cnambfre  38420  ftc1cnnc  38444  sdclem2  38495  sdclem1  38496  fdc  38498  caushft  38514  issmgrpOLD  38616  ismndo  38625  isrngo  38650  isdivrngo  38703  csbcom2fi  38879  elecALTV  39022  brrabga  39092  eldmxrncnvepres  39185  eldmxrncnvepres2  39186  elrels2  39192  blockadjliftmap  39209  dfpre  39227  eupre  39245  eldmcoss  39299  coss0  39320  petseq  39727  dath  40612  diclspsn  42070  dvh4dimlem  42319  dvh2dim  42321  dvh3dim3N  42325  lcfrvalsnN  42417  mapdh6eN  42616  mapdh7dN  42626  mapdh8b  42656  hdmap1l6e  42690  lcmfunnnd  42881  3factsumint1  42890  primrootsunit1  42966  primrootscoprmpow  42968  aks6d1c2lem4  42996  sticksstones2  43016  sticksstones3  43017  sticksstones10  43024  sticksstones12a  43026  sticksstones12  43027  aks6d1c6lem2  43040  aks6d1c6lem3  43041  redvmptabs  43238  readvrec2  43239  readvrec  43240  frlmfielbas  43391  mhpind  43443  pellex  43679  rmspecnonsq  43751  islmodfg  43913  aaitgo  44006  areaquad  44060  ordeldif1o  44104  naddwordnexlem4  44245  fpwfvss  44255  finona1cl  44296  elcnvcnvintab  44425  elnonrel  44428  elcnvcnvlem  44442  cnvcnvintabd  44443  brfvrcld2  44535  grur1cld  45073  dvgrat  45139  cvgdvgrat  45140  radcnvrat  45141  nznngen  45143  uzmptshftfval  45173  binomcxplemcvg  45181  binomcxplemnotnn0  45183  tpid3gVD  45667  en3lplem2VD  45669  orbitclmpt  45784  wfaxrep  45820  wfaxsep  45821  wfaxpow  45823  wfaxpr  45824  wfaxun  45825  wfac8prim  45828  brpermmodelcnv  45830  nregmodellem  45842  iuneq1i  45921  rexanuz3  45931  eliuniin  45934  eliuniin2  45955  disjinfi  46027  iuneqfzuzlem  46167  allbutfi  46225  eluzelz2  46234  uz0  46243  uzublem  46261  uzid3  46266  elicores  46366  uzinico  46392  climsuselem1  46440  climsuse  46441  islptre  46452  fnlimfvre  46505  limsupresico  46531  limsupvaluz  46539  limsupubuzlem  46543  limsupequzmptlem  46559  liminfresico  46602  cnrefiisplem  46660  stoweidlem14  46845  stoweidlem39  46870  stoweidlem48  46879  stoweidlem51  46882  stoweidlem59  46890  stoweidlem62  46893  wallispilem3  46898  fourierdlem42  46980  fourierdlem62  46999  fourierdlem80  47017  fourierdlem103  47040  fourierdlem104  47041  etransclem26  47091  rrxsnicc  47131  ioorrnopn  47136  ioorrnopnxr  47138  sge00  47207  sge0fodjrnlem  47247  sge0isum  47258  sge0seq  47277  meadjiunlem  47296  carageneld  47333  volicorescl  47384  hoidmv1lelem1  47422  hoidmv1le  47425  hoidmvlelem1  47426  hoidmvlelem3  47428  ovnhoilem2  47433  hoiqssbllem2  47454  opnvonmbllem2  47464  ovolval4lem1  47480  iinhoiicc  47505  vonioolem1  47511  smflimlem1  47602  smflimlem2  47603  smflim  47608  nsssmfmbf  47610  smfresal  47619  smfrec  47620  smfdiv  47628  smfpimbor1lem2  47630  smflim2  47637  smflimmpt  47641  smfinflem  47648  smflimsuplem1  47651  smflimsuplem2  47652  smflimsuplem3  47653  smflimsuplem5  47655  smflimsuplem6  47656  smflimsup  47659  smflimsupmpt  47660  smfliminfmpt  47663  fcores  47958  ndmaovcl  48094  ndmaovcom  48096  ndmaovass  48097  ndmaovdistr  48098  dfatco  48147  otiunsndisjX  48170  fvmptrabdm  48184  ceilhalfelfzo1  48225  modmknepk  48259  elsetpreimafvb  48287  sprsymrelfolem2  48396  sprsymrelf  48398  sprsymrelf1  48399  prpair  48404  prproropf1olem0  48405  paireqne  48414  fmtno4prmfac  48478  dfodd5  48579  sbgoldbo  48706  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  clnbgrcl  48740  clnbgredg  48759  sclnbgrel  48766  isubgredg  48785  uhgrimedgi  48809  isuspgrim0  48813  isuspgrimlem  48814  gricushgr  48836  clnbgrgrimlem  48852  grimedg  48854  usgrgrtrirex  48869  stgrnbgr0  48883  isubgr3stgrlem3  48887  isubgr3stgrlem4  48888  isubgr3stgrlem6  48890  isubgr3stgrlem7  48891  uspgrlimlem2  48908  uspgrlimlem3  48909  grlimedgclnbgr  48914  grlimprclnbgr  48915  grlimprclnbgrvtx  48918  grlimgrtrilem2  48921  usgrexmpl2trifr  48956  gpgvtxel  48966  gpgedgel  48969  gpgusgralem  48975  gpg5order  48979  gpgvtxedg0  48982  gpgvtxedg1  48983  gpgnbgrvtx0  48993  gpgnbgrvtx1  48994  gpg5nbgrvtx03star  48999  gpg5nbgr3star  49000  gpgvtxdg3  49001  gpg5gricstgr3  49009  gpgprismgr4cycllem3  49016  gpgprismgr4cycllem7  49020  gpgprismgr4cycllem8  49021  gpgprismgr4cycllem10  49023  pgnbgreunbgrlem3  49037  pgnbgreunbgrlem6  49043  pgnbgreunbgr  49044  uspgrsprf  49065  uspgrsprf1  49066  uspgrsprfo  49067  dfidom2  49261  ply1sclrmsm  49317  lcoop  49344  lincfsuppcl  49346  linccl  49347  lincvalsng  49349  lincvalpr  49351  lincvalsc0  49354  linc0scn0  49356  lincdifsn  49357  linc1  49358  lincsum  49362  lincscm  49363  lspsslco  49370  snlindsntor  49404  lincresunit3lem2  49413  ldepsnlinclem1  49438  ldepsnlinclem2  49439  prelrrx2  49646  prelrrx2b  49647  rrx2xpref1o  49651  rrx2plord  49653  rrx2linesl  49676  sectrcl  49951  invrcl  49953  initopropdlemlem  50168  initopropd  50172  termopropd  50173  zeroopropd  50174  oppcthin  50367  indthinc  50391  prsthinc  50393  elpglem3  50642  veronesevrowd  50815