Theorem eleq2i 2854

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

Syntax hints:   ↔ wb 208   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  eleq12i  2855  eleqtri  2860  eleq2s  2880  hbxfreq  2892  nfceqi  2921  raleqbii  3334  rexeqbii  3335  rabeqi  3427  rabrabi  3433  reqabi  3437  elab2gw  3637  elab2g  3639  elrabf  3647  elrab3t  3649  elrab2  3654  cbvsbcw  3777  cbvsbcvw  3778  cbvsbc  3779  elin2  4155  elsymdif  4210  noel  4290  eltpg  4645  elunirab  4880  elintrab  4918  disjxiun  5097  exss  5430  otiunsndisj  5489  brabsb  5501  brabga  5504  epelg  5548  pofun  5573  elxp  5670  opeliunxp  5714  opeliun2xp  5715  bropaex12  5738  brab2a  5740  elcnv  5848  cnv0  5855  dmopabelb  5892  elrnmptg  5937  elres  6006  elimampt  6032  elrid  6035  rninxp  6165  elid  6186  elsuci  6415  elsucg  6416  elsuc2g  6417  elfv  6865  0fv  6908  opabiota  6949  dffv2  6962  fvopab3g  6970  fvmptex  6990  fvopab5  7009  fsneq  7016  fvn0ssdmfun  7055  fveqressseq  7060  f0cli  7079  fmptco  7111  fvrnressn  7144  funfvima  7214  elunirnALT  7236  fliftel  7293  eloprabga  7505  elrnmpo  7532  elimampo  7533  ovid  7537  offval  7669  1st2val  7998  2nd2val  7999  bropopvvv  8069  bropfvvvv  8071  fsplit  8096  xporderlem  8107  frpoins3xpg  8120  frpoins3xp3g  8121  brtpos2  8212  frrlem8  8274  frrlem9  8275  frrlem10  8276  fprresex  8291  issmo  8319  smores3  8324  tfrlem7  8354  tfrlem9  8356  tfrlem9a  8357  tfr2b  8367  tfr2  8369  rdgsuc  8395  frsucmptn  8410  tz7.48-2  8413  el1o  8464  ord2eln012  8466  dif1o  8469  ondif2  8471  oawordeulem  8523  elecg  8723  brecop  8792  erovlem  8795  eceqoveq  8804  mapsncnv  8875  mptelixpg  8917  brsdom  8955  isfi  8956  enssdomOLD  8958  brdom2  8963  xpcomco  9039  brsdom2  9073  en3lplem2  9568  cnfcom2lem  9656  brttrcl2  9669  ttrcltr  9671  rnttrcl  9677  epfrs  9686  r1limg  9729  r1ord  9738  r1ord3  9740  tz9.12lem3  9747  rankvaln  9757  r1elss  9764  rankpwi  9781  ssrankr1  9793  r1val3  9796  r1pw  9803  rankr1b  9822  djur  9877  djuunxp  9879  eldju2ndl  9882  eldju2ndr  9883  isnum2  9903  cardprclem  9937  infxpenlem  9969  alephcard  10026  alephnbtwn  10027  alephnbtwn2  10028  alephord2  10032  alephsdom  10042  dfac3  10077  dfac5lem2  10080  dfac5lem3  10081  dfac5lem5  10083  pwsdompw  10159  cfub  10205  cardcf  10208  cflecard  10209  cfle  10210  cflim2  10220  cofsmo  10226  cfidm  10232  isfin3  10253  isfin5  10256  isfin6  10257  sdom2en01  10259  fin23lem26  10282  fin23lem30  10299  isf32lem5  10314  itunitc1  10377  ituniiun  10379  axdc3lem3  10409  axcclem  10414  axdclem  10476  iunfo  10496  iundom2g  10497  cardidg  10505  konigthlem  10526  alephadd  10535  alephreg  10540  pwcfsdom  10541  cfpwsdom  10542  elgch  10580  fpwwe2lem11  10599  canth4  10605  wunex2  10696  r1tskina  10740  elni  10834  nlt1pi  10864  adderpq  10914  mulerpq  10915  recmulnq  10922  addsrpr  11033  mulsrpr  11034  opelcn  11087  opelreal  11088  elreal  11089  elreal2  11090  0ncn  11091  addcnsr  11093  mulcnsr  11094  xrlenlt  11247  elnn0  12483  elnnne0  12495  un0addcl  12514  un0mulcl  12515  elxnn0  12556  uztrn2  12858  elnnuz  12879  elnn0uz  12880  elq  12951  elxr  13118  elfzm1b  13607  elfz0lmr  13789  uzrdgfni  13971  fzennn  13981  ser0  14067  hash2pwpr  14489  iswrd  14528  pfxccatpfx1  14749  s3iunsndisj  14981  sumz  15749  sumss  15751  fsumcvg3  15756  abscvgcvg  15847  isumshft  15869  prodf1  15921  prodeq1i  15946  zprod  15967  prod1  15974  prodss  15977  prodsn  15992  prodsnf  15994  bpolydiflem  16084  bpoly2  16087  bpoly3  16088  bpoly4  16089  ruclem6  16267  divides  16288  dvdsflip  16351  pwp1fsum  16425  sadc0  16488  eulerthlem2  16817  prm23lt5  16850  4sqlem2  16985  4sqlem12  16992  vdwpc  17016  xpscf  17595  cidpropd  17742  oppcsect  17811  funcpropd  17935  natpropd  18012  dfinito2  18036  dftermo2  18037  initoeu2lem0  18046  arwhoma  18078  eldmcoa  18098  pospo  18375  psss  18612  ex-chn1  18669  ex-chn2  18670  ismgmn0  18676  gsumpropd2lem  18713  elefmndbas  18907  smndex1basss  18942  smndex1mgm  18944  pwmnd  18974  dfgrp2e  19005  mulgfval  19111  eqg0subg  19237  cycsubmel  19241  ghmeqker  19283  elcntr  19370  cntri  19372  cntzsgrpcl  19374  oppgsubg  19403  fvcosymgeq  19469  symgfixels  19474  pmtrfrn  19498  efgsfo  19779  efgrelexlemb  19790  lt6abl  19935  dmdprd  20040  dprdval  20045  dprdw  20052  srgbinomlem4  20279  isnirred  20469  isrhm  20527  issrng  20893  lspexchn2  21201  lspindp2l  21204  lspindp2  21205  lbsextlem2  21229  rnglidl1  21302  df2idl2  21327  2idlss  21332  rngqiprngimfo  21371  cnfldfun  21438  pzriprnglem3  21535  pzriprnglem4  21536  pzriprnglem7  21539  pzriprnglem8  21540  pzriprnglem9  21541  pzriprnglem12  21544  pzriprnglem14  21546  dsmmelbas  21791  frlmbas3  21828  lindsind2  21871  islindf4  21890  psrbagf  21970  evlslem4  22129  psdmul  22231  ply1bascl2  22266  cply1mul  22359  lply1binom  22373  matsubgcell  22494  matinvgcell  22495  matvscacell  22496  matepmcl  22522  matepm2cl  22523  scmatscm  22573  smatvscl  22584  marrepcl  22624  marepvcl  22629  mulmarep1el  22632  mulmarep1gsum1  22633  mulmarep1gsum2  22634  submabas  22638  m1detdiag  22657  mdetdiag  22659  m2detleib  22691  gsummatr01lem3  22717  gsummatr01  22719  smadiadetlem4  22729  slesolinv  22740  slesolinvbi  22741  slesolex  22742  cramerimplem2  22744  pmatcoe1fsupp  22761  mat2pmatbas  22786  mat2pmatmul  22791  mat2pmatlin  22795  decpmatmul  22832  monmatcollpw  22839  pm2mpf1  22859  pm2mpghm  22876  istps  22994  mretopd  23152  neiptopuni  23190  lpdifsn  23203  restcls  23241  perfopn  23245  pnfnei  23280  mnfnei  23281  lmss  23358  hauscmplem  23466  is2ndc  23506  2ndcdisj  23516  hausnlly  23553  txuni2  23625  ptpjpre1  23631  elpt  23632  dfac14  23678  xkococn  23720  fbasrn  23944  fin1aufil  23992  elfm2  24008  elfm3  24010  fbflim  24036  flffbas  24055  cnpflf2  24060  fclsbas  24081  efmndtmd  24161  tsmssubm  24203  iscusp2  24361  imasdsf1olem  24433  metustel  24610  metuel2  24625  isnghm  24783  opnreen  24892  iccpnfcnv  25006  ehleudisval  25481  ehl1eudis  25482  ehl2eudis  25484  minveclem3b  25490  ovoliunlem1  25564  ioombl1lem4  25623  subopnmbl  25666  vitalilem2  25671  vitalilem3  25672  mbfimaopnlem  25717  mbfimaopn2  25719  itg2l  25791  dvply1  26348  vieta1lem1  26374  vieta1lem2  26375  elaa  26380  taylthlem2  26437  abelthlem6  26499  abelthlem9  26503  sinq34lt0t  26574  ellogrn  26624  dvrelog  26702  ellogdm  26704  logtayl2  26727  cxpcn3lem  26812  cxpcn3  26813  1cubr  26907  atandm  26941  atanf  26945  reasinsin  26961  atans2  26996  dmarea  27022  xrlimcnp  27033  amgmlem  27054  ppiublem1  27266  lgsdir2lem2  27390  gausslemma2dlem1a  27429  lgsquadlem1  27444  lgsquadlem2  27445  2sqlem1  27481  rpvmasum2  27576  madeval2  27926  newval  27928  leftval  27942  rightval  27943  lltr  27955  madess  27959  oldssmade  27960  oldss  27963  lrold  27990  addsproplem2  28063  addsproplem4  28065  addsproplem6  28067  negsproplem4  28124  negsproplem6  28126  precsexlem10  28309  precsexlem11  28310  ltonold  28354  elnns  28433  elzs  28477  edgiedgb  29255  isuhgr  29261  isushgr  29262  isupgr  29285  isumgr  29296  umgredg  29339  umgrpredgv  29341  umgredgne  29346  umgredgnlp  29348  isuspgr  29353  isusgr  29354  ausgrusgri  29369  usgredgppr  29397  edgssv2  29399  uspgredg2vlem  29424  uspgredg2v  29425  ushgredgedg  29430  ushgredgedgloop  29432  griedg0ssusgr  29466  uhgrissubgr  29476  subumgredg2  29486  uhgrspansubgrlem  29491  umgrres1lem  29511  upgrres1  29514  nbgrcl  29536  nbuhgr  29544  nbuhgr2vtx1edgblem  29552  nbupgrres  29565  edgnbusgreu  29568  nbusgredgeu0  29569  nbusgrf1o0  29570  hashnbusgrnn0  29577  nbupgruvtxres  29608  cffldtocusgr  29648  cusgrfilem2  29657  vtxdg0v  29674  vtxduhgr0nedg  29693  uhgrvd00  29735  vtxdginducedm1  29744  finsumvtxdg2ssteplem4  29749  wlk1walk  29839  wlkp1lem6  29877  iswwlks  30036  wwlknllvtx  30046  wwlksonvtx  30055  wspthnonp  30059  wlkiswwlksupgr2  30077  wwlksnwwlksnon  30115  2pthon3v  30143  umgr2wlk  30149  elwwlks2s3  30151  wwlks2onv  30153  elwwlks2ons3im  30154  isclwwlk  30186  clwwlkccatlem  30191  clwlkclwwlk  30204  wwlksext2clwwlk  30259  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  clwwlknon1  30299  clwwlknon1nloop  30301  clwwlknon2x  30305  1pthon2v  30355  uhgr3cyclex  30384  isconngr  30391  isconngr1  30392  eucrctshift  30445  frgrnbnb  30495  frgrncvvdeqlem1  30501  frgrncvvdeqlem2  30502  frgrncvvdeqlem3  30503  frgrncvvdeqlem9  30509  fusgreghash2wspv  30537  extwwlkfab  30554  numclwwlk1lem2foa  30556  numclwwlk1lem2fo  30560  clwlknon2num  30570  numclwlk2lem2f1o  30581  numclwwlk5lem  30589  topnfbey  30671  isvclem  30780  isnvlem  30813  vsfval  30836  h2hlm  31183  hhcmpl  31403  hhcms  31406  elch0  31457  omlsilem  31605  h1de2ctlem  31758  elspansni  31761  nonbooli  31854  spansncvi  31855  adjeq  32138  cnlnssadj  32283  cnvbraval  32313  brabgaf  32808  2ndresdju  32851  fmptdF  32858  fmptcof2  32859  acunirnmpt  32861  acunirnmpt2  32862  ofpreima  32867  fcnvgreu  32874  fdifsuppconst  32891  1stpreima  32909  2ndpreima  32910  fz2ssnn0  32987  elxrge02  33109  ccatws1f1o  33129  gsumwrd2dccatlem  33257  psgnfzto1stlem  33280  cycpmgcl  33333  elrgspnlem1  33423  elrgspnlem2  33424  elrgspnlem4  33426  elrgspnsubrunlem1  33428  rlocisunit  33457  domnprodeq0  33460  nsgqusf1olem2  33600  nsgqusf1olem3  33601  prmidl0  33637  crngmxidl  33657  opprnsg  33672  rprmirredb  33728  zringfrac  33750  evl1deg2  33773  evl1deg3  33774  ply1degltel  33790  ply1degleel  33791  evlextv  33839  esplyfval3  33869  esplyindfv  33873  esplyfvn  33874  vietalem  33876  fldextrspunlsplem  33970  isconstr  34033  constrsuc  34035  constrconj  34042  submatres  34103  lmat22lem  34114  crefdf  34145  cmppcmp  34155  rspectopn  34164  prsdm  34211  prsrn  34212  xrge0iifcnv  34230  xrge0iifiso  34232  xrge0iifhom  34234  pnfneige0  34248  qqhre  34317  rrhre  34318  esumnul  34345  esumcvgsum  34385  ldgenpisyslem1  34460  measvuni  34511  cntnevol  34525  dya2iocnrect  34578  sibf0  34631  oddpwdc  34651  eulerpartlemd  34663  eulerpartgbij  34669  eulerpartlemgh  34675  isrrvv  34740  coinfliprv  34780  ballotlem7  34833  signswch  34855  hashreprin  34914  chtvalz  34923  circlemethhgt  34937  hgt750lemb  34950  tgoldbachgt  34957  bnj23  35014  bnj158  35025  bnj168  35026  bnj1138  35084  bnj1143  35085  bnj1454  35137  bnj110  35153  bnj882  35221  bnj893  35223  bnj916  35228  bnj970  35242  bnj983  35246  bnj984  35247  bnj1137  35290  bnj1174  35298  bnj1388  35328  bnj1398  35329  r1wf  35392  onvf1odlem4  35449  loop1cycl  35487  subfacp1lem5  35534  satfv1  35713  satfrnmapom  35720  satf0op  35727  satf0n0  35728  fmlafvel  35735  fmlaomn0  35740  fmlan0  35741  satffunlem2lem2  35756  satfv0fvfmla0  35763  satefvfmla0  35768  mrsub0  35866  mrsubccat  35868  mrsubcn  35869  elmrsubrn  35870  msubco  35881  msubvrs  35910  elmthm  35926  mthmblem  35930  ellcsrspsn  35991  elrn3  36112  dfon2lem7  36137  brsset  36237  eltrans  36239  elfix  36251  ellimits  36258  elfuns  36263  elsingles  36266  fvtransport  36382  brcolinear2  36408  fvray  36491  linedegen  36493  fvline  36494  ellines  36502  fwddifn0  36514  elhf  36524  hfninf  36536  rmoeqi  36547  rmoeqbii  36548  reueqi  36549  reueqbii  36550  rabeqbii  36554  iuneq12i  36555  iineq1i  36556  iineq12i  36557  riotaeqbii  36558  ixpeq1i  36560  itgeq12i  36566  cbvprodvw2  36607  fnessref  36717  ttctr  36853  bj-ififc  37025  bj-csbsnlem  37388  bj-elgab  37424  currysetlem1  37432  bj-eltag  37462  bj-sngltag  37468  bj-projun  37479  bj-velpwALT  37538  bj-0nelmpt  37606  bj-opelidres  37653  bj-inftyexpitaudisj  37697  bj-elccinfty  37706  f1omptsnlem  37830  icoreelrnab  37848  relowlpssretop  37858  rdgssun  37872  exrecfnlem  37873  finxpnom  37895  uncov  38100  tan2h  38111  ptrecube  38119  poimirlem25  38144  poimirlem29  38148  poimirlem30  38149  poimirlem31  38150  poimirlem32  38151  cnambfre  38167  ftc1cnnc  38191  sdclem2  38241  sdclem1  38242  fdc  38244  caushft  38260  issmgrpOLD  38362  ismndo  38371  isrngo  38396  isdivrngo  38449  csbcom2fi  38627  elecALTV  38770  brrabga  38840  eldmxrncnvepres  38933  eldmxrncnvepres2  38934  elrels2  38940  blockadjliftmap  38957  dfpre  38975  eupre  38993  eldmcoss  39047  coss0  39068  petseq  39475  dath  40360  diclspsn  41818  dvh4dimlem  42067  dvh2dim  42069  dvh3dim3N  42073  lcfrvalsnN  42165  mapdh6eN  42364  mapdh7dN  42374  mapdh8b  42404  hdmap1l6e  42438  lcmfunnnd  42629  3factsumint1  42638  primrootsunit1  42714  primrootscoprmpow  42716  aks6d1c2lem4  42744  sticksstones2  42764  sticksstones3  42765  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  aks6d1c6lem2  42788  aks6d1c6lem3  42789  redvmptabs  42969  readvrec2  42970  readvrec  42971  frlmfielbas  43122  mhpind  43176  pellex  43412  rmspecnonsq  43484  islmodfg  43646  aaitgo  43739  areaquad  43793  ordeldif1o  43837  naddwordnexlem4  43978  fpwfvss  43988  finona1cl  44029  elcnvcnvintab  44158  elnonrel  44161  elcnvcnvlem  44175  cnvcnvintabd  44176  brfvrcld2  44268  grur1cld  44808  dvgrat  44888  cvgdvgrat  44889  radcnvrat  44890  nznngen  44892  uzmptshftfval  44922  binomcxplemcvg  44930  binomcxplemnotnn0  44932  tpid3gVD  45417  en3lplem2VD  45419  orbitclmpt  45534  wfaxrep  45570  wfaxsep  45571  wfaxpow  45573  wfaxpr  45574  wfaxun  45575  wfac8prim  45578  brpermmodelcnv  45580  nregmodellem  45592  iuneq1i  45664  rexanuz3  45674  eliuniin  45677  eliuniin2  45698  disjinfi  45770  iuneqfzuzlem  45910  allbutfi  45968  eluzelz2  45977  uz0  45986  uzublem  46004  uzid3  46009  elicores  46109  uzinico  46135  climsuselem1  46183  climsuse  46184  islptre  46195  fnlimfvre  46248  limsupresico  46274  limsupvaluz  46282  limsupubuzlem  46286  limsupequzmptlem  46302  liminfresico  46345  cnrefiisplem  46403  stoweidlem14  46588  stoweidlem39  46613  stoweidlem48  46622  stoweidlem51  46625  stoweidlem59  46633  stoweidlem62  46636  wallispilem3  46641  fourierdlem42  46723  fourierdlem62  46742  fourierdlem80  46760  fourierdlem103  46783  fourierdlem104  46784  etransclem26  46834  rrxsnicc  46874  ioorrnopn  46879  ioorrnopnxr  46881  sge00  46950  sge0fodjrnlem  46990  sge0isum  47001  sge0seq  47020  meadjiunlem  47039  carageneld  47076  volicorescl  47127  hoidmv1lelem1  47165  hoidmv1le  47168  hoidmvlelem1  47169  hoidmvlelem3  47171  ovnhoilem2  47176  hoiqssbllem2  47197  opnvonmbllem2  47207  ovolval4lem1  47223  iinhoiicc  47248  vonioolem1  47254  smflimlem1  47345  smflimlem2  47346  smflim  47351  nsssmfmbf  47353  smfresal  47362  smfrec  47363  smfdiv  47371  smfpimbor1lem2  47373  smflim2  47380  smflimmpt  47384  smfinflem  47391  smflimsuplem1  47394  smflimsuplem2  47395  smflimsuplem3  47396  smflimsuplem5  47398  smflimsuplem6  47399  smflimsup  47402  smflimsupmpt  47403  smfliminfmpt  47406  chnerlem1  47458  chnerlem2  47459  tannpoly  47484  sinnpoly  47485  fcores  47661  ndmaovcl  47797  ndmaovcom  47799  ndmaovass  47800  ndmaovdistr  47801  dfatco  47850  otiunsndisjX  47873  fvmptrabdm  47887  ceilhalfelfzo1  47928  modmknepk  47962  elsetpreimafvb  47990  sprsymrelfolem2  48099  sprsymrelf  48101  sprsymrelf1  48102  prpair  48107  prproropf1olem0  48108  paireqne  48117  fmtno4prmfac  48181  dfodd5  48282  sbgoldbo  48409  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  clnbgrcl  48443  clnbgredg  48462  sclnbgrel  48469  isubgredg  48488  uhgrimedgi  48512  isuspgrim0  48516  isuspgrimlem  48517  gricushgr  48539  clnbgrgrimlem  48555  grimedg  48557  usgrgrtrirex  48572  stgrnbgr0  48586  isubgr3stgrlem3  48590  isubgr3stgrlem4  48591  isubgr3stgrlem6  48593  isubgr3stgrlem7  48594  uspgrlimlem2  48611  uspgrlimlem3  48612  grlimedgclnbgr  48617  grlimprclnbgr  48618  grlimprclnbgrvtx  48621  grlimgrtrilem2  48624  usgrexmpl2trifr  48659  gpgvtxel  48669  gpgedgel  48672  gpgusgralem  48678  gpg5order  48682  gpgvtxedg0  48685  gpgvtxedg1  48686  gpgnbgrvtx0  48696  gpgnbgrvtx1  48697  gpg5nbgrvtx03star  48702  gpg5nbgr3star  48703  gpgvtxdg3  48704  gpg5gricstgr3  48712  gpgprismgr4cycllem3  48719  gpgprismgr4cycllem7  48723  gpgprismgr4cycllem8  48724  gpgprismgr4cycllem10  48726  pgnbgreunbgrlem3  48740  pgnbgreunbgrlem6  48746  pgnbgreunbgr  48747  uspgrsprf  48768  uspgrsprf1  48769  uspgrsprfo  48770  ply1sclrmsm  49006  lcoop  49033  lincfsuppcl  49035  linccl  49036  lincvalsng  49038  lincvalpr  49040  lincvalsc0  49043  linc0scn0  49045  lincdifsn  49046  linc1  49047  lincsum  49051  lincscm  49052  lspsslco  49059  snlindsntor  49093  lincresunit3lem2  49102  ldepsnlinclem1  49127  ldepsnlinclem2  49128  prelrrx2  49335  prelrrx2b  49336  rrx2xpref1o  49340  rrx2plord  49342  rrx2linesl  49365  sectrcl  49643  invrcl  49645  initopropdlemlem  49860  initopropd  49864  termopropd  49865  zeroopropd  49866  oppcthin  50059  indthinc  50083  prsthinc  50085  elpglem3  50334