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 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eleq12i  2832  eleqtri  2837  eleq2s  2857  hbxfreq  2869  nfceqi  2898  raleqbii  3311  rexeqbii  3312  rabeqi  3404  rabrabi  3410  reqabi  3414  elab2gw  3616  elab2g  3618  elrabf  3626  elrab3t  3628  elrab2  3632  cbvsbcw  3756  cbvsbcvw  3757  cbvsbc  3758  elin2  4132  elsymdif  4186  noel  4266  eltpg  4618  elunirab  4853  elintrab  4890  disjxiun  5069  exss  5402  otiunsndisj  5461  brabsb  5473  brabga  5476  epelg  5519  pofun  5544  elxp  5641  opeliunxp  5685  opeliun2xp  5686  bropaex12  5709  brab2a  5711  elcnv  5818  dmopabelb  5858  elrnmptg  5903  elres  5972  elimampt  5995  elrid  5998  cnv0  6090  rninxp  6130  elid  6150  elsuci  6379  elsucg  6380  elsuc2g  6381  elfv  6825  0fv  6868  opabiota  6909  dffv2  6922  fvopab3g  6930  fvmptex  6950  fvopab5  6969  fsneq  6976  fvn0ssdmfun  7015  fveqressseq  7020  f0cli  7039  fmptco  7071  fvrnressn  7104  funfvima  7174  elunirnALT  7196  fliftel  7253  eloprabga  7465  elrnmpo  7492  elimampo  7493  ovid  7497  offval  7629  1st2val  7959  2nd2val  7960  bropopvvv  8029  bropfvvvv  8031  fsplit  8056  xporderlem  8067  frpoins3xpg  8080  frpoins3xp3g  8081  brtpos2  8172  frrlem8  8233  frrlem9  8234  frrlem10  8235  fprresex  8250  issmo  8278  smores3  8283  tfrlem7  8312  tfrlem9  8314  tfrlem9a  8315  tfr2b  8325  tfr2  8327  rdgsuc  8353  frsucmptn  8368  tz7.48-2  8371  el1o  8420  ord2eln012  8422  dif1o  8425  ondif2  8427  oawordeulem  8479  elecg  8678  brecop  8747  erovlem  8750  eceqoveq  8759  mapsncnv  8831  mptelixpg  8873  brsdom  8911  isfi  8912  enssdomOLD  8914  brdom2  8919  xpcomco  8995  brsdom2  9029  en3lplem2  9525  cnfcom2lem  9613  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  epfrs  9643  r1limg  9686  r1ord  9695  r1ord3  9697  tz9.12lem3  9704  rankvaln  9714  r1elss  9721  rankpwi  9738  ssrankr1  9750  r1val3  9753  r1pw  9760  rankr1b  9779  djur  9834  djuunxp  9836  eldju2ndl  9839  eldju2ndr  9840  isnum2  9860  cardprclem  9894  infxpenlem  9926  alephcard  9983  alephnbtwn  9984  alephnbtwn2  9985  alephord2  9989  alephsdom  9999  dfac3  10034  dfac5lem2  10037  dfac5lem3  10038  dfac5lem5  10040  pwsdompw  10116  cfub  10162  cardcf  10165  cflecard  10166  cfle  10167  cflim2  10176  cofsmo  10182  cfidm  10188  isfin3  10209  isfin5  10212  isfin6  10213  sdom2en01  10215  fin23lem26  10238  fin23lem30  10255  isf32lem5  10270  itunitc1  10333  ituniiun  10335  axdc3lem3  10365  axcclem  10370  axdclem  10432  iunfo  10452  iundom2g  10453  cardidg  10461  konigthlem  10482  alephadd  10491  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  elgch  10536  fpwwe2lem11  10555  canth4  10561  wunex2  10652  r1tskina  10696  elni  10790  nlt1pi  10820  adderpq  10870  mulerpq  10871  recmulnq  10878  addsrpr  10989  mulsrpr  10990  opelcn  11043  opelreal  11044  elreal  11045  elreal2  11046  0ncn  11047  addcnsr  11049  mulcnsr  11050  xrlenlt  11201  elnn0  12430  elnnne0  12442  un0addcl  12461  un0mulcl  12462  elxnn0  12503  uztrn2  12798  elnnuz  12819  elnn0uz  12820  elq  12891  elxr  13058  elfzm1b  13547  elfz0lmr  13729  uzrdgfni  13911  fzennn  13921  ser0  14007  hash2pwpr  14429  iswrd  14468  pfxccatpfx1  14689  s3iunsndisj  14921  sumz  15675  sumss  15677  fsumcvg3  15682  abscvgcvg  15773  isumshft  15795  prodf1  15847  prodeq1i  15872  zprod  15893  prod1  15900  prodss  15903  prodsn  15918  prodsnf  15920  bpolydiflem  16010  bpoly2  16013  bpoly3  16014  bpoly4  16015  ruclem6  16193  divides  16214  dvdsflip  16277  pwp1fsum  16351  sadc0  16414  eulerthlem2  16743  prm23lt5  16776  4sqlem2  16911  4sqlem12  16918  vdwpc  16942  xpscf  17520  cidpropd  17667  oppcsect  17736  funcpropd  17860  natpropd  17937  dfinito2  17961  dftermo2  17962  initoeu2lem0  17971  arwhoma  18003  eldmcoa  18023  pospo  18300  psss  18537  ex-chn1  18594  ex-chn2  18595  ismgmn0  18601  gsumpropd2lem  18638  elefmndbas  18832  smndex1basss  18867  smndex1mgm  18869  pwmnd  18899  dfgrp2e  18930  mulgfval  19036  eqg0subg  19162  cycsubmel  19166  ghmeqker  19209  elcntr  19296  cntri  19298  cntzsgrpcl  19300  oppgsubg  19329  fvcosymgeq  19395  symgfixels  19400  pmtrfrn  19424  efgsfo  19705  efgrelexlemb  19716  lt6abl  19861  dmdprd  19966  dprdval  19971  dprdw  19978  srgbinomlem4  20201  isnirred  20391  isrhm  20449  issrng  20816  lspexchn2  21124  lspindp2l  21127  lspindp2  21128  lbsextlem2  21152  rnglidl1  21225  df2idl2  21250  2idlss  21255  rngqiprngimfo  21294  cnfldfun  21361  pzriprnglem3  21458  pzriprnglem4  21459  pzriprnglem7  21462  pzriprnglem8  21463  pzriprnglem9  21464  pzriprnglem12  21467  pzriprnglem14  21469  dsmmelbas  21714  frlmbas3  21751  lindsind2  21794  islindf4  21813  psrbagf  21893  evlslem4  22052  psdmul  22154  ply1bascl2  22189  cply1mul  22282  lply1binom  22296  matsubgcell  22417  matinvgcell  22418  matvscacell  22419  matepmcl  22445  matepm2cl  22446  scmatscm  22496  smatvscl  22507  marrepcl  22547  marepvcl  22552  mulmarep1el  22555  mulmarep1gsum1  22556  mulmarep1gsum2  22557  submabas  22561  m1detdiag  22580  mdetdiag  22582  m2detleib  22614  gsummatr01lem3  22640  gsummatr01  22642  smadiadetlem4  22652  slesolinv  22663  slesolinvbi  22664  slesolex  22665  cramerimplem2  22667  pmatcoe1fsupp  22684  mat2pmatbas  22709  mat2pmatmul  22714  mat2pmatlin  22718  decpmatmul  22755  monmatcollpw  22762  pm2mpf1  22782  pm2mpghm  22799  istps  22917  mretopd  23075  neiptopuni  23113  lpdifsn  23126  restcls  23164  perfopn  23168  pnfnei  23203  mnfnei  23204  lmss  23281  hauscmplem  23389  is2ndc  23429  2ndcdisj  23439  hausnlly  23476  txuni2  23548  ptpjpre1  23554  elpt  23555  dfac14  23601  xkococn  23643  fbasrn  23867  fin1aufil  23915  elfm2  23931  elfm3  23933  fbflim  23959  flffbas  23978  cnpflf2  23983  fclsbas  24004  efmndtmd  24084  tsmssubm  24126  iscusp2  24284  imasdsf1olem  24356  metustel  24533  metuel2  24548  isnghm  24706  opnreen  24815  iccpnfcnv  24929  ehleudisval  25404  ehl1eudis  25405  ehl2eudis  25407  minveclem3b  25413  ovoliunlem1  25487  ioombl1lem4  25546  subopnmbl  25589  vitalilem2  25594  vitalilem3  25595  mbfimaopnlem  25640  mbfimaopn2  25642  itg2l  25714  dvply1  26268  vieta1lem1  26294  vieta1lem2  26295  elaa  26300  taylthlem2  26357  abelthlem6  26419  abelthlem9  26423  sinq34lt0t  26491  ellogrn  26541  dvrelog  26619  ellogdm  26621  logtayl2  26644  cxpcn3lem  26729  cxpcn3  26730  1cubr  26824  atandm  26858  atanf  26862  reasinsin  26878  atans2  26913  dmarea  26939  xrlimcnp  26950  amgmlem  26971  ppiublem1  27183  lgsdir2lem2  27307  gausslemma2dlem1a  27346  lgsquadlem1  27361  lgsquadlem2  27362  2sqlem1  27398  rpvmasum2  27493  madeval2  27843  newval  27845  leftval  27859  rightval  27860  lltr  27872  madess  27876  oldssmade  27877  oldss  27880  lrold  27907  addsproplem2  27980  addsproplem4  27982  addsproplem6  27984  negsproplem4  28041  negsproplem6  28043  precsexlem10  28226  precsexlem11  28227  ltonold  28271  elnns  28350  elzs  28394  edgiedgb  29141  isuhgr  29147  isushgr  29148  isupgr  29171  isumgr  29182  umgredg  29225  umgrpredgv  29227  umgredgne  29232  umgredgnlp  29234  isuspgr  29239  isusgr  29240  ausgrusgri  29255  usgredgppr  29283  edgssv2  29285  uspgredg2vlem  29310  uspgredg2v  29311  ushgredgedg  29316  ushgredgedgloop  29318  griedg0ssusgr  29352  uhgrissubgr  29362  subumgredg2  29372  uhgrspansubgrlem  29377  umgrres1lem  29397  upgrres1  29400  nbgrcl  29422  nbuhgr  29430  nbuhgr2vtx1edgblem  29438  nbupgrres  29451  edgnbusgreu  29454  nbusgredgeu0  29455  nbusgrf1o0  29456  hashnbusgrnn0  29463  nbupgruvtxres  29494  cffldtocusgr  29534  cusgrfilem2  29543  vtxdg0v  29560  vtxduhgr0nedg  29579  uhgrvd00  29621  vtxdginducedm1  29630  finsumvtxdg2ssteplem4  29635  wlk1walk  29725  wlkp1lem6  29763  iswwlks  29922  wwlknllvtx  29932  wwlksonvtx  29941  wspthnonp  29945  wlkiswwlksupgr2  29963  wwlksnwwlksnon  30001  2pthon3v  30029  umgr2wlk  30035  elwwlks2s3  30037  wwlks2onv  30039  elwwlks2ons3im  30040  isclwwlk  30072  clwwlkccatlem  30077  clwlkclwwlk  30090  wwlksext2clwwlk  30145  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon1  30185  clwwlknon1nloop  30187  clwwlknon2x  30191  1pthon2v  30241  uhgr3cyclex  30270  isconngr  30277  isconngr1  30278  eucrctshift  30331  frgrnbnb  30381  frgrncvvdeqlem1  30387  frgrncvvdeqlem2  30388  frgrncvvdeqlem3  30389  frgrncvvdeqlem9  30395  fusgreghash2wspv  30423  extwwlkfab  30440  numclwwlk1lem2foa  30442  numclwwlk1lem2fo  30446  clwlknon2num  30456  numclwlk2lem2f1o  30467  numclwwlk5lem  30475  topnfbey  30557  isvclem  30666  isnvlem  30699  vsfval  30722  h2hlm  31069  hhcmpl  31289  hhcms  31292  elch0  31343  omlsilem  31491  h1de2ctlem  31644  elspansni  31647  nonbooli  31740  spansncvi  31741  adjeq  32024  cnlnssadj  32169  cnvbraval  32199  brabgaf  32698  2ndresdju  32741  fmptdF  32748  fmptcof2  32749  acunirnmpt  32751  acunirnmpt2  32752  ofpreima  32757  fcnvgreu  32764  fdifsuppconst  32781  1stpreima  32799  2ndpreima  32800  fz2ssnn0  32877  elxrge02  33010  ccatws1f1o  33030  gsumwrd2dccatlem  33158  psgnfzto1stlem  33181  cycpmgcl  33234  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrunlem1  33328  domnprodeq0  33357  nsgqusf1olem2  33497  nsgqusf1olem3  33498  prmidl0  33533  crngmxidl  33552  opprnsg  33567  rprmirredb  33615  zringfrac  33637  evl1deg2  33660  evl1deg3  33661  ply1degltel  33677  ply1degleel  33678  evlextv  33726  esplyfval3  33756  esplyindfv  33760  esplyfvn  33761  vietalem  33763  fldextrspunlsplem  33857  isconstr  33920  constrsuc  33922  constrconj  33929  submatres  33990  lmat22lem  34001  crefdf  34032  cmppcmp  34042  rspectopn  34051  prsdm  34098  prsrn  34099  xrge0iifcnv  34117  xrge0iifiso  34119  xrge0iifhom  34121  pnfneige0  34135  qqhre  34204  rrhre  34205  esumnul  34232  esumcvgsum  34272  ldgenpisyslem1  34347  measvuni  34398  cntnevol  34412  dya2iocnrect  34465  sibf0  34518  oddpwdc  34538  eulerpartlemd  34550  eulerpartgbij  34556  eulerpartlemgh  34562  isrrvv  34627  coinfliprv  34667  ballotlem7  34720  signswch  34745  hashreprin  34804  chtvalz  34813  circlemethhgt  34827  hgt750lemb  34840  tgoldbachgt  34847  bnj23  34901  bnj158  34912  bnj168  34913  bnj1138  34971  bnj1143  34972  bnj1454  35024  bnj110  35040  bnj882  35108  bnj893  35110  bnj916  35115  bnj970  35129  bnj983  35133  bnj984  35134  bnj1137  35177  bnj1174  35185  bnj1388  35215  bnj1398  35216  r1wf  35277  onvf1odlem4  35334  loop1cycl  35365  subfacp1lem5  35412  satfv1  35591  satfrnmapom  35598  satf0op  35605  satf0n0  35606  fmlafvel  35613  fmlaomn0  35618  fmlan0  35619  satffunlem2lem2  35634  satfv0fvfmla0  35641  satefvfmla0  35646  mrsub0  35744  mrsubccat  35746  mrsubcn  35747  elmrsubrn  35748  msubco  35759  msubvrs  35788  elmthm  35804  mthmblem  35808  ellcsrspsn  35869  elrn3  35990  dfon2lem7  36015  brsset  36115  eltrans  36117  elfix  36129  ellimits  36136  elfuns  36141  elsingles  36144  fvtransport  36260  brcolinear2  36286  fvray  36369  linedegen  36371  fvline  36372  ellines  36380  fwddifn0  36392  elhf  36402  hfninf  36414  rmoeqi  36415  rmoeqbii  36416  reueqi  36417  reueqbii  36418  rabeqbii  36422  iuneq12i  36423  iineq1i  36424  iineq12i  36425  riotaeqbii  36426  ixpeq1i  36428  itgeq12i  36434  cbvprodvw2  36475  fnessref  36585  ttctr  36721  bj-ififc  36893  bj-csbsnlem  37256  bj-elgab  37292  currysetlem1  37300  bj-eltag  37330  bj-sngltag  37336  bj-projun  37347  bj-velpwALT  37406  bj-0nelmpt  37474  bj-opelidres  37521  bj-inftyexpitaudisj  37565  bj-elccinfty  37574  f1omptsnlem  37698  icoreelrnab  37716  relowlpssretop  37726  rdgssun  37740  exrecfnlem  37741  finxpnom  37763  uncov  37968  tan2h  37979  ptrecube  37987  poimirlem25  38012  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  cnambfre  38035  ftc1cnnc  38059  sdclem2  38109  sdclem1  38110  fdc  38112  caushft  38128  issmgrpOLD  38230  ismndo  38239  isrngo  38264  isdivrngo  38317  csbcom2fi  38495  elecALTV  38638  brrabga  38708  eldmxrncnvepres  38801  eldmxrncnvepres2  38802  elrels2  38808  blockadjliftmap  38825  dfpre  38843  eupre  38861  eldmcoss  38915  coss0  38936  petseq  39343  dath  40228  diclspsn  41686  dvh4dimlem  41935  dvh2dim  41937  dvh3dim3N  41941  lcfrvalsnN  42033  mapdh6eN  42232  mapdh7dN  42242  mapdh8b  42272  hdmap1l6e  42306  lcmfunnnd  42497  3factsumint1  42506  primrootsunit1  42582  primrootscoprmpow  42584  aks6d1c2lem4  42612  sticksstones2  42632  sticksstones3  42633  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem2  42656  aks6d1c6lem3  42657  redvmptabs  42837  readvrec2  42838  readvrec  42839  frlmfielbas  42990  mhpind  43044  pellex  43280  rmspecnonsq  43352  islmodfg  43514  aaitgo  43607  areaquad  43661  ordeldif1o  43705  naddwordnexlem4  43846  fpwfvss  43856  finona1cl  43897  elcnvcnvintab  44026  elnonrel  44029  elcnvcnvlem  44043  cnvcnvintabd  44044  brfvrcld2  44136  grur1cld  44676  dvgrat  44756  cvgdvgrat  44757  radcnvrat  44758  nznngen  44760  uzmptshftfval  44790  binomcxplemcvg  44798  binomcxplemnotnn0  44800  tpid3gVD  45285  en3lplem2VD  45287  orbitclmpt  45402  wfaxrep  45438  wfaxsep  45439  wfaxpow  45441  wfaxpr  45442  wfaxun  45443  wfac8prim  45446  brpermmodelcnv  45448  nregmodellem  45460  iuneq1i  45532  rexanuz3  45543  eliuniin  45546  eliuniin2  45567  disjinfi  45639  iuneqfzuzlem  45779  allbutfi  45837  eluzelz2  45846  uz0  45855  uzublem  45873  uzid3  45878  elicores  45978  uzinico  46004  climsuselem1  46052  climsuse  46053  islptre  46064  fnlimfvre  46117  limsupresico  46143  limsupvaluz  46151  limsupubuzlem  46155  limsupequzmptlem  46171  liminfresico  46214  cnrefiisplem  46272  stoweidlem14  46457  stoweidlem39  46482  stoweidlem48  46491  stoweidlem51  46494  stoweidlem59  46502  stoweidlem62  46505  wallispilem3  46510  fourierdlem42  46592  fourierdlem62  46611  fourierdlem80  46629  fourierdlem103  46652  fourierdlem104  46653  etransclem26  46703  rrxsnicc  46743  ioorrnopn  46748  ioorrnopnxr  46750  sge00  46819  sge0fodjrnlem  46859  sge0isum  46870  sge0seq  46889  meadjiunlem  46908  carageneld  46945  volicorescl  46996  hoidmv1lelem1  47034  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem3  47040  ovnhoilem2  47045  hoiqssbllem2  47066  opnvonmbllem2  47076  ovolval4lem1  47092  iinhoiicc  47117  vonioolem1  47123  smflimlem1  47214  smflimlem2  47215  smflim  47220  nsssmfmbf  47222  smfresal  47231  smfrec  47232  smfdiv  47240  smfpimbor1lem2  47242  smflim2  47249  smflimmpt  47253  smfinflem  47260  smflimsuplem1  47263  smflimsuplem2  47264  smflimsuplem3  47265  smflimsuplem5  47267  smflimsuplem6  47268  smflimsup  47271  smflimsupmpt  47272  smfliminfmpt  47275  chnerlem1  47327  chnerlem2  47328  tannpoly  47353  sinnpoly  47354  fcores  47530  ndmaovcl  47666  ndmaovcom  47668  ndmaovass  47669  ndmaovdistr  47670  dfatco  47719  otiunsndisjX  47742  fvmptrabdm  47756  ceilhalfelfzo1  47797  modmknepk  47831  elsetpreimafvb  47859  sprsymrelfolem2  47968  sprsymrelf  47970  sprsymrelf1  47971  prpair  47976  prproropf1olem0  47977  paireqne  47986  fmtno4prmfac  48050  dfodd5  48151  sbgoldbo  48278  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  clnbgrcl  48312  clnbgredg  48331  sclnbgrel  48338  isubgredg  48357  uhgrimedgi  48381  isuspgrim0  48385  isuspgrimlem  48386  gricushgr  48408  clnbgrgrimlem  48424  grimedg  48426  usgrgrtrirex  48441  stgrnbgr0  48455  isubgr3stgrlem3  48459  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  isubgr3stgrlem7  48463  uspgrlimlem2  48480  uspgrlimlem3  48481  grlimedgclnbgr  48486  grlimprclnbgr  48487  grlimprclnbgrvtx  48490  grlimgrtrilem2  48493  usgrexmpl2trifr  48528  gpgvtxel  48538  gpgedgel  48541  gpgusgralem  48547  gpg5order  48551  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgnbgrvtx0  48565  gpgnbgrvtx1  48566  gpg5nbgrvtx03star  48571  gpg5nbgr3star  48572  gpgvtxdg3  48573  gpg5gricstgr3  48581  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem8  48593  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615  pgnbgreunbgr  48616  uspgrsprf  48637  uspgrsprf1  48638  uspgrsprfo  48639  ply1sclrmsm  48875  lcoop  48902  lincfsuppcl  48904  linccl  48905  lincvalsng  48907  lincvalpr  48909  lincvalsc0  48912  linc0scn0  48914  lincdifsn  48915  linc1  48916  lincsum  48920  lincscm  48921  lspsslco  48928  snlindsntor  48962  lincresunit3lem2  48971  ldepsnlinclem1  48996  ldepsnlinclem2  48997  prelrrx2  49204  prelrrx2b  49205  rrx2xpref1o  49209  rrx2plord  49211  rrx2linesl  49234  sectrcl  49512  invrcl  49514  initopropdlemlem  49729  initopropd  49733  termopropd  49734  zeroopropd  49735  oppcthin  49928  indthinc  49952  prsthinc  49954  elpglem3  50203