Theorem eleq2i 2826

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  eleq12i  2827  eleqtri  2832  eleq2s  2852  hbxfreq  2865  nfceqi  2895  raleqbii  3323  rexeqbii  3324  rabeqi  3429  rabrabi  3435  reqabi  3439  elab2gw  3657  elab2g  3659  elrabf  3667  elrab3t  3670  elrab2  3674  cbvsbcw  3798  cbvsbcvw  3799  cbvsbc  3800  elin2  4178  elsymdif  4233  noel  4313  eltpg  4662  elunirab  4898  elintrab  4936  disjxiun  5116  exss  5438  otiunsndisj  5495  brabsb  5506  brabga  5509  epelg  5554  pofun  5579  elxp  5677  opeliunxp  5721  opeliun2xp  5722  bropaex12  5746  brab2a  5748  elcnv  5856  dmopabelb  5896  elrnmptg  5941  elres  6007  elimampt  6030  elrid  6033  rninxp  6168  elid  6188  elsuci  6420  elsucg  6421  elsuc2g  6422  elfv  6873  0fv  6919  opabiota  6960  dffv2  6973  fvopab3g  6980  fvmptex  6999  fvopab5  7018  fvn0ssdmfun  7063  fveqressseq  7068  f0cli  7087  fmptco  7118  fvrnressn  7150  funfvima  7221  elunirnALT  7243  fliftel  7301  eloprabga  7514  elrnmpo  7541  elimampo  7542  ovid  7546  offval  7678  sucexeloniOLD  7802  suceloniOLD  7804  1st2val  8014  2nd2val  8015  bropopvvv  8087  bropfvvvv  8089  fsplit  8114  xporderlem  8124  frpoins3xpg  8137  frpoins3xp3g  8138  brtpos2  8229  frrlem8  8290  frrlem9  8291  frrlem10  8292  fprresex  8307  wfrdmclOLD  8329  wfrfunOLD  8331  wfrlem12OLD  8332  wfrlem17OLD  8337  wfr2OLD  8340  issmo  8360  smores3  8365  tfrlem7  8395  tfrlem9  8397  tfrlem9a  8398  tfr2b  8408  tfr2  8410  rdgsuc  8436  frsucmptn  8451  tz7.48-2  8454  el1o  8505  ord2eln012  8507  dif1o  8510  ondif2  8512  oawordeulem  8564  elecg  8761  brecop  8822  erovlem  8825  eceqoveq  8834  mapsncnv  8905  mptelixpg  8947  brsdom  8987  isfi  8988  enssdom  8989  brdom2  8994  xpcomco  9074  brsdom2  9109  en3lplem2  9625  cnfcom2lem  9713  brttrcl2  9726  ttrcltr  9728  rnttrcl  9734  epfrs  9743  r1limg  9783  r1ord  9792  r1ord3  9794  tz9.12lem3  9801  rankvaln  9811  r1elss  9818  rankpwi  9835  ssrankr1  9847  r1val3  9850  r1pw  9857  rankr1b  9876  djur  9931  djuunxp  9933  eldju2ndl  9936  eldju2ndr  9937  isnum2  9957  cardprclem  9991  infxpenlem  10025  alephcard  10082  alephnbtwn  10083  alephnbtwn2  10084  alephord2  10088  alephsdom  10098  dfac3  10133  dfac5lem2  10136  dfac5lem3  10137  dfac5lem5  10139  pwsdompw  10215  cfub  10261  cardcf  10264  cflecard  10265  cfle  10266  cflim2  10275  cofsmo  10281  cfidm  10287  isfin3  10308  isfin5  10311  isfin6  10312  sdom2en01  10314  fin23lem26  10337  fin23lem30  10354  isf32lem5  10369  itunitc1  10432  ituniiun  10434  axdc3lem3  10464  axcclem  10469  axdclem  10531  iunfo  10551  iundom2g  10552  cardidg  10560  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  11298  elnn0  12501  elnnne0  12513  un0addcl  12532  un0mulcl  12533  elxnn0  12574  uztrn2  12869  elnnuz  12894  elnn0uz  12895  elq  12964  elxr  13130  elfzm1b  13617  elfz0lmr  13796  uzrdgfni  13974  fzennn  13984  ser0  14070  hash2pwpr  14492  iswrd  14531  pfxccatpfx1  14752  s3iunsndisj  14985  sumz  15736  sumss  15738  fsumcvg3  15743  abscvgcvg  15833  isumshft  15853  prodf1  15905  prodeq1i  15930  zprod  15951  prod1  15958  prodss  15961  prodsn  15976  prodsnf  15978  bpolydiflem  16068  bpoly2  16071  bpoly3  16072  bpoly4  16073  ruclem6  16251  divides  16272  dvdsflip  16334  pwp1fsum  16408  sadc0  16471  eulerthlem2  16799  prm23lt5  16832  4sqlem2  16967  4sqlem12  16974  vdwpc  16998  xpscf  17577  cidpropd  17720  oppcsect  17789  funcpropd  17913  natpropd  17990  dfinito2  18014  dftermo2  18015  initoeu2lem0  18024  arwhoma  18056  eldmcoa  18076  pospo  18353  psss  18588  ismgmn0  18618  gsumpropd2lem  18655  elefmndbas  18849  smndex1basss  18881  smndex1mgm  18883  pwmnd  18913  dfgrp2e  18944  mulgfval  19050  eqg0subg  19177  cycsubmel  19181  ghmeqker  19224  elcntr  19311  cntri  19313  cntzsgrpcl  19315  oppgsubg  19344  fvcosymgeq  19408  symgfixels  19413  pmtrfrn  19437  efgsfo  19718  efgrelexlemb  19729  lt6abl  19874  dmdprd  19979  dprdval  19984  dprdw  19991  srgbinomlem4  20187  isnirred  20378  isrhm  20436  issrng  20802  lspexchn2  21090  lspindp2l  21093  lspindp2  21094  lbsextlem2  21118  rnglidl1  21191  df2idl2  21216  2idlss  21221  rngqiprngimfo  21260  cnfldfun  21327  cnfldfunOLD  21340  pzriprnglem3  21442  pzriprnglem4  21443  pzriprnglem7  21446  pzriprnglem8  21447  pzriprnglem9  21448  pzriprnglem12  21451  pzriprnglem14  21453  dsmmelbas  21697  frlmbas3  21734  lindsind2  21777  islindf4  21796  psrbagf  21876  evlslem4  22032  psdmul  22102  ply1bascl2  22138  cply1mul  22232  lply1binom  22246  matsubgcell  22370  matinvgcell  22371  matvscacell  22372  matepmcl  22398  matepm2cl  22399  scmatscm  22449  smatvscl  22460  marrepcl  22500  marepvcl  22505  mulmarep1el  22508  mulmarep1gsum1  22509  mulmarep1gsum2  22510  submabas  22514  m1detdiag  22533  mdetdiag  22535  m2detleib  22567  gsummatr01lem3  22593  gsummatr01  22595  smadiadetlem4  22605  slesolinv  22616  slesolinvbi  22617  slesolex  22618  cramerimplem2  22620  pmatcoe1fsupp  22637  mat2pmatbas  22662  mat2pmatmul  22667  mat2pmatlin  22671  decpmatmul  22708  monmatcollpw  22715  pm2mpf1  22735  pm2mpghm  22752  istps  22870  mretopd  23028  neiptopuni  23066  lpdifsn  23079  restcls  23117  perfopn  23121  pnfnei  23156  mnfnei  23157  lmss  23234  hauscmplem  23342  is2ndc  23382  2ndcdisj  23392  hausnlly  23429  txuni2  23501  ptpjpre1  23507  elpt  23508  dfac14  23554  xkococn  23596  fbasrn  23820  fin1aufil  23868  elfm2  23884  elfm3  23886  fbflim  23912  flffbas  23931  cnpflf2  23936  fclsbas  23957  efmndtmd  24037  tsmssubm  24079  iscusp2  24238  imasdsf1olem  24310  metustel  24487  metuel2  24502  isnghm  24660  opnreen  24769  iccpnfcnv  24891  ehleudisval  25369  ehl1eudis  25370  ehl2eudis  25372  minveclem3b  25378  ovoliunlem1  25453  ioombl1lem4  25512  subopnmbl  25555  vitalilem2  25560  vitalilem3  25561  mbfimaopnlem  25606  mbfimaopn2  25608  itg2l  25680  dvply1  26241  vieta1lem1  26268  vieta1lem2  26269  elaa  26274  taylthlem2  26332  taylthlem2OLD  26333  abelthlem6  26396  abelthlem9  26400  sinq34lt0t  26468  ellogrn  26518  dvrelog  26596  ellogdm  26598  logtayl2  26621  cxpcn3lem  26707  cxpcn3  26708  1cubr  26802  atandm  26836  atanf  26840  reasinsin  26856  atans2  26891  dmarea  26917  xrlimcnp  26928  amgmlem  26950  ppiublem1  27163  lgsdir2lem2  27287  gausslemma2dlem1a  27326  lgsquadlem1  27341  lgsquadlem2  27342  2sqlem1  27378  rpvmasum2  27473  madeval2  27809  newval  27811  leftval  27819  rightval  27820  lltropt  27828  madess  27832  oldssmade  27833  lrold  27852  addsproplem2  27920  addsproplem4  27922  addsproplem6  27924  negsproplem4  27980  negsproplem6  27982  precsexlem10  28157  precsexlem11  28158  sltonold  28200  elnns  28260  elzs  28287  edgiedgb  28979  isuhgr  28985  isushgr  28986  isupgr  29009  isumgr  29020  umgredg  29063  umgrpredgv  29065  umgredgne  29070  umgredgnlp  29072  isuspgr  29077  isusgr  29078  ausgrusgri  29093  usgredgppr  29121  edgssv2  29123  uspgredg2vlem  29148  uspgredg2v  29149  ushgredgedg  29154  ushgredgedgloop  29156  griedg0ssusgr  29190  uhgrissubgr  29200  subumgredg2  29210  uhgrspansubgrlem  29215  umgrres1lem  29235  upgrres1  29238  nbgrcl  29260  nbuhgr  29268  nbuhgr2vtx1edgblem  29276  nbupgrres  29289  edgnbusgreu  29292  nbusgredgeu0  29293  nbusgrf1o0  29294  hashnbusgrnn0  29301  nbupgruvtxres  29332  cffldtocusgr  29372  cffldtocusgrOLD  29373  cusgrfilem2  29382  vtxdg0v  29399  vtxduhgr0nedg  29418  uhgrvd00  29460  vtxdginducedm1  29469  finsumvtxdg2ssteplem4  29474  wlk1walk  29565  wlkp1lem6  29604  iswwlks  29764  wwlknllvtx  29774  wwlksonvtx  29783  wspthnonp  29787  wlkiswwlksupgr2  29805  wwlksnwwlksnon  29843  2pthon3v  29871  umgr2wlk  29877  elwwlks2s3  29879  wwlks2onv  29881  elwwlks2ons3im  29882  isclwwlk  29911  clwwlkccatlem  29916  clwlkclwwlk  29929  wwlksext2clwwlk  29984  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlknon1  30024  clwwlknon1nloop  30026  clwwlknon2x  30030  1pthon2v  30080  uhgr3cyclex  30109  isconngr  30116  isconngr1  30117  eucrctshift  30170  frgrnbnb  30220  frgrncvvdeqlem1  30226  frgrncvvdeqlem2  30227  frgrncvvdeqlem3  30228  frgrncvvdeqlem9  30234  fusgreghash2wspv  30262  extwwlkfab  30279  numclwwlk1lem2foa  30281  numclwwlk1lem2fo  30285  clwlknon2num  30295  numclwlk2lem2f1o  30306  numclwwlk5lem  30314  topnfbey  30396  isvclem  30504  isnvlem  30537  vsfval  30560  h2hlm  30907  hhcmpl  31127  hhcms  31130  elch0  31181  omlsilem  31329  h1de2ctlem  31482  elspansni  31485  nonbooli  31578  spansncvi  31579  adjeq  31862  cnlnssadj  32007  cnvbraval  32037  brabgaf  32534  2ndresdju  32573  fmptdF  32580  fmptcof2  32581  acunirnmpt  32583  acunirnmpt2  32584  ofpreima  32589  fcnvgreu  32597  fdifsuppconst  32612  1stpreima  32630  2ndpreima  32631  fz2ssnn0  32708  elxrge02  32852  ccatws1f1o  32873  gsumwrd2dccatlem  33006  psgnfzto1stlem  33057  cycpmgcl  33110  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem1  33188  nsgqusf1olem2  33375  nsgqusf1olem3  33376  prmidl0  33411  crngmxidl  33430  opprnsg  33445  rprmirredb  33493  zringfrac  33515  evl1deg2  33536  evl1deg3  33537  ply1degltel  33550  ply1degleel  33551  fldextrspunlsplem  33660  isconstr  33716  constrsuc  33718  constrconj  33725  submatres  33783  lmat22lem  33794  crefdf  33825  cmppcmp  33835  rspectopn  33844  prsdm  33891  prsrn  33892  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0iifhom  33914  pnfneige0  33928  qqhre  33997  rrhre  33998  esumnul  34025  esumcvgsum  34065  ldgenpisyslem1  34140  measvuni  34191  cntnevol  34205  dya2iocnrect  34259  sibf0  34312  oddpwdc  34332  eulerpartlemd  34344  eulerpartgbij  34350  eulerpartlemgh  34356  isrrvv  34421  coinfliprv  34461  ballotlem7  34514  signswch  34539  hashreprin  34598  chtvalz  34607  circlemethhgt  34621  hgt750lemb  34634  tgoldbachgt  34641  bnj23  34695  bnj158  34706  bnj168  34707  bnj1138  34765  bnj1143  34767  bnj1454  34819  bnj110  34835  bnj882  34903  bnj893  34905  bnj916  34910  bnj970  34924  bnj983  34928  bnj984  34929  bnj1137  34972  bnj1174  34980  bnj1388  35010  bnj1398  35011  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  35725  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  36211  fnessref  36321  bj-ififc  36546  bj-csbsnlem  36867  bj-elgab  36903  currysetlem1  36911  bj-eltag  36941  bj-sngltag  36947  bj-projun  36958  bj-velpwALT  37017  bj-0nelmpt  37080  bj-opelidres  37125  bj-inftyexpitaudisj  37169  bj-elccinfty  37178  f1omptsnlem  37300  icoreelrnab  37318  relowlpssretop  37328  rdgssun  37342  exrecfnlem  37343  finxpnom  37365  uncov  37571  tan2h  37582  ptrecube  37590  poimirlem25  37615  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  cnambfre  37638  ftc1cnnc  37662  sdclem2  37712  sdclem1  37713  fdc  37715  caushft  37731  issmgrpOLD  37833  ismndo  37842  isrngo  37867  isdivrngo  37920  csbcom2fi  38098  elecALTV  38230  brrabga  38305  eldmcoss  38422  coss0  38443  elrels2  38450  dath  39701  diclspsn  41159  dvh4dimlem  41408  dvh2dim  41410  dvh3dim3N  41414  lcfrvalsnN  41506  mapdh6eN  41705  mapdh7dN  41715  mapdh8b  41745  hdmap1l6e  41779  lcmfunnnd  41971  3factsumint1  41980  primrootsunit1  42056  primrootscoprmpow  42058  aks6d1c2lem4  42086  sticksstones2  42106  sticksstones3  42107  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem2  42130  aks6d1c6lem3  42131  redvmptabs  42350  readvrec2  42351  readvrec  42352  frlmfielbas  42470  mhpind  42564  pellex  42805  rmspecnonsq  42877  islmodfg  43040  aaitgo  43133  areaquad  43187  ordeldif1o  43231  naddwordnexlem4  43372  fpwfvss  43383  finona1cl  43424  elcnvcnvintab  43553  elnonrel  43556  elcnvcnvlem  43570  cnvcnvintabd  43571  brfvrcld2  43663  grur1cld  44204  dvgrat  44284  cvgdvgrat  44285  radcnvrat  44286  nznngen  44288  uzmptshftfval  44318  binomcxplemcvg  44326  binomcxplemnotnn0  44328  tpid3gVD  44814  en3lplem2VD  44816  orbitclmpt  44931  wfaxrep  44967  wfaxsep  44968  wfaxpow  44970  wfaxpr  44971  wfaxun  44972  wfac8prim  44975  brpermmodelcnv  44977  iuneq1i  45057  rexanuz3  45068  eliuniin  45071  eliuniin2  45092  disjinfi  45164  fsneq  45178  iuneqfzuzlem  45309  allbutfi  45368  eluzelz2  45378  uz0  45387  uzublem  45405  uzid3  45410  elicores  45510  uzinico  45536  climsuselem1  45584  climsuse  45585  islptre  45596  fnlimfvre  45651  limsupresico  45677  limsupvaluz  45685  limsupubuzlem  45689  limsupequzmptlem  45705  liminfresico  45748  cnrefiisplem  45806  stoweidlem14  45991  stoweidlem39  46016  stoweidlem48  46025  stoweidlem51  46028  stoweidlem59  46036  stoweidlem62  46039  wallispilem3  46044  fourierdlem42  46126  fourierdlem62  46145  fourierdlem80  46163  fourierdlem103  46186  fourierdlem104  46187  etransclem26  46237  rrxsnicc  46277  ioorrnopn  46282  ioorrnopnxr  46284  sge00  46353  sge0fodjrnlem  46393  sge0isum  46404  sge0seq  46423  meadjiunlem  46442  carageneld  46479  volicorescl  46530  hoidmv1lelem1  46568  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem3  46574  ovnhoilem2  46579  hoiqssbllem2  46600  opnvonmbllem2  46610  ovolval4lem1  46626  iinhoiicc  46651  vonioolem1  46657  smflimlem1  46748  smflimlem2  46749  smflim  46754  nsssmfmbf  46756  smfresal  46765  smfrec  46766  smfdiv  46774  smfpimbor1lem2  46776  smflim2  46783  smflimmpt  46787  smfinflem  46794  smflimsuplem1  46797  smflimsuplem2  46798  smflimsuplem3  46799  smflimsuplem5  46801  smflimsuplem6  46802  smflimsup  46805  smflimsupmpt  46806  smfliminfmpt  46809  fcores  47044  ndmaovcl  47180  ndmaovcom  47182  ndmaovass  47183  ndmaovdistr  47184  dfatco  47233  otiunsndisjX  47256  fvmptrabdm  47270  ceilhalfelfzo1  47307  elsetpreimafvb  47346  sprsymrelfolem2  47455  sprsymrelf  47457  sprsymrelf1  47458  prpair  47463  prproropf1olem0  47464  paireqne  47473  fmtno4prmfac  47534  dfodd5  47622  sbgoldbo  47749  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  clnbgrcl  47783  clnbgredg  47801  sclnbgrel  47808  isubgredg  47827  uhgrimedgi  47851  isuspgrim0  47855  isuspgrimlem  47856  gricushgr  47878  clnbgrgrimlem  47894  grimedg  47896  usgrgrtrirex  47910  stgrnbgr0  47924  isubgr3stgrlem3  47928  isubgr3stgrlem4  47929  isubgr3stgrlem6  47931  isubgr3stgrlem7  47932  uspgrlimlem2  47949  uspgrlimlem3  47950  grlimgrtrilem1  47954  grlimgrtrilem2  47955  usgrexmpl2trifr  47989  gpgvtxel  47999  gpgedgel  48002  gpgusgralem  48008  gpg5order  48012  gpgvtxedg0  48015  gpgvtxedg1  48016  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  gpg3nbgrvtx1  48028  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  gpgvtxdg3  48032  gpg5gricstgr3  48040  gpgprismgr4cycllem3  48044  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem8  48049  gpgprismgr4cycllem10  48051  uspgrsprf  48069  uspgrsprf1  48070  uspgrsprfo  48071  ply1sclrmsm  48307  lcoop  48335  lincfsuppcl  48337  linccl  48338  lincvalsng  48340  lincvalpr  48342  lincvalsc0  48345  linc0scn0  48347  lincdifsn  48348  linc1  48349  lincsum  48353  lincscm  48354  lspsslco  48361  snlindsntor  48395  lincresunit3lem2  48404  ldepsnlinclem1  48429  ldepsnlinclem2  48430  prelrrx2  48641  prelrrx2b  48642  rrx2xpref1o  48646  rrx2plord  48648  rrx2linesl  48671  initopropdlemlem  49104  initopropd  49108  termopropd  49109  zeroopropd  49110  oppcthin  49272  indthinc  49296  prsthinc  49298  elpglem3  49525