Theorem eleq2i 2833

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

Syntax hints:   ↔ wb 208   = wceq 1548   ∈ wcel 2121

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  eleq12i  2834  eleqtri  2839  eleq2s  2859  hbxfreq  2871  nfceqi  2900  raleqbii  3313  rexeqbii  3314  rabeqi  3406  rabrabi  3412  reqabi  3416  elab2gw  3618  elab2g  3620  elrabf  3628  elrab3t  3630  elrab2  3634  cbvsbcw  3758  cbvsbcvw  3759  cbvsbc  3760  elin2  4135  elsymdif  4189  noel  4269  eltpg  4621  elunirab  4856  elintrab  4893  disjxiun  5072  exss  5405  otiunsndisj  5464  brabsb  5476  brabga  5479  epelg  5522  pofun  5547  elxp  5644  opeliunxp  5688  opeliun2xp  5689  bropaex12  5712  brab2a  5714  elcnv  5821  cnv0  5828  dmopabelb  5865  elrnmptg  5910  elres  5979  elimampt  6002  elrid  6005  rninxp  6134  elid  6154  elsuci  6383  elsucg  6384  elsuc2g  6385  elfv  6829  0fv  6872  opabiota  6913  dffv2  6926  fvopab3g  6934  fvmptex  6954  fvopab5  6973  fsneq  6980  fvn0ssdmfun  7019  fveqressseq  7024  f0cli  7043  fmptco  7075  fvrnressn  7108  funfvima  7178  elunirnALT  7200  fliftel  7257  eloprabga  7469  elrnmpo  7496  elimampo  7497  ovid  7501  offval  7633  1st2val  7963  2nd2val  7964  bropopvvv  8033  bropfvvvv  8035  fsplit  8060  xporderlem  8071  frpoins3xpg  8084  frpoins3xp3g  8085  brtpos2  8176  frrlem8  8237  frrlem9  8238  frrlem10  8239  fprresex  8254  issmo  8282  smores3  8287  tfrlem7  8316  tfrlem9  8318  tfrlem9a  8319  tfr2b  8329  tfr2  8331  rdgsuc  8357  frsucmptn  8372  tz7.48-2  8375  el1o  8424  ord2eln012  8426  dif1o  8429  ondif2  8431  oawordeulem  8483  elecg  8682  brecop  8751  erovlem  8754  eceqoveq  8763  mapsncnv  8835  mptelixpg  8877  brsdom  8915  isfi  8916  enssdomOLD  8918  brdom2  8923  xpcomco  8999  brsdom2  9033  en3lplem2  9529  cnfcom2lem  9617  brttrcl2  9630  ttrcltr  9632  rnttrcl  9638  epfrs  9647  r1limg  9690  r1ord  9699  r1ord3  9701  tz9.12lem3  9708  rankvaln  9718  r1elss  9725  rankpwi  9742  ssrankr1  9754  r1val3  9757  r1pw  9764  rankr1b  9783  djur  9838  djuunxp  9840  eldju2ndl  9843  eldju2ndr  9844  isnum2  9864  cardprclem  9898  infxpenlem  9930  alephcard  9987  alephnbtwn  9988  alephnbtwn2  9989  alephord2  9993  alephsdom  10003  dfac3  10038  dfac5lem2  10041  dfac5lem3  10042  dfac5lem5  10044  pwsdompw  10120  cfub  10166  cardcf  10169  cflecard  10170  cfle  10171  cflim2  10180  cofsmo  10186  cfidm  10192  isfin3  10213  isfin5  10216  isfin6  10217  sdom2en01  10219  fin23lem26  10242  fin23lem30  10259  isf32lem5  10274  itunitc1  10337  ituniiun  10339  axdc3lem3  10369  axcclem  10374  axdclem  10436  iunfo  10456  iundom2g  10457  cardidg  10465  konigthlem  10486  alephadd  10495  alephreg  10500  pwcfsdom  10501  cfpwsdom  10502  elgch  10540  fpwwe2lem11  10559  canth4  10565  wunex2  10656  r1tskina  10700  elni  10794  nlt1pi  10824  adderpq  10874  mulerpq  10875  recmulnq  10882  addsrpr  10993  mulsrpr  10994  opelcn  11047  opelreal  11048  elreal  11049  elreal2  11050  0ncn  11051  addcnsr  11053  mulcnsr  11054  xrlenlt  11205  elnn0  12434  elnnne0  12446  un0addcl  12465  un0mulcl  12466  elxnn0  12507  uztrn2  12802  elnnuz  12823  elnn0uz  12824  elq  12895  elxr  13062  elfzm1b  13551  elfz0lmr  13733  uzrdgfni  13915  fzennn  13925  ser0  14011  hash2pwpr  14433  iswrd  14472  pfxccatpfx1  14693  s3iunsndisj  14925  sumz  15679  sumss  15681  fsumcvg3  15686  abscvgcvg  15777  isumshft  15799  prodf1  15851  prodeq1i  15876  zprod  15897  prod1  15904  prodss  15907  prodsn  15922  prodsnf  15924  bpolydiflem  16014  bpoly2  16017  bpoly3  16018  bpoly4  16019  ruclem6  16197  divides  16218  dvdsflip  16281  pwp1fsum  16355  sadc0  16418  eulerthlem2  16747  prm23lt5  16780  4sqlem2  16915  4sqlem12  16922  vdwpc  16946  xpscf  17524  cidpropd  17671  oppcsect  17740  funcpropd  17864  natpropd  17941  dfinito2  17965  dftermo2  17966  initoeu2lem0  17975  arwhoma  18007  eldmcoa  18027  pospo  18304  psss  18541  ex-chn1  18598  ex-chn2  18599  ismgmn0  18605  gsumpropd2lem  18642  elefmndbas  18836  smndex1basss  18871  smndex1mgm  18873  pwmnd  18903  dfgrp2e  18934  mulgfval  19040  eqg0subg  19166  cycsubmel  19170  ghmeqker  19213  elcntr  19300  cntri  19302  cntzsgrpcl  19304  oppgsubg  19333  fvcosymgeq  19399  symgfixels  19404  pmtrfrn  19428  efgsfo  19709  efgrelexlemb  19720  lt6abl  19865  dmdprd  19970  dprdval  19975  dprdw  19982  srgbinomlem4  20205  isnirred  20395  isrhm  20453  issrng  20820  lspexchn2  21128  lspindp2l  21131  lspindp2  21132  lbsextlem2  21156  rnglidl1  21229  df2idl2  21254  2idlss  21259  rngqiprngimfo  21298  cnfldfun  21365  pzriprnglem3  21462  pzriprnglem4  21463  pzriprnglem7  21466  pzriprnglem8  21467  pzriprnglem9  21468  pzriprnglem12  21471  pzriprnglem14  21473  dsmmelbas  21718  frlmbas3  21755  lindsind2  21798  islindf4  21817  psrbagf  21897  evlslem4  22056  psdmul  22158  ply1bascl2  22193  cply1mul  22286  lply1binom  22300  matsubgcell  22421  matinvgcell  22422  matvscacell  22423  matepmcl  22449  matepm2cl  22450  scmatscm  22500  smatvscl  22511  marrepcl  22551  marepvcl  22556  mulmarep1el  22559  mulmarep1gsum1  22560  mulmarep1gsum2  22561  submabas  22565  m1detdiag  22584  mdetdiag  22586  m2detleib  22618  gsummatr01lem3  22644  gsummatr01  22646  smadiadetlem4  22656  slesolinv  22667  slesolinvbi  22668  slesolex  22669  cramerimplem2  22671  pmatcoe1fsupp  22688  mat2pmatbas  22713  mat2pmatmul  22718  mat2pmatlin  22722  decpmatmul  22759  monmatcollpw  22766  pm2mpf1  22786  pm2mpghm  22803  istps  22921  mretopd  23079  neiptopuni  23117  lpdifsn  23130  restcls  23168  perfopn  23172  pnfnei  23207  mnfnei  23208  lmss  23285  hauscmplem  23393  is2ndc  23433  2ndcdisj  23443  hausnlly  23480  txuni2  23552  ptpjpre1  23558  elpt  23559  dfac14  23605  xkococn  23647  fbasrn  23871  fin1aufil  23919  elfm2  23935  elfm3  23937  fbflim  23963  flffbas  23982  cnpflf2  23987  fclsbas  24008  efmndtmd  24088  tsmssubm  24130  iscusp2  24288  imasdsf1olem  24360  metustel  24537  metuel2  24552  isnghm  24710  opnreen  24819  iccpnfcnv  24933  ehleudisval  25408  ehl1eudis  25409  ehl2eudis  25411  minveclem3b  25417  ovoliunlem1  25491  ioombl1lem4  25550  subopnmbl  25593  vitalilem2  25598  vitalilem3  25599  mbfimaopnlem  25644  mbfimaopn2  25646  itg2l  25718  dvply1  26272  vieta1lem1  26298  vieta1lem2  26299  elaa  26304  taylthlem2  26361  abelthlem6  26423  abelthlem9  26427  sinq34lt0t  26495  ellogrn  26545  dvrelog  26623  ellogdm  26625  logtayl2  26648  cxpcn3lem  26733  cxpcn3  26734  1cubr  26828  atandm  26862  atanf  26866  reasinsin  26882  atans2  26917  dmarea  26943  xrlimcnp  26954  amgmlem  26975  ppiublem1  27187  lgsdir2lem2  27311  gausslemma2dlem1a  27350  lgsquadlem1  27365  lgsquadlem2  27366  2sqlem1  27402  rpvmasum2  27497  madeval2  27847  newval  27849  leftval  27863  rightval  27864  lltr  27876  madess  27880  oldssmade  27881  oldss  27884  lrold  27911  addsproplem2  27984  addsproplem4  27986  addsproplem6  27988  negsproplem4  28045  negsproplem6  28047  precsexlem10  28230  precsexlem11  28231  ltonold  28275  elnns  28354  elzs  28398  edgiedgb  29145  isuhgr  29151  isushgr  29152  isupgr  29175  isumgr  29186  umgredg  29229  umgrpredgv  29231  umgredgne  29236  umgredgnlp  29238  isuspgr  29243  isusgr  29244  ausgrusgri  29259  usgredgppr  29287  edgssv2  29289  uspgredg2vlem  29314  uspgredg2v  29315  ushgredgedg  29320  ushgredgedgloop  29322  griedg0ssusgr  29356  uhgrissubgr  29366  subumgredg2  29376  uhgrspansubgrlem  29381  umgrres1lem  29401  upgrres1  29404  nbgrcl  29426  nbuhgr  29434  nbuhgr2vtx1edgblem  29442  nbupgrres  29455  edgnbusgreu  29458  nbusgredgeu0  29459  nbusgrf1o0  29460  hashnbusgrnn0  29467  nbupgruvtxres  29498  cffldtocusgr  29538  cusgrfilem2  29547  vtxdg0v  29564  vtxduhgr0nedg  29583  uhgrvd00  29625  vtxdginducedm1  29634  finsumvtxdg2ssteplem4  29639  wlk1walk  29729  wlkp1lem6  29767  iswwlks  29926  wwlknllvtx  29936  wwlksonvtx  29945  wspthnonp  29949  wlkiswwlksupgr2  29967  wwlksnwwlksnon  30005  2pthon3v  30033  umgr2wlk  30039  elwwlks2s3  30041  wwlks2onv  30043  elwwlks2ons3im  30044  isclwwlk  30076  clwwlkccatlem  30081  clwlkclwwlk  30094  wwlksext2clwwlk  30149  hashecclwwlkn1  30169  umgrhashecclwwlk  30170  clwwlknon1  30189  clwwlknon1nloop  30191  clwwlknon2x  30195  1pthon2v  30245  uhgr3cyclex  30274  isconngr  30281  isconngr1  30282  eucrctshift  30335  frgrnbnb  30385  frgrncvvdeqlem1  30391  frgrncvvdeqlem2  30392  frgrncvvdeqlem3  30393  frgrncvvdeqlem9  30399  fusgreghash2wspv  30427  extwwlkfab  30444  numclwwlk1lem2foa  30446  numclwwlk1lem2fo  30450  clwlknon2num  30460  numclwlk2lem2f1o  30471  numclwwlk5lem  30479  topnfbey  30561  isvclem  30670  isnvlem  30703  vsfval  30726  h2hlm  31073  hhcmpl  31293  hhcms  31296  elch0  31347  omlsilem  31495  h1de2ctlem  31648  elspansni  31651  nonbooli  31744  spansncvi  31745  adjeq  32028  cnlnssadj  32173  cnvbraval  32203  brabgaf  32702  2ndresdju  32745  fmptdF  32752  fmptcof2  32753  acunirnmpt  32755  acunirnmpt2  32756  ofpreima  32761  fcnvgreu  32768  fdifsuppconst  32785  1stpreima  32803  2ndpreima  32804  fz2ssnn0  32881  elxrge02  33014  ccatws1f1o  33034  gsumwrd2dccatlem  33162  psgnfzto1stlem  33185  cycpmgcl  33238  elrgspnlem1  33327  elrgspnlem2  33328  elrgspnlem4  33330  elrgspnsubrunlem1  33332  domnprodeq0  33361  nsgqusf1olem2  33501  nsgqusf1olem3  33502  prmidl0  33537  crngmxidl  33556  opprnsg  33571  rprmirredb  33627  zringfrac  33649  evl1deg2  33672  evl1deg3  33673  ply1degltel  33689  ply1degleel  33690  evlextv  33738  esplyfval3  33768  esplyindfv  33772  esplyfvn  33773  vietalem  33775  fldextrspunlsplem  33869  isconstr  33932  constrsuc  33934  constrconj  33941  submatres  34002  lmat22lem  34013  crefdf  34044  cmppcmp  34054  rspectopn  34063  prsdm  34110  prsrn  34111  xrge0iifcnv  34129  xrge0iifiso  34131  xrge0iifhom  34133  pnfneige0  34147  qqhre  34216  rrhre  34217  esumnul  34244  esumcvgsum  34284  ldgenpisyslem1  34359  measvuni  34410  cntnevol  34424  dya2iocnrect  34477  sibf0  34530  oddpwdc  34550  eulerpartlemd  34562  eulerpartgbij  34568  eulerpartlemgh  34574  isrrvv  34639  coinfliprv  34679  ballotlem7  34732  signswch  34757  hashreprin  34816  chtvalz  34825  circlemethhgt  34839  hgt750lemb  34852  tgoldbachgt  34859  bnj23  34916  bnj158  34927  bnj168  34928  bnj1138  34986  bnj1143  34987  bnj1454  35039  bnj110  35055  bnj882  35123  bnj893  35125  bnj916  35130  bnj970  35144  bnj983  35148  bnj984  35149  bnj1137  35192  bnj1174  35200  bnj1388  35230  bnj1398  35231  r1wf  35292  onvf1odlem4  35349  loop1cycl  35380  subfacp1lem5  35427  satfv1  35606  satfrnmapom  35613  satf0op  35620  satf0n0  35621  fmlafvel  35628  fmlaomn0  35633  fmlan0  35634  satffunlem2lem2  35649  satfv0fvfmla0  35656  satefvfmla0  35661  mrsub0  35759  mrsubccat  35761  mrsubcn  35762  elmrsubrn  35763  msubco  35774  msubvrs  35803  elmthm  35819  mthmblem  35823  ellcsrspsn  35884  elrn3  36005  dfon2lem7  36030  brsset  36130  eltrans  36132  elfix  36144  ellimits  36151  elfuns  36156  elsingles  36159  fvtransport  36275  brcolinear2  36301  fvray  36384  linedegen  36386  fvline  36387  ellines  36395  fwddifn0  36407  elhf  36417  hfninf  36429  rmoeqi  36430  rmoeqbii  36431  reueqi  36432  reueqbii  36433  rabeqbii  36437  iuneq12i  36438  iineq1i  36439  iineq12i  36440  riotaeqbii  36441  ixpeq1i  36443  itgeq12i  36449  cbvprodvw2  36490  fnessref  36600  ttctr  36736  bj-ififc  36908  bj-csbsnlem  37271  bj-elgab  37307  currysetlem1  37315  bj-eltag  37345  bj-sngltag  37351  bj-projun  37362  bj-velpwALT  37421  bj-0nelmpt  37489  bj-opelidres  37536  bj-inftyexpitaudisj  37580  bj-elccinfty  37589  f1omptsnlem  37713  icoreelrnab  37731  relowlpssretop  37741  rdgssun  37755  exrecfnlem  37756  finxpnom  37778  uncov  37983  tan2h  37994  ptrecube  38002  poimirlem25  38027  poimirlem29  38031  poimirlem30  38032  poimirlem31  38033  poimirlem32  38034  cnambfre  38050  ftc1cnnc  38074  sdclem2  38124  sdclem1  38125  fdc  38127  caushft  38143  issmgrpOLD  38245  ismndo  38254  isrngo  38279  isdivrngo  38332  csbcom2fi  38510  elecALTV  38653  brrabga  38723  eldmxrncnvepres  38816  eldmxrncnvepres2  38817  elrels2  38823  blockadjliftmap  38840  dfpre  38858  eupre  38876  eldmcoss  38930  coss0  38951  petseq  39358  dath  40243  diclspsn  41701  dvh4dimlem  41950  dvh2dim  41952  dvh3dim3N  41956  lcfrvalsnN  42048  mapdh6eN  42247  mapdh7dN  42257  mapdh8b  42287  hdmap1l6e  42321  lcmfunnnd  42512  3factsumint1  42521  primrootsunit1  42597  primrootscoprmpow  42599  aks6d1c2lem4  42627  sticksstones2  42647  sticksstones3  42648  sticksstones10  42655  sticksstones12a  42657  sticksstones12  42658  aks6d1c6lem2  42671  aks6d1c6lem3  42672  redvmptabs  42852  readvrec2  42853  readvrec  42854  frlmfielbas  43005  mhpind  43059  pellex  43295  rmspecnonsq  43367  islmodfg  43529  aaitgo  43622  areaquad  43676  ordeldif1o  43720  naddwordnexlem4  43861  fpwfvss  43871  finona1cl  43912  elcnvcnvintab  44041  elnonrel  44044  elcnvcnvlem  44058  cnvcnvintabd  44059  brfvrcld2  44151  grur1cld  44691  dvgrat  44771  cvgdvgrat  44772  radcnvrat  44773  nznngen  44775  uzmptshftfval  44805  binomcxplemcvg  44813  binomcxplemnotnn0  44815  tpid3gVD  45300  en3lplem2VD  45302  orbitclmpt  45417  wfaxrep  45453  wfaxsep  45454  wfaxpow  45456  wfaxpr  45457  wfaxun  45458  wfac8prim  45461  brpermmodelcnv  45463  nregmodellem  45475  iuneq1i  45547  rexanuz3  45557  eliuniin  45560  eliuniin2  45581  disjinfi  45653  iuneqfzuzlem  45793  allbutfi  45851  eluzelz2  45860  uz0  45869  uzublem  45887  uzid3  45892  elicores  45992  uzinico  46018  climsuselem1  46066  climsuse  46067  islptre  46078  fnlimfvre  46131  limsupresico  46157  limsupvaluz  46165  limsupubuzlem  46169  limsupequzmptlem  46185  liminfresico  46228  cnrefiisplem  46286  stoweidlem14  46471  stoweidlem39  46496  stoweidlem48  46505  stoweidlem51  46508  stoweidlem59  46516  stoweidlem62  46519  wallispilem3  46524  fourierdlem42  46606  fourierdlem62  46625  fourierdlem80  46643  fourierdlem103  46666  fourierdlem104  46667  etransclem26  46717  rrxsnicc  46757  ioorrnopn  46762  ioorrnopnxr  46764  sge00  46833  sge0fodjrnlem  46873  sge0isum  46884  sge0seq  46903  meadjiunlem  46922  carageneld  46959  volicorescl  47010  hoidmv1lelem1  47048  hoidmv1le  47051  hoidmvlelem1  47052  hoidmvlelem3  47054  ovnhoilem2  47059  hoiqssbllem2  47080  opnvonmbllem2  47090  ovolval4lem1  47106  iinhoiicc  47131  vonioolem1  47137  smflimlem1  47228  smflimlem2  47229  smflim  47234  nsssmfmbf  47236  smfresal  47245  smfrec  47246  smfdiv  47254  smfpimbor1lem2  47256  smflim2  47263  smflimmpt  47267  smfinflem  47274  smflimsuplem1  47277  smflimsuplem2  47278  smflimsuplem3  47279  smflimsuplem5  47281  smflimsuplem6  47282  smflimsup  47285  smflimsupmpt  47286  smfliminfmpt  47289  chnerlem1  47341  chnerlem2  47342  tannpoly  47367  sinnpoly  47368  fcores  47544  ndmaovcl  47680  ndmaovcom  47682  ndmaovass  47683  ndmaovdistr  47684  dfatco  47733  otiunsndisjX  47756  fvmptrabdm  47770  ceilhalfelfzo1  47811  modmknepk  47845  elsetpreimafvb  47873  sprsymrelfolem2  47982  sprsymrelf  47984  sprsymrelf1  47985  prpair  47990  prproropf1olem0  47991  paireqne  48000  fmtno4prmfac  48064  dfodd5  48165  sbgoldbo  48292  nnsum4primeseven  48305  nnsum4primesevenALTV  48306  clnbgrcl  48326  clnbgredg  48345  sclnbgrel  48352  isubgredg  48371  uhgrimedgi  48395  isuspgrim0  48399  isuspgrimlem  48400  gricushgr  48422  clnbgrgrimlem  48438  grimedg  48440  usgrgrtrirex  48455  stgrnbgr0  48469  isubgr3stgrlem3  48473  isubgr3stgrlem4  48474  isubgr3stgrlem6  48476  isubgr3stgrlem7  48477  uspgrlimlem2  48494  uspgrlimlem3  48495  grlimedgclnbgr  48500  grlimprclnbgr  48501  grlimprclnbgrvtx  48504  grlimgrtrilem2  48507  usgrexmpl2trifr  48542  gpgvtxel  48552  gpgedgel  48555  gpgusgralem  48561  gpg5order  48565  gpgvtxedg0  48568  gpgvtxedg1  48569  gpgnbgrvtx0  48579  gpgnbgrvtx1  48580  gpg5nbgrvtx03star  48585  gpg5nbgr3star  48586  gpgvtxdg3  48587  gpg5gricstgr3  48595  gpgprismgr4cycllem3  48602  gpgprismgr4cycllem7  48606  gpgprismgr4cycllem8  48607  gpgprismgr4cycllem10  48609  pgnbgreunbgrlem3  48623  pgnbgreunbgrlem6  48629  pgnbgreunbgr  48630  uspgrsprf  48651  uspgrsprf1  48652  uspgrsprfo  48653  ply1sclrmsm  48889  lcoop  48916  lincfsuppcl  48918  linccl  48919  lincvalsng  48921  lincvalpr  48923  lincvalsc0  48926  linc0scn0  48928  lincdifsn  48929  linc1  48930  lincsum  48934  lincscm  48935  lspsslco  48942  snlindsntor  48976  lincresunit3lem2  48985  ldepsnlinclem1  49010  ldepsnlinclem2  49011  prelrrx2  49218  prelrrx2b  49219  rrx2xpref1o  49223  rrx2plord  49225  rrx2linesl  49248  sectrcl  49526  invrcl  49528  initopropdlemlem  49743  initopropd  49747  termopropd  49748  zeroopropd  49749  oppcthin  49942  indthinc  49966  prsthinc  49968  elpglem3  50217