Theorem eleq2i 2821

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  eleq12i  2822  eleqtri  2827  eleq2s  2847  hbxfreq  2859  nfceqi  2889  raleqbii  3319  rexeqbii  3320  rabeqi  3422  rabrabi  3428  reqabi  3432  elab2gw  3648  elab2g  3650  elrabf  3658  elrab3t  3661  elrab2  3665  cbvsbcw  3789  cbvsbcvw  3790  cbvsbc  3791  elin2  4169  elsymdif  4224  noel  4304  eltpg  4653  elunirab  4889  elintrab  4927  disjxiun  5107  exss  5426  otiunsndisj  5483  brabsb  5494  brabga  5497  epelg  5542  pofun  5567  elxp  5664  opeliunxp  5708  opeliun2xp  5709  bropaex12  5733  brab2a  5735  elcnv  5843  dmopabelb  5883  elrnmptg  5928  elres  5994  elimampt  6017  elrid  6020  rninxp  6155  elid  6175  elsuci  6404  elsucg  6405  elsuc2g  6406  elfv  6859  0fv  6905  opabiota  6946  dffv2  6959  fvopab3g  6966  fvmptex  6985  fvopab5  7004  fvn0ssdmfun  7049  fveqressseq  7054  f0cli  7073  fmptco  7104  fvrnressn  7136  funfvima  7207  elunirnALT  7229  fliftel  7287  eloprabga  7501  elrnmpo  7528  elimampo  7529  ovid  7533  offval  7665  sucexeloniOLD  7789  1st2val  7999  2nd2val  8000  bropopvvv  8072  bropfvvvv  8074  fsplit  8099  xporderlem  8109  frpoins3xpg  8122  frpoins3xp3g  8123  brtpos2  8214  frrlem8  8275  frrlem9  8276  frrlem10  8277  fprresex  8292  issmo  8320  smores3  8325  tfrlem7  8354  tfrlem9  8356  tfrlem9a  8357  tfr2b  8367  tfr2  8369  rdgsuc  8395  frsucmptn  8410  tz7.48-2  8413  el1o  8462  ord2eln012  8464  dif1o  8467  ondif2  8469  oawordeulem  8521  elecg  8718  brecop  8786  erovlem  8789  eceqoveq  8798  mapsncnv  8869  mptelixpg  8911  brsdom  8949  isfi  8950  enssdom  8951  brdom2  8956  xpcomco  9036  brsdom2  9071  en3lplem2  9573  cnfcom2lem  9661  brttrcl2  9674  ttrcltr  9676  rnttrcl  9682  epfrs  9691  r1limg  9731  r1ord  9740  r1ord3  9742  tz9.12lem3  9749  rankvaln  9759  r1elss  9766  rankpwi  9783  ssrankr1  9795  r1val3  9798  r1pw  9805  rankr1b  9824  djur  9879  djuunxp  9881  eldju2ndl  9884  eldju2ndr  9885  isnum2  9905  cardprclem  9939  infxpenlem  9973  alephcard  10030  alephnbtwn  10031  alephnbtwn2  10032  alephord2  10036  alephsdom  10046  dfac3  10081  dfac5lem2  10084  dfac5lem3  10085  dfac5lem5  10087  pwsdompw  10163  cfub  10209  cardcf  10212  cflecard  10213  cfle  10214  cflim2  10223  cofsmo  10229  cfidm  10235  isfin3  10256  isfin5  10259  isfin6  10260  sdom2en01  10262  fin23lem26  10285  fin23lem30  10302  isf32lem5  10317  itunitc1  10380  ituniiun  10382  axdc3lem3  10412  axcclem  10417  axdclem  10479  iunfo  10499  iundom2g  10500  cardidg  10508  konigthlem  10528  alephadd  10537  alephreg  10542  pwcfsdom  10543  cfpwsdom  10544  elgch  10582  fpwwe2lem11  10601  canth4  10607  wunex2  10698  r1tskina  10742  elni  10836  nlt1pi  10866  adderpq  10916  mulerpq  10917  recmulnq  10924  addsrpr  11035  mulsrpr  11036  opelcn  11089  opelreal  11090  elreal  11091  elreal2  11092  0ncn  11093  addcnsr  11095  mulcnsr  11096  xrlenlt  11246  elnn0  12451  elnnne0  12463  un0addcl  12482  un0mulcl  12483  elxnn0  12524  uztrn2  12819  elnnuz  12844  elnn0uz  12845  elq  12916  elxr  13083  elfzm1b  13570  elfz0lmr  13750  uzrdgfni  13930  fzennn  13940  ser0  14026  hash2pwpr  14448  iswrd  14487  pfxccatpfx1  14708  s3iunsndisj  14941  sumz  15695  sumss  15697  fsumcvg3  15702  abscvgcvg  15792  isumshft  15812  prodf1  15864  prodeq1i  15889  zprod  15910  prod1  15917  prodss  15920  prodsn  15935  prodsnf  15937  bpolydiflem  16027  bpoly2  16030  bpoly3  16031  bpoly4  16032  ruclem6  16210  divides  16231  dvdsflip  16294  pwp1fsum  16368  sadc0  16431  eulerthlem2  16759  prm23lt5  16792  4sqlem2  16927  4sqlem12  16934  vdwpc  16958  xpscf  17535  cidpropd  17678  oppcsect  17747  funcpropd  17871  natpropd  17948  dfinito2  17972  dftermo2  17973  initoeu2lem0  17982  arwhoma  18014  eldmcoa  18034  pospo  18311  psss  18546  ismgmn0  18576  gsumpropd2lem  18613  elefmndbas  18807  smndex1basss  18839  smndex1mgm  18841  pwmnd  18871  dfgrp2e  18902  mulgfval  19008  eqg0subg  19135  cycsubmel  19139  ghmeqker  19182  elcntr  19269  cntri  19271  cntzsgrpcl  19273  oppgsubg  19302  fvcosymgeq  19366  symgfixels  19371  pmtrfrn  19395  efgsfo  19676  efgrelexlemb  19687  lt6abl  19832  dmdprd  19937  dprdval  19942  dprdw  19949  srgbinomlem4  20145  isnirred  20336  isrhm  20394  issrng  20760  lspexchn2  21048  lspindp2l  21051  lspindp2  21052  lbsextlem2  21076  rnglidl1  21149  df2idl2  21174  2idlss  21179  rngqiprngimfo  21218  cnfldfun  21285  cnfldfunOLD  21298  pzriprnglem3  21400  pzriprnglem4  21401  pzriprnglem7  21404  pzriprnglem8  21405  pzriprnglem9  21406  pzriprnglem12  21409  pzriprnglem14  21411  dsmmelbas  21655  frlmbas3  21692  lindsind2  21735  islindf4  21754  psrbagf  21834  evlslem4  21990  psdmul  22060  ply1bascl2  22096  cply1mul  22190  lply1binom  22204  matsubgcell  22328  matinvgcell  22329  matvscacell  22330  matepmcl  22356  matepm2cl  22357  scmatscm  22407  smatvscl  22418  marrepcl  22458  marepvcl  22463  mulmarep1el  22466  mulmarep1gsum1  22467  mulmarep1gsum2  22468  submabas  22472  m1detdiag  22491  mdetdiag  22493  m2detleib  22525  gsummatr01lem3  22551  gsummatr01  22553  smadiadetlem4  22563  slesolinv  22574  slesolinvbi  22575  slesolex  22576  cramerimplem2  22578  pmatcoe1fsupp  22595  mat2pmatbas  22620  mat2pmatmul  22625  mat2pmatlin  22629  decpmatmul  22666  monmatcollpw  22673  pm2mpf1  22693  pm2mpghm  22710  istps  22828  mretopd  22986  neiptopuni  23024  lpdifsn  23037  restcls  23075  perfopn  23079  pnfnei  23114  mnfnei  23115  lmss  23192  hauscmplem  23300  is2ndc  23340  2ndcdisj  23350  hausnlly  23387  txuni2  23459  ptpjpre1  23465  elpt  23466  dfac14  23512  xkococn  23554  fbasrn  23778  fin1aufil  23826  elfm2  23842  elfm3  23844  fbflim  23870  flffbas  23889  cnpflf2  23894  fclsbas  23915  efmndtmd  23995  tsmssubm  24037  iscusp2  24196  imasdsf1olem  24268  metustel  24445  metuel2  24460  isnghm  24618  opnreen  24727  iccpnfcnv  24849  ehleudisval  25326  ehl1eudis  25327  ehl2eudis  25329  minveclem3b  25335  ovoliunlem1  25410  ioombl1lem4  25469  subopnmbl  25512  vitalilem2  25517  vitalilem3  25518  mbfimaopnlem  25563  mbfimaopn2  25565  itg2l  25637  dvply1  26198  vieta1lem1  26225  vieta1lem2  26226  elaa  26231  taylthlem2  26289  taylthlem2OLD  26290  abelthlem6  26353  abelthlem9  26357  sinq34lt0t  26425  ellogrn  26475  dvrelog  26553  ellogdm  26555  logtayl2  26578  cxpcn3lem  26664  cxpcn3  26665  1cubr  26759  atandm  26793  atanf  26797  reasinsin  26813  atans2  26848  dmarea  26874  xrlimcnp  26885  amgmlem  26907  ppiublem1  27120  lgsdir2lem2  27244  gausslemma2dlem1a  27283  lgsquadlem1  27298  lgsquadlem2  27299  2sqlem1  27335  rpvmasum2  27430  madeval2  27768  newval  27770  leftval  27778  rightval  27779  lltropt  27791  madess  27795  oldssmade  27796  lrold  27815  addsproplem2  27884  addsproplem4  27886  addsproplem6  27888  negsproplem4  27944  negsproplem6  27946  precsexlem10  28125  precsexlem11  28126  sltonold  28169  elnns  28239  elzs  28279  edgiedgb  28988  isuhgr  28994  isushgr  28995  isupgr  29018  isumgr  29029  umgredg  29072  umgrpredgv  29074  umgredgne  29079  umgredgnlp  29081  isuspgr  29086  isusgr  29087  ausgrusgri  29102  usgredgppr  29130  edgssv2  29132  uspgredg2vlem  29157  uspgredg2v  29158  ushgredgedg  29163  ushgredgedgloop  29165  griedg0ssusgr  29199  uhgrissubgr  29209  subumgredg2  29219  uhgrspansubgrlem  29224  umgrres1lem  29244  upgrres1  29247  nbgrcl  29269  nbuhgr  29277  nbuhgr2vtx1edgblem  29285  nbupgrres  29298  edgnbusgreu  29301  nbusgredgeu0  29302  nbusgrf1o0  29303  hashnbusgrnn0  29310  nbupgruvtxres  29341  cffldtocusgr  29381  cffldtocusgrOLD  29382  cusgrfilem2  29391  vtxdg0v  29408  vtxduhgr0nedg  29427  uhgrvd00  29469  vtxdginducedm1  29478  finsumvtxdg2ssteplem4  29483  wlk1walk  29574  wlkp1lem6  29613  iswwlks  29773  wwlknllvtx  29783  wwlksonvtx  29792  wspthnonp  29796  wlkiswwlksupgr2  29814  wwlksnwwlksnon  29852  2pthon3v  29880  umgr2wlk  29886  elwwlks2s3  29888  wwlks2onv  29890  elwwlks2ons3im  29891  isclwwlk  29920  clwwlkccatlem  29925  clwlkclwwlk  29938  wwlksext2clwwlk  29993  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknon1  30033  clwwlknon1nloop  30035  clwwlknon2x  30039  1pthon2v  30089  uhgr3cyclex  30118  isconngr  30125  isconngr1  30126  eucrctshift  30179  frgrnbnb  30229  frgrncvvdeqlem1  30235  frgrncvvdeqlem2  30236  frgrncvvdeqlem3  30237  frgrncvvdeqlem9  30243  fusgreghash2wspv  30271  extwwlkfab  30288  numclwwlk1lem2foa  30290  numclwwlk1lem2fo  30294  clwlknon2num  30304  numclwlk2lem2f1o  30315  numclwwlk5lem  30323  topnfbey  30405  isvclem  30513  isnvlem  30546  vsfval  30569  h2hlm  30916  hhcmpl  31136  hhcms  31139  elch0  31190  omlsilem  31338  h1de2ctlem  31491  elspansni  31494  nonbooli  31587  spansncvi  31588  adjeq  31871  cnlnssadj  32016  cnvbraval  32046  brabgaf  32543  2ndresdju  32580  fmptdF  32587  fmptcof2  32588  acunirnmpt  32590  acunirnmpt2  32591  ofpreima  32596  fcnvgreu  32604  fdifsuppconst  32619  1stpreima  32637  2ndpreima  32638  fz2ssnn0  32715  elxrge02  32859  ccatws1f1o  32880  gsumwrd2dccatlem  33013  psgnfzto1stlem  33064  cycpmgcl  33117  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem1  33205  nsgqusf1olem2  33392  nsgqusf1olem3  33393  prmidl0  33428  crngmxidl  33447  opprnsg  33462  rprmirredb  33510  zringfrac  33532  evl1deg2  33553  evl1deg3  33554  ply1degltel  33567  ply1degleel  33568  fldextrspunlsplem  33675  isconstr  33733  constrsuc  33735  constrconj  33742  submatres  33803  lmat22lem  33814  crefdf  33845  cmppcmp  33855  rspectopn  33864  prsdm  33911  prsrn  33912  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  pnfneige0  33948  qqhre  34017  rrhre  34018  esumnul  34045  esumcvgsum  34085  ldgenpisyslem1  34160  measvuni  34211  cntnevol  34225  dya2iocnrect  34279  sibf0  34332  oddpwdc  34352  eulerpartlemd  34364  eulerpartgbij  34370  eulerpartlemgh  34376  isrrvv  34441  coinfliprv  34481  ballotlem7  34534  signswch  34559  hashreprin  34618  chtvalz  34627  circlemethhgt  34641  hgt750lemb  34654  tgoldbachgt  34661  bnj23  34715  bnj158  34726  bnj168  34727  bnj1138  34785  bnj1143  34787  bnj1454  34839  bnj110  34855  bnj882  34923  bnj893  34925  bnj916  34930  bnj970  34944  bnj983  34948  bnj984  34949  bnj1137  34992  bnj1174  35000  bnj1388  35030  bnj1398  35031  onvf1odlem4  35100  loop1cycl  35131  subfacp1lem5  35178  satfv1  35357  satfrnmapom  35364  satf0op  35371  satf0n0  35372  fmlafvel  35379  fmlaomn0  35384  fmlan0  35385  satffunlem2lem2  35400  satfv0fvfmla0  35407  satefvfmla0  35412  mrsub0  35510  mrsubccat  35512  mrsubcn  35513  elmrsubrn  35514  msubco  35525  msubvrs  35554  elmthm  35570  mthmblem  35574  ellcsrspsn  35635  elrn3  35756  dfon2lem7  35784  brsset  35884  eltrans  35886  elfix  35898  ellimits  35905  elfuns  35910  elsingles  35913  fvtransport  36027  brcolinear2  36053  fvray  36136  linedegen  36138  fvline  36139  ellines  36147  fwddifn0  36159  elhf  36169  hfninf  36181  rmoeqi  36182  rmoeqbii  36183  reueqi  36184  reueqbii  36185  rabeqbii  36189  iuneq12i  36190  iineq1i  36191  iineq12i  36192  riotaeqbii  36193  ixpeq1i  36195  itgeq12i  36201  cbvprodvw2  36242  fnessref  36352  bj-ififc  36577  bj-csbsnlem  36898  bj-elgab  36934  currysetlem1  36942  bj-eltag  36972  bj-sngltag  36978  bj-projun  36989  bj-velpwALT  37048  bj-0nelmpt  37111  bj-opelidres  37156  bj-inftyexpitaudisj  37200  bj-elccinfty  37209  f1omptsnlem  37331  icoreelrnab  37349  relowlpssretop  37359  rdgssun  37373  exrecfnlem  37374  finxpnom  37396  uncov  37602  tan2h  37613  ptrecube  37621  poimirlem25  37646  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  cnambfre  37669  ftc1cnnc  37693  sdclem2  37743  sdclem1  37744  fdc  37746  caushft  37762  issmgrpOLD  37864  ismndo  37873  isrngo  37898  isdivrngo  37951  csbcom2fi  38129  elecALTV  38262  brrabga  38330  eldmxrncnvepres  38403  eldmxrncnvepres2  38404  eldmcoss  38456  coss0  38477  elrels2  38484  dath  39737  diclspsn  41195  dvh4dimlem  41444  dvh2dim  41446  dvh3dim3N  41450  lcfrvalsnN  41542  mapdh6eN  41741  mapdh7dN  41751  mapdh8b  41781  hdmap1l6e  41815  lcmfunnnd  42007  3factsumint1  42016  primrootsunit1  42092  primrootscoprmpow  42094  aks6d1c2lem4  42122  sticksstones2  42142  sticksstones3  42143  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem2  42166  aks6d1c6lem3  42167  redvmptabs  42355  readvrec2  42356  readvrec  42357  frlmfielbas  42495  mhpind  42589  pellex  42830  rmspecnonsq  42902  islmodfg  43065  aaitgo  43158  areaquad  43212  ordeldif1o  43256  naddwordnexlem4  43397  fpwfvss  43408  finona1cl  43449  elcnvcnvintab  43578  elnonrel  43581  elcnvcnvlem  43595  cnvcnvintabd  43596  brfvrcld2  43688  grur1cld  44228  dvgrat  44308  cvgdvgrat  44309  radcnvrat  44310  nznngen  44312  uzmptshftfval  44342  binomcxplemcvg  44350  binomcxplemnotnn0  44352  tpid3gVD  44838  en3lplem2VD  44840  orbitclmpt  44955  wfaxrep  44991  wfaxsep  44992  wfaxpow  44994  wfaxpr  44995  wfaxun  44996  wfac8prim  44999  brpermmodelcnv  45001  nregmodellem  45013  iuneq1i  45086  rexanuz3  45097  eliuniin  45100  eliuniin2  45121  disjinfi  45193  fsneq  45207  iuneqfzuzlem  45337  allbutfi  45396  eluzelz2  45406  uz0  45415  uzublem  45433  uzid3  45438  elicores  45538  uzinico  45564  climsuselem1  45612  climsuse  45613  islptre  45624  fnlimfvre  45679  limsupresico  45705  limsupvaluz  45713  limsupubuzlem  45717  limsupequzmptlem  45733  liminfresico  45776  cnrefiisplem  45834  stoweidlem14  46019  stoweidlem39  46044  stoweidlem48  46053  stoweidlem51  46056  stoweidlem59  46064  stoweidlem62  46067  wallispilem3  46072  fourierdlem42  46154  fourierdlem62  46173  fourierdlem80  46191  fourierdlem103  46214  fourierdlem104  46215  etransclem26  46265  rrxsnicc  46305  ioorrnopn  46310  ioorrnopnxr  46312  sge00  46381  sge0fodjrnlem  46421  sge0isum  46432  sge0seq  46451  meadjiunlem  46470  carageneld  46507  volicorescl  46558  hoidmv1lelem1  46596  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem3  46602  ovnhoilem2  46607  hoiqssbllem2  46628  opnvonmbllem2  46638  ovolval4lem1  46654  iinhoiicc  46679  vonioolem1  46685  smflimlem1  46776  smflimlem2  46777  smflim  46782  nsssmfmbf  46784  smfresal  46793  smfrec  46794  smfdiv  46802  smfpimbor1lem2  46804  smflim2  46811  smflimmpt  46815  smfinflem  46822  smflimsuplem1  46825  smflimsuplem2  46826  smflimsuplem3  46827  smflimsuplem5  46829  smflimsuplem6  46830  smflimsup  46833  smflimsupmpt  46834  smfliminfmpt  46837  fcores  47072  ndmaovcl  47208  ndmaovcom  47210  ndmaovass  47211  ndmaovdistr  47212  dfatco  47261  otiunsndisjX  47284  fvmptrabdm  47298  ceilhalfelfzo1  47335  modmknepk  47367  elsetpreimafvb  47389  sprsymrelfolem2  47498  sprsymrelf  47500  sprsymrelf1  47501  prpair  47506  prproropf1olem0  47507  paireqne  47516  fmtno4prmfac  47577  dfodd5  47665  sbgoldbo  47792  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  clnbgrcl  47826  clnbgredg  47844  sclnbgrel  47851  isubgredg  47870  uhgrimedgi  47894  isuspgrim0  47898  isuspgrimlem  47899  gricushgr  47921  clnbgrgrimlem  47937  grimedg  47939  usgrgrtrirex  47953  stgrnbgr0  47967  isubgr3stgrlem3  47971  isubgr3stgrlem4  47972  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  uspgrlimlem2  47992  uspgrlimlem3  47993  grlimgrtrilem1  47997  grlimgrtrilem2  47998  usgrexmpl2trifr  48032  gpgvtxel  48042  gpgedgel  48045  gpgusgralem  48051  gpg5order  48055  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpgvtxdg3  48077  gpg5gricstgr3  48085  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem8  48096  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  pgnbgreunbgr  48119  uspgrsprf  48138  uspgrsprf1  48139  uspgrsprfo  48140  ply1sclrmsm  48376  lcoop  48404  lincfsuppcl  48406  linccl  48407  lincvalsng  48409  lincvalpr  48411  lincvalsc0  48414  linc0scn0  48416  lincdifsn  48417  linc1  48418  lincsum  48422  lincscm  48423  lspsslco  48430  snlindsntor  48464  lincresunit3lem2  48473  ldepsnlinclem1  48498  ldepsnlinclem2  48499  prelrrx2  48706  prelrrx2b  48707  rrx2xpref1o  48711  rrx2plord  48713  rrx2linesl  48736  sectrcl  49015  invrcl  49017  initopropdlemlem  49232  initopropd  49236  termopropd  49237  zeroopropd  49238  oppcthin  49431  indthinc  49455  prsthinc  49457  elpglem3  49706