Theorem eleq2i 2825

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  eleq12i  2826  eleqtri  2831  eleq2s  2851  hbxfreq  2864  nfceqi  2900  raleqbii  3338  rexeqbii  3339  rabeqi  3445  rabrabi  3450  reqabi  3454  elab2g  3670  elrabf  3679  elrab3t  3682  elrab2  3686  cbvsbcw  3811  cbvsbcvw  3812  cbvsbc  3813  elin2  4197  elsymdif  4247  noel  4330  noelOLD  4331  eltpg  4689  elunirab  4924  elintrab  4964  disjxiun  5145  exss  5463  otiunsndisj  5520  brabsb  5531  brabga  5534  epelg  5581  pofun  5606  elxp  5699  opeliunxp  5743  bropaex12  5767  brab2a  5769  elcnv  5876  dmopabelb  5916  elrnmptg  5958  elres  6020  elrid  6045  rninxp  6178  elid  6198  elsuci  6431  elsucg  6432  elsuc2g  6433  elfv  6889  0fv  6935  opabiota  6974  dffv2  6986  fvopab3g  6993  fvmptex  7012  fvopab5  7030  fvn0ssdmfun  7076  fveqressseq  7081  f0cli  7099  fmptco  7129  fvrnressn  7161  funfvima  7234  elunirnALT  7253  fliftel  7308  eloprabga  7518  eloprabgaOLD  7519  elrnmpo  7547  ovid  7551  offval  7681  sucexeloniOLD  7800  suceloniOLD  7802  1st2val  8005  2nd2val  8006  bropopvvv  8078  bropfvvvv  8080  fsplit  8105  xporderlem  8115  frpoins3xpg  8128  frpoins3xp3g  8129  brtpos2  8219  frrlem8  8280  frrlem9  8281  frrlem10  8282  fprresex  8297  wfrdmclOLD  8319  wfrfunOLD  8321  wfrlem12OLD  8322  wfrlem17OLD  8327  wfr2OLD  8330  issmo  8350  smores3  8355  tfrlem7  8385  tfrlem9  8387  tfrlem9a  8388  tfr2b  8398  tfr2  8400  rdgsuc  8426  frsucmptn  8441  tz7.48-2  8444  el1o  8497  ord2eln012  8499  dif1o  8502  ondif2  8504  oawordeulem  8556  elecg  8748  brecop  8806  erovlem  8809  eceqoveq  8818  mapsncnv  8889  mptelixpg  8931  brsdom  8973  isfi  8974  enssdom  8975  brdom2  8980  xpcomco  9064  brsdom2  9099  en3lplem2  9610  cnfcom2lem  9698  brttrcl2  9711  ttrcltr  9713  rnttrcl  9719  epfrs  9728  r1limg  9768  r1ord  9777  r1ord3  9779  tz9.12lem3  9786  rankvaln  9796  r1elss  9803  rankpwi  9820  ssrankr1  9832  r1val3  9835  r1pw  9842  rankr1b  9861  djur  9916  djuunxp  9918  eldju2ndl  9921  eldju2ndr  9922  isnum2  9942  cardprclem  9976  infxpenlem  10010  alephcard  10067  alephnbtwn  10068  alephnbtwn2  10069  alephord2  10073  alephsdom  10083  dfac3  10118  dfac5lem2  10121  dfac5lem3  10122  dfac5lem5  10124  pwsdompw  10201  cfub  10246  cardcf  10249  cflecard  10250  cfle  10251  cflim2  10260  cofsmo  10266  cfidm  10272  isfin3  10293  isfin5  10296  isfin6  10297  sdom2en01  10299  fin23lem26  10322  fin23lem30  10339  isf32lem5  10354  itunitc1  10417  ituniiun  10419  axdc3lem3  10449  axcclem  10454  axdclem  10516  iunfo  10536  iundom2g  10537  cardidg  10545  konigthlem  10565  alephadd  10574  alephreg  10579  pwcfsdom  10580  cfpwsdom  10581  elgch  10619  fpwwe2lem11  10638  canth4  10644  wunex2  10735  r1tskina  10779  elni  10873  nlt1pi  10903  adderpq  10953  mulerpq  10954  recmulnq  10961  addsrpr  11072  mulsrpr  11073  opelcn  11126  opelreal  11127  elreal  11128  elreal2  11129  0ncn  11130  addcnsr  11132  mulcnsr  11133  xrlenlt  11283  elnn0  12478  elnnne0  12490  un0addcl  12509  un0mulcl  12510  elxnn0  12550  uztrn2  12845  elnnuz  12870  elnn0uz  12871  elq  12938  elxr  13100  elfzm1b  13583  elfz0lmr  13751  uzrdgfni  13927  fzennn  13937  ser0  14024  hash2pwpr  14441  iswrd  14470  pfxccatpfx1  14690  s3iunsndisj  14919  sumz  15672  sumss  15674  fsumcvg3  15679  abscvgcvg  15769  isumshft  15789  prodf1  15841  zprod  15885  prod1  15892  prodss  15895  prodsn  15910  prodsnf  15912  bpolydiflem  16002  bpoly2  16005  bpoly3  16006  bpoly4  16007  ruclem6  16182  divides  16203  dvdsflip  16264  pwp1fsum  16338  sadc0  16399  eulerthlem2  16719  prm23lt5  16751  4sqlem2  16886  4sqlem12  16893  vdwpc  16917  xpscf  17515  cidpropd  17658  oppcsect  17729  funcpropd  17855  natpropd  17933  dfinito2  17957  dftermo2  17958  initoeu2lem0  17967  arwhoma  17999  eldmcoa  18019  pospo  18302  psss  18537  ismgmn0  18567  gsumpropd2lem  18604  elefmndbas  18790  smndex1basss  18822  smndex1mgm  18824  pwmnd  18854  dfgrp2e  18884  mulgfval  18988  eqg0subg  19111  cycsubmel  19115  ghmeqker  19157  elcntr  19235  cntri  19237  cntzsgrpcl  19239  oppgsubg  19271  fvcosymgeq  19338  symgfixels  19343  pmtrfrn  19367  efgsfo  19648  efgrelexlemb  19659  lt6abl  19804  dmdprd  19909  dprdval  19914  dprdw  19921  srgbinomlem4  20123  isnirred  20311  isrhm  20369  issrng  20601  lspexchn2  20889  lspindp2l  20892  lspindp2  20893  lbsextlem2  20917  2idlss  21017  rnglidl1  21033  rngqiprngimfo  21060  cnfldfun  21156  pzriprnglem3  21252  pzriprnglem4  21253  pzriprnglem7  21256  pzriprnglem8  21257  pzriprnglem9  21258  pzriprnglem12  21261  pzriprnglem14  21263  dsmmelbas  21513  frlmbas3  21550  lindsind2  21593  islindf4  21612  psrbagf  21690  evlslem4  21856  ply1bascl2  21947  cply1mul  22038  lply1binom  22050  matsubgcell  22156  matinvgcell  22157  matvscacell  22158  matepmcl  22184  matepm2cl  22185  scmatscm  22235  smatvscl  22246  marrepcl  22286  marepvcl  22291  mulmarep1el  22294  mulmarep1gsum1  22295  mulmarep1gsum2  22296  submabas  22300  m1detdiag  22319  mdetdiag  22321  m2detleib  22353  gsummatr01lem3  22379  gsummatr01  22381  smadiadetlem4  22391  slesolinv  22402  slesolinvbi  22403  slesolex  22404  cramerimplem2  22406  pmatcoe1fsupp  22423  mat2pmatbas  22448  mat2pmatmul  22453  mat2pmatlin  22457  decpmatmul  22494  monmatcollpw  22501  pm2mpf1  22521  pm2mpghm  22538  istps  22656  mretopd  22816  neiptopuni  22854  lpdifsn  22867  restcls  22905  perfopn  22909  pnfnei  22944  mnfnei  22945  lmss  23022  hauscmplem  23130  is2ndc  23170  2ndcdisj  23180  hausnlly  23217  txuni2  23289  ptpjpre1  23295  elpt  23296  dfac14  23342  xkococn  23384  fbasrn  23608  fin1aufil  23656  elfm2  23672  elfm3  23674  fbflim  23700  flffbas  23719  cnpflf2  23724  fclsbas  23745  efmndtmd  23825  tsmssubm  23867  iscusp2  24027  imasdsf1olem  24099  metustel  24279  metuel2  24294  isnghm  24460  opnreen  24567  iccpnfcnv  24684  ehleudisval  25160  ehl1eudis  25161  ehl2eudis  25163  minveclem3b  25169  ovoliunlem1  25243  ioombl1lem4  25302  subopnmbl  25345  vitalilem2  25350  vitalilem3  25351  mbfimaopnlem  25396  mbfimaopn2  25398  itg2l  25471  dvply1  26021  vieta1lem1  26047  vieta1lem2  26048  elaa  26053  taylthlem2  26110  abelthlem6  26172  abelthlem9  26176  sinq34lt0t  26243  ellogrn  26292  dvrelog  26369  ellogdm  26371  logtayl2  26394  cxpcn3lem  26479  cxpcn3  26480  1cubr  26571  atandm  26605  atanf  26609  reasinsin  26625  atans2  26660  dmarea  26686  xrlimcnp  26697  amgmlem  26718  ppiublem1  26929  lgsdir2lem2  27053  gausslemma2dlem1a  27092  lgsquadlem1  27107  lgsquadlem2  27108  2sqlem1  27144  rpvmasum2  27239  madeval2  27573  newval  27575  leftval  27583  rightval  27584  lltropt  27592  madess  27596  oldssmade  27597  lrold  27616  addsproplem2  27680  addsproplem4  27682  addsproplem6  27684  negsproplem4  27732  negsproplem6  27734  precsexlem10  27889  precsexlem11  27890  sltonold  27914  edgiedgb  28569  isuhgr  28575  isushgr  28576  isupgr  28599  isumgr  28610  umgredg  28653  umgrpredgv  28655  umgredgne  28660  umgredgnlp  28662  isuspgr  28667  isusgr  28668  ausgrusgri  28683  usgredgppr  28708  edgssv2  28710  uspgredg2vlem  28735  uspgredg2v  28736  ushgredgedg  28741  ushgredgedgloop  28743  griedg0ssusgr  28777  uhgrissubgr  28787  subumgredg2  28797  uhgrspansubgrlem  28802  umgrres1lem  28822  upgrres1  28825  nbgrcl  28847  nbuhgr  28855  nbuhgr2vtx1edgblem  28863  nbupgrres  28876  edgnbusgreu  28879  nbusgredgeu0  28880  nbusgrf1o0  28881  hashnbusgrnn0  28888  nbupgruvtxres  28919  cffldtocusgr  28959  cusgrfilem2  28968  vtxdg0v  28985  vtxduhgr0nedg  29004  uhgrvd00  29046  vtxdginducedm1  29055  finsumvtxdg2ssteplem4  29060  wlk1walk  29151  wlkp1lem6  29190  iswwlks  29345  wwlknllvtx  29355  wwlksonvtx  29364  wspthnonp  29368  wlkiswwlksupgr2  29386  wwlksnwwlksnon  29424  2pthon3v  29452  umgr2wlk  29458  elwwlks2s3  29460  wwlks2onv  29462  elwwlks2ons3im  29463  isclwwlk  29492  clwwlkccatlem  29497  clwlkclwwlk  29510  wwlksext2clwwlk  29565  hashecclwwlkn1  29585  umgrhashecclwwlk  29586  clwwlknon1  29605  clwwlknon1nloop  29607  clwwlknon2x  29611  1pthon2v  29661  uhgr3cyclex  29690  isconngr  29697  isconngr1  29698  eucrctshift  29751  frgrnbnb  29801  frgrncvvdeqlem1  29807  frgrncvvdeqlem2  29808  frgrncvvdeqlem3  29809  frgrncvvdeqlem9  29815  fusgreghash2wspv  29843  extwwlkfab  29860  numclwwlk1lem2foa  29862  numclwwlk1lem2fo  29866  clwlknon2num  29876  numclwlk2lem2f1o  29887  numclwwlk5lem  29895  topnfbey  29977  isvclem  30085  isnvlem  30118  vsfval  30141  h2hlm  30488  hhcmpl  30708  hhcms  30711  elch0  30762  omlsilem  30910  h1de2ctlem  31063  elspansni  31066  nonbooli  31159  spansncvi  31160  adjeq  31443  cnlnssadj  31588  cnvbraval  31618  brabgaf  32092  elimampt  32117  2ndresdju  32129  fmptdF  32136  fmptcof2  32137  acunirnmpt  32139  acunirnmpt2  32140  ofpreima  32145  fcnvgreu  32153  fdifsuppconst  32166  1stpreima  32183  2ndpreima  32184  fz2ssnn0  32251  elxrge02  32353  psgnfzto1stlem  32517  cycpmgcl  32570  nsgqusf1olem2  32787  nsgqusf1olem3  32788  prmidl0  32831  crngmxidl  32847  opprnsg  32860  ply1degltel  32928  ply1degleel  32929  submatres  33072  lmat22lem  33083  crefdf  33114  cmppcmp  33124  rspectopn  33133  prsdm  33180  prsrn  33181  xrge0iifcnv  33199  xrge0iifiso  33201  xrge0iifhom  33203  pnfneige0  33217  qqhre  33286  rrhre  33287  esumnul  33332  esumcvgsum  33372  ldgenpisyslem1  33447  measvuni  33498  cntnevol  33512  dya2iocnrect  33566  sibf0  33619  oddpwdc  33639  eulerpartlemd  33651  eulerpartgbij  33657  eulerpartlemgh  33663  isrrvv  33728  coinfliprv  33767  ballotlem7  33820  signswch  33858  hashreprin  33918  chtvalz  33927  circlemethhgt  33941  hgt750lemb  33954  tgoldbachgt  33961  bnj23  34015  bnj158  34026  bnj168  34027  bnj1138  34085  bnj1143  34087  bnj1454  34139  bnj110  34155  bnj882  34223  bnj893  34225  bnj916  34230  bnj970  34244  bnj983  34248  bnj984  34249  bnj1137  34292  bnj1174  34300  bnj1388  34330  bnj1398  34331  loop1cycl  34414  subfacp1lem5  34461  satfv1  34640  satfrnmapom  34647  satf0op  34654  satf0n0  34655  fmlafvel  34662  fmlaomn0  34667  fmlan0  34668  satffunlem2lem2  34683  satfv0fvfmla0  34690  satefvfmla0  34695  mrsub0  34793  mrsubccat  34795  mrsubcn  34796  elmrsubrn  34797  msubco  34808  msubvrs  34837  elmthm  34853  mthmblem  34857  elrn3  35024  dfon2lem7  35053  brsset  35153  eltrans  35155  elfix  35167  ellimits  35174  elfuns  35179  elsingles  35182  fvtransport  35296  brcolinear2  35322  fvray  35405  linedegen  35407  fvline  35408  ellines  35416  fwddifn0  35428  elhf  35438  hfninf  35450  gg-cnfldfun  35483  gg-cffldtocusgr  35485  fnessref  35545  bj-ififc  35762  bj-csbsnlem  36086  bj-elgab  36122  currysetlem1  36131  bj-eltag  36161  bj-sngltag  36167  bj-projun  36178  bj-velpwALT  36237  bj-0nelmpt  36300  bj-opelidres  36345  bj-inftyexpitaudisj  36389  bj-elccinfty  36398  f1omptsnlem  36520  icoreelrnab  36538  relowlpssretop  36548  rdgssun  36562  exrecfnlem  36563  finxpnom  36585  uncov  36772  tan2h  36783  ptrecube  36791  poimirlem25  36816  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimirlem32  36823  cnambfre  36839  ftc1cnnc  36863  sdclem2  36913  sdclem1  36914  fdc  36916  caushft  36932  issmgrpOLD  37034  ismndo  37043  isrngo  37068  isdivrngo  37121  csbcom2fi  37299  elecALTV  37437  brrabga  37513  eldmcoss  37631  coss0  37652  elrels2  37659  dath  38910  diclspsn  40368  dvh4dimlem  40617  dvh2dim  40619  dvh3dim3N  40623  lcfrvalsnN  40715  mapdh6eN  40914  mapdh7dN  40924  mapdh8b  40954  hdmap1l6e  40988  lcmfunnnd  41183  3factsumint1  41192  sticksstones2  41269  sticksstones3  41270  sticksstones10  41277  sticksstones12a  41279  sticksstones12  41280  frlmfielbas  41380  mhpind  41468  elab2gw  41711  pellex  41875  rmspecnonsq  41947  islmodfg  42113  aaitgo  42206  areaquad  42267  ordeldif1o  42312  naddwordnexlem4  42454  fpwfvss  42465  finona1cl  42506  elcnvcnvintab  42635  elnonrel  42638  elcnvcnvlem  42652  cnvcnvintabd  42653  brfvrcld2  42745  grur1cld  43293  dvgrat  43373  cvgdvgrat  43374  radcnvrat  43375  nznngen  43377  uzmptshftfval  43407  binomcxplemcvg  43415  binomcxplemnotnn0  43417  tpid3gVD  43905  en3lplem2VD  43907  rexanuz3  44087  eliuniin  44090  eliuniin2  44111  disjinfi  44190  fsneq  44204  iuneqfzuzlem  44343  allbutfi  44402  eluzelz2  44412  uz0  44421  uzublem  44439  uzid3  44444  elicores  44545  uzinico  44572  climsuselem1  44622  climsuse  44623  islptre  44634  fnlimfvre  44689  limsupresico  44715  limsupvaluz  44723  limsupubuzlem  44727  limsupequzmptlem  44743  liminfresico  44786  cnrefiisplem  44844  stoweidlem14  45029  stoweidlem39  45054  stoweidlem48  45063  stoweidlem51  45066  stoweidlem59  45074  stoweidlem62  45077  wallispilem3  45082  fourierdlem42  45164  fourierdlem62  45183  fourierdlem80  45201  fourierdlem103  45224  fourierdlem104  45225  etransclem26  45275  rrxsnicc  45315  ioorrnopn  45320  ioorrnopnxr  45322  sge00  45391  sge0fodjrnlem  45431  sge0isum  45442  sge0seq  45461  meadjiunlem  45480  carageneld  45517  volicorescl  45568  hoidmv1lelem1  45606  hoidmv1le  45609  hoidmvlelem1  45610  hoidmvlelem3  45612  ovnhoilem2  45617  hoiqssbllem2  45638  opnvonmbllem2  45648  ovolval4lem1  45664  iinhoiicc  45689  vonioolem1  45695  smflimlem1  45786  smflimlem2  45787  smflim  45792  nsssmfmbf  45794  smfresal  45803  smfrec  45804  smfdiv  45812  smfpimbor1lem2  45814  smflim2  45821  smflimmpt  45825  smfinflem  45832  smfinfmpt  45834  smflimsuplem1  45835  smflimsuplem2  45836  smflimsuplem3  45837  smflimsuplem5  45839  smflimsuplem6  45840  smflimsup  45843  smflimsupmpt  45844  smfliminfmpt  45847  fcores  46076  ndmaovcl  46210  ndmaovcom  46212  ndmaovass  46213  ndmaovdistr  46214  dfatco  46263  otiunsndisjX  46286  fvmptrabdm  46300  elsetpreimafvb  46351  sprsymrelfolem2  46460  sprsymrelf  46462  sprsymrelf1  46463  prpair  46468  prproropf1olem0  46469  paireqne  46478  fmtno4prmfac  46539  dfodd5  46627  sbgoldbo  46754  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  isomushgr  46793  isomuspgrlem2c  46797  uspgrsprf  46823  uspgrsprf1  46824  uspgrsprfo  46825  opeliun2xp  47097  ply1sclrmsm  47152  lcoop  47180  lincfsuppcl  47182  linccl  47183  lincvalsng  47185  lincvalpr  47187  lincvalsc0  47190  linc0scn0  47192  lincdifsn  47193  linc1  47194  lincsum  47198  lincscm  47199  lspsslco  47206  snlindsntor  47240  lincresunit3lem2  47249  ldepsnlinclem1  47274  ldepsnlinclem2  47275  prelrrx2  47487  prelrrx2b  47488  rrx2xpref1o  47492  rrx2plord  47494  rrx2linesl  47517  oppcthin  47747  indthinc  47760  prsthinc  47762  elpglem3  47846