Theorem eleq2i 2857

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  eleq12i  2858  eleqtri  2863  eleq2s  2883  hbxfreq  2895  nfceqi  2924  raleqbii  3338  rexeqbii  3339  rabeqi  3431  rabrabi  3437  reqabi  3441  elab2gw  3639  elab2g  3641  elrabf  3649  elrab3t  3651  elrab2  3656  cbvsbcw  3779  cbvsbcvw  3780  cbvsbc  3781  elin2  4156  elsymdif  4211  noel  4291  eltpg  4654  elunirab  4889  elintrab  4927  disjxiun  5108  exss  5446  otiunsndisj  5505  brabsb  5517  brabga  5520  epelg  5564  pofun  5589  elxp  5686  opeliunxp  5730  opeliun2xp  5731  bropaex12  5754  brab2a  5756  elcnv  5864  cnv0  5871  dmopabelb  5908  elrnmptg  5953  elres  6021  elimampt  6047  elrid  6050  rninxp  6179  elid  6200  elsuci  6434  elsucg  6435  elsuc2g  6436  elfv  6883  0fv  6926  opabiota  6967  dffv2  6980  fvopab3g  6988  fvmptex  7008  fvopab5  7027  fsneq  7034  fvn0ssdmfun  7073  fveqressseq  7078  f0cli  7097  fmptco  7129  fvrnressn  7164  fvtp0  7205  funfvima  7235  elunirnALT  7255  fliftel  7316  eloprabga  7528  elrnmpo  7555  elimampo  7556  ovid  7560  offval  7693  1st2val  8020  2nd2val  8021  bropopvvv  8091  bropfvvvv  8093  fsplit  8118  xporderlem  8129  frpoins3xpg  8142  frpoins3xp3g  8143  brtpos2  8234  frrlem8  8296  frrlem9  8297  frrlem10  8298  fprresex  8313  issmo  8341  smores3  8346  tfrlem7  8376  tfrlem9  8378  tfrlem9a  8379  tfr2b  8389  tfr2  8391  rdgsuc  8417  frsucmptn  8432  tz7.48-2  8435  el1o  8486  ord2eln012  8488  dif1o  8491  ondif2  8493  oawordeulem  8545  elecg  8745  brecop  8814  erovlem  8817  eceqoveq  8826  mapsncnv  8897  mptelixpg  8939  brsdom  8977  isfi  8978  enssdomOLD  8980  brdom2  8985  xpcomco  9062  brsdom2  9096  en3lplem2  9589  cnfcom2lem  9677  brttrcl2  9690  ttrcltr  9692  rnttrcl  9698  epfrs  9707  r1limg  9750  r1ord  9759  r1ord3  9761  tz9.12lem3  9768  rankvaln  9778  r1elss  9785  rankpwi  9802  ssrankr1  9814  r1val3  9817  r1pw  9824  rankr1b  9843  djur  9921  djuunxp  9923  eldju2ndl  9926  eldju2ndr  9927  isnum2  9947  cardprclem  9981  infxpenlem  10013  alephcard  10070  alephnbtwn  10071  alephnbtwn2  10072  alephord2  10076  alephsdom  10086  dfac3  10121  dfac5lem2  10124  dfac5lem3  10125  dfac5lem5  10127  pwsdompw  10202  cfub  10247  cardcf  10250  cflecard  10251  cfle  10252  cflim2  10262  cofsmo  10268  cfidm  10274  isfin3  10295  isfin5  10298  isfin6  10299  sdom2en01  10301  fin23lem26  10324  fin23lem30  10341  isf32lem5  10356  itunitc1  10419  ituniiun  10421  axdc3lem3  10451  axcclem  10456  axdclem  10518  iunfo  10540  iundom2g  10541  cardidg  10549  konigthlem  10570  alephadd  10579  alephreg  10584  pwcfsdom  10585  cfpwsdom  10586  elgch  10624  fpwwe2lem11  10643  canth4  10649  wunex2  10740  r1tskina  10784  elni  10878  nlt1pi  10908  adderpq  10958  mulerpq  10959  recmulnq  10966  addsrpr  11077  mulsrpr  11078  opelcn  11131  opelreal  11132  elreal  11133  elreal2  11134  0ncn  11135  addcnsr  11137  mulcnsr  11138  xrlenlt  11291  elnn0  12523  elnnne0  12535  un0addcl  12554  un0mulcl  12555  elxnn0  12596  uztrn2  12899  elnnuz  12920  elnn0uz  12921  elq  12992  elxr  13159  elfzm1b  13649  elfz0lmr  13831  uzrdgfni  14014  fzennn  14024  ser0  14110  hash2pwpr  14533  iswrd  14572  pfxccatpfx1  14797  s3iunsndisj  15031  sumz  15798  sumss  15800  fsumcvg3  15805  abscvgcvg  15896  isumshft  15918  prodf1  15970  prodeq1i  15995  zprod  16016  prod1  16023  prodss  16026  prodsn  16041  prodsnf  16043  bpolydiflem  16132  bpoly2  16135  bpoly3  16136  bpoly4  16137  ruclem6  16315  divides  16336  dvdsflip  16399  pwp1fsum  16473  sadc0  16536  eulerthlem2  16865  prm23lt5  16898  4sqlem2  17033  4sqlem12  17040  vdwpc  17064  xpscf  17643  cidpropd  17790  oppcsect  17859  funcpropd  17983  natpropd  18060  dfinito2  18084  dftermo2  18085  initoeu2lem0  18094  arwhoma  18126  eldmcoa  18146  pospo  18423  psss  18660  ex-chn1  18717  ex-chn2  18718  ismgmn0  18724  gsumpropd2lem  18771  elefmndbas  18971  smndex1basss  19006  smndex1mgm  19008  pwmnd  19045  dfgrp2e  19076  mulgfval  19181  eqg0subg  19313  cycsubmel  19317  ghmeqker  19359  elcntr  19446  cntri  19448  cntzsgrpcl  19450  oppgsubg  19479  fvcosymgeq  19545  symgfixels  19550  pmtrfrn  19574  efgsfo  19855  efgrelexlemb  19866  lt6abl  20011  dmdprd  20116  dprdval  20121  dprdw  20128  srgbinomlem4  20357  isnirred  20550  isrhm  20609  isdrng3lem1  20903  issrng  20999  lspexchn2  21307  lspindp2l  21310  lspindp2  21311  lbsextlem2  21335  rnglidl1  21410  df2idl2  21448  2idlss  21453  rngqiprngimfo  21493  prmidl0  21530  cnfldfun  21588  pzriprnglem3  21685  pzriprnglem4  21686  pzriprnglem7  21689  pzriprnglem8  21690  pzriprnglem9  21691  pzriprnglem12  21694  pzriprnglem14  21696  dsmmelbas  21941  frlmbas3  21978  lindsind2  22021  islindf4  22040  psrbagf  22120  evlslem4  22279  psdmul  22381  ply1bascl2  22416  cply1mul  22508  lply1binom  22522  matsubgcell  22643  matinvgcell  22644  matvscacell  22645  matepmcl  22671  matepm2cl  22672  scmatscm  22722  smatvscl  22733  marrepcl  22773  marepvcl  22778  mulmarep1el  22781  mulmarep1gsum1  22782  mulmarep1gsum2  22783  submabas  22787  m1detdiag  22806  mdetdiag  22808  m2detleib  22840  gsummatr01lem3  22866  gsummatr01  22868  smadiadetlem4  22878  slesolinv  22889  slesolinvbi  22890  slesolex  22891  cramerimplem2  22893  pmatcoe1fsupp  22910  mat2pmatbas  22935  mat2pmatmul  22940  mat2pmatlin  22944  decpmatmul  22981  monmatcollpw  22988  pm2mpf1  23008  pm2mpghm  23025  istps  23143  mretopd  23301  neiptopuni  23339  lpdifsn  23352  restcls  23390  perfopn  23394  pnfnei  23429  mnfnei  23430  lmss  23507  hauscmplem  23615  is2ndc  23655  2ndcdisj  23666  hausnlly  23703  txuni2  23775  ptpjpre1  23781  elpt  23782  dfac14  23828  xkococn  23870  fbasrn  24094  fin1aufil  24142  elfm2  24158  elfm3  24160  fbflim  24186  flffbas  24205  cnpflf2  24210  fclsbas  24231  efmndtmd  24311  tsmssubm  24353  iscusp2  24511  imasdsf1olem  24583  metustel  24760  metuel2  24775  isnghm  24933  opnreen  25042  iccpnfcnv  25156  ehleudisval  25631  ehl1eudis  25632  ehl2eudis  25634  minveclem3b  25640  ovoliunlem1  25714  ioombl1lem4  25773  subopnmbl  25816  vitalilem2  25821  vitalilem3  25822  mbfimaopnlem  25867  mbfimaopn2  25869  itg2l  25941  dvply1  26498  vieta1lem1  26524  vieta1lem2  26525  elaa  26530  taylthlem2  26590  abelthlem6  26652  abelthlem9  26656  sinq34lt0t  26727  ellogrn  26777  dvrelog  26855  ellogdm  26857  logtayl2  26880  cxpcn3lem  26965  cxpcn3  26966  1cubr  27060  atandm  27094  atanf  27098  reasinsin  27114  atans2  27149  dmarea  27175  xrlimcnp  27186  amgmlem  27207  ppiublem1  27419  lgsdir2lem2  27543  gausslemma2dlem1a  27582  lgsquadlem1  27597  lgsquadlem2  27598  2sqlem1  27634  rpvmasum2  27729  madeval2  28079  newval  28081  leftval  28095  rightval  28096  lltr  28108  madess  28112  oldssmade  28113  oldss  28116  lrold  28143  addsproplem2  28216  addsproplem4  28218  addsproplem6  28220  negsproplem4  28277  negsproplem6  28279  precsexlem10  28462  precsexlem11  28463  ltonold  28507  elnns  28586  elzs  28630  edgiedgb  29461  isuhgr  29467  isushgr  29468  isupgr  29491  isumgr  29502  umgredg  29545  umgrpredgv  29547  umgredgne  29552  umgredgnlp  29554  isuspgr  29562  isusgr  29563  ausgrusgri  29578  usgredgppr  29606  edgssv2  29608  uspgredg2vlem  29633  uspgredg2v  29634  ushgredgedg  29639  ushgredgedgloop  29641  griedg0ssusgr  29675  uhgrissubgr  29685  subumgredg2  29695  uhgrspansubgrlem  29700  umgrres1lem  29720  upgrres1  29723  nbgrcl  29745  nbuhgr  29753  nbuhgr2vtx1edgblem  29761  nbupgrres  29774  edgnbusgreu  29777  nbusgredgeu0  29778  nbusgrf1o0  29779  hashnbusgrnn0  29786  nbupgruvtxres  29817  cffldtocusgr  29857  cusgrfilem2  29866  vtxdg0v  29883  vtxduhgr0nedg  29902  uhgrvd00  29944  vtxdginducedm1  29953  finsumvtxdg2ssteplem4  29958  wlk1walk  30048  wlkp1lem6  30086  iswwlks  30254  wwlknllvtx  30264  wwlksonvtx  30273  wspthnonp  30277  wlkiswwlksupgr2  30295  wwlksnwwlksnon  30333  2pthon3v  30361  umgr2wlk  30367  elwwlks2s3  30369  wwlks2onv  30371  elwwlks2ons3im  30372  isclwwlk  30404  clwwlkccatlem  30409  clwlkclwwlk  30422  wwlksext2clwwlk  30477  hashecclwwlkn1  30497  umgrhashecclwwlk  30498  clwwlknon1  30517  clwwlknon1nloop  30519  clwwlknon2x  30523  loop1cycl  30573  1pthon2v  30577  uhgr3cyclex  30606  isconngr  30613  isconngr1  30614  eucrctshift  30667  frgrnbnb  30717  frgrncvvdeqlem1  30723  frgrncvvdeqlem2  30724  frgrncvvdeqlem3  30725  frgrncvvdeqlem9  30731  fusgreghash2wspv  30759  extwwlkfab  30776  numclwwlk1lem2foa  30778  numclwwlk1lem2fo  30782  clwlknon2num  30792  numclwlk2lem2f1o  30803  numclwwlk5lem  30811  topnfbey  30893  isvclem  31002  isnvlem  31035  vsfval  31058  h2hlm  31405  hhcmpl  31625  hhcms  31628  elch0  31679  omlsilem  31827  h1de2ctlem  31980  elspansni  31983  nonbooli  32076  spansncvi  32077  adjeq  32360  cnlnssadj  32505  cnvbraval  32535  brabgaf  33024  2ndresdju  33067  fmptdf2  33074  fmptcof2  33075  acunirnmpt  33077  acunirnmpt2  33078  ofpreima  33083  fcnvgreu  33090  fdifsuppconst  33107  1stpreima  33125  2ndpreima  33126  fz2ssnn0  33202  elxrge02  33323  ccatws1f1o  33339  gsumwrd2dccatlem  33463  psgnfzto1stlem  33486  cycpmgcl  33539  elrgspnlem1  33628  elrgspnlem2  33629  elrgspnlem4  33631  elrgspnsubrunlem1  33633  rlocisunit  33662  domnprodeq0  33665  nsgqusf1olem2  33789  nsgqusf1olem3  33790  crngmxidl  33818  opprnsg  33832  rprmirredb  33888  zringfrac  33910  evl1deg2  33933  evl1deg3  33934  ply1degltel  33950  ply1degleel  33951  evlextv  33998  esplyfval3  34028  esplyindfv  34032  esplyfvn  34033  vietalem  34035  fldextrspunlsplem  34129  isconstr  34192  constrsuc  34194  constrconj  34201  submatres  34262  lmat22lem  34273  crefdf  34304  cmppcmp  34314  rspectopn  34323  prsdm  34370  prsrn  34371  xrge0iifcnv  34389  xrge0iifiso  34391  xrge0iifhom  34393  pnfneige0  34407  qqhre  34476  rrhre  34477  esumnul  34504  esumcvgsum  34544  ldgenpisyslem1  34620  measvuni  34671  cntnevol  34685  dya2iocnrect  34738  sibf0  34791  oddpwdc  34811  eulerpartlemd  34823  eulerpartgbij  34829  eulerpartlemgh  34835  isrrvv  34900  coinfliprv  34940  ballotlem7  34993  signswch  35015  hashreprin  35074  chtvalz  35083  circlemethhgt  35097  hgt750lemb  35110  tgoldbachgt  35117  bnj23  35174  bnj158  35185  bnj168  35186  bnj1138  35244  bnj1143  35245  bnj1454  35297  bnj110  35313  bnj882  35381  bnj893  35383  bnj916  35388  bnj970  35402  bnj983  35406  bnj984  35407  bnj1137  35450  bnj1174  35458  bnj1388  35488  bnj1398  35489  r1wf  35549  onrankid  35554  onvf1odlem4  35649  subfacp1lem5  35715  satfv1  35894  satfrnmapom  35901  satf0op  35908  satf0n0  35909  fmlafvel  35916  fmlaomn0  35921  fmlan0  35922  satffunlem2lem2  35937  satfv0fvfmla0  35944  satefvfmla0  35949  mrsub0  36047  mrsubccat  36049  mrsubcn  36050  elmrsubrn  36051  msubco  36062  msubvrs  36091  elmthm  36107  mthmblem  36111  ellcsrspsn  36172  elrn3  36293  dfon2lem7  36318  brsset  36418  eltrans  36420  elfix  36432  ellimits  36439  elfuns  36444  elsingles  36447  fvtransport  36563  brcolinear2  36589  fvray  36672  linedegen  36674  fvline  36675  ellines  36683  fwddifn0  36695  elhf  36705  hfninf  36717  rmoeqi  36758  rmoeqbii  36759  reueqi  36760  reueqbii  36761  rabeqbii  36765  iuneq12i  36766  iineq1i  36767  iineq12i  36768  riotaeqbii  36769  ixpeq1i  36771  itgeq12i  36777  cbvprodvw2  36818  fnessref  36927  ttctr  37063  bj-ififc  37234  bj-csbsnlem  37597  bj-elgab  37634  currysetlem1  37642  bj-eltag  37672  bj-sngltag  37678  bj-projun  37689  bj-velpwALT  37748  bj-0nelmpt  37817  bj-opelidres  37864  bj-inftyexpitaudisj  37908  bj-elccinfty  37917  f1omptsnlem  38041  icoreelrnab  38059  relowlpssretop  38069  rdgssun  38083  exrecfnlem  38084  finxpnom  38106  uncov  38311  tan2h  38322  ptrecube  38330  poimirlem25  38355  poimirlem29  38359  poimirlem30  38360  poimirlem31  38361  poimirlem32  38362  cnambfre  38378  ftc1cnnc  38402  sdclem2  38453  sdclem1  38454  fdc  38456  caushft  38472  issmgrpOLD  38574  ismndo  38583  isrngo  38608  isdivrngo  38661  csbcom2fi  38837  elecALTV  38980  brrabga  39050  eldmxrncnvepres  39143  eldmxrncnvepres2  39144  elrels2  39150  blockadjliftmap  39167  dfpre  39185  eupre  39203  eldmcoss  39257  coss0  39278  petseq  39685  dath  40570  diclspsn  42028  dvh4dimlem  42277  dvh2dim  42279  dvh3dim3N  42283  lcfrvalsnN  42375  mapdh6eN  42574  mapdh7dN  42584  mapdh8b  42614  hdmap1l6e  42648  lcmfunnnd  42839  3factsumint1  42848  primrootsunit1  42924  primrootscoprmpow  42926  aks6d1c2lem4  42954  sticksstones2  42974  sticksstones3  42975  sticksstones10  42982  sticksstones12a  42984  sticksstones12  42985  aks6d1c6lem2  42998  aks6d1c6lem3  42999  redvmptabs  43181  readvrec2  43182  readvrec  43183  frlmfielbas  43334  mhpind  43386  pellex  43622  rmspecnonsq  43694  islmodfg  43856  aaitgo  43949  areaquad  44003  ordeldif1o  44047  naddwordnexlem4  44188  fpwfvss  44198  finona1cl  44239  elcnvcnvintab  44368  elnonrel  44371  elcnvcnvlem  44385  cnvcnvintabd  44386  brfvrcld2  44478  grur1cld  45016  dvgrat  45082  cvgdvgrat  45083  radcnvrat  45084  nznngen  45086  uzmptshftfval  45116  binomcxplemcvg  45124  binomcxplemnotnn0  45126  tpid3gVD  45610  en3lplem2VD  45612  orbitclmpt  45727  wfaxrep  45763  wfaxsep  45764  wfaxpow  45766  wfaxpr  45767  wfaxun  45768  wfac8prim  45771  brpermmodelcnv  45773  nregmodellem  45785  iuneq1i  45864  rexanuz3  45874  eliuniin  45877  eliuniin2  45898  disjinfi  45970  iuneqfzuzlem  46110  allbutfi  46168  eluzelz2  46177  uz0  46186  uzublem  46204  uzid3  46209  elicores  46309  uzinico  46335  climsuselem1  46383  climsuse  46384  islptre  46395  fnlimfvre  46448  limsupresico  46474  limsupvaluz  46482  limsupubuzlem  46486  limsupequzmptlem  46502  liminfresico  46545  cnrefiisplem  46603  stoweidlem14  46788  stoweidlem39  46813  stoweidlem48  46822  stoweidlem51  46825  stoweidlem59  46833  stoweidlem62  46836  wallispilem3  46841  fourierdlem42  46923  fourierdlem62  46942  fourierdlem80  46960  fourierdlem103  46983  fourierdlem104  46984  etransclem26  47034  rrxsnicc  47074  ioorrnopn  47079  ioorrnopnxr  47081  sge00  47150  sge0fodjrnlem  47190  sge0isum  47201  sge0seq  47220  meadjiunlem  47239  carageneld  47276  volicorescl  47327  hoidmv1lelem1  47365  hoidmv1le  47368  hoidmvlelem1  47369  hoidmvlelem3  47371  ovnhoilem2  47376  hoiqssbllem2  47397  opnvonmbllem2  47407  ovolval4lem1  47423  iinhoiicc  47448  vonioolem1  47454  smflimlem1  47545  smflimlem2  47546  smflim  47551  nsssmfmbf  47553  smfresal  47562  smfrec  47563  smfdiv  47571  smfpimbor1lem2  47573  smflim2  47580  smflimmpt  47584  smfinflem  47591  smflimsuplem1  47594  smflimsuplem2  47595  smflimsuplem3  47596  smflimsuplem5  47598  smflimsuplem6  47599  smflimsup  47602  smflimsupmpt  47603  smfliminfmpt  47606  chnerlem1  47658  chnerlem2  47659  tannpoly  47687  sinnpoly  47688  fcores  47864  ndmaovcl  48000  ndmaovcom  48002  ndmaovass  48003  ndmaovdistr  48004  dfatco  48053  otiunsndisjX  48076  fvmptrabdm  48090  ceilhalfelfzo1  48131  modmknepk  48165  elsetpreimafvb  48193  sprsymrelfolem2  48302  sprsymrelf  48304  sprsymrelf1  48305  prpair  48310  prproropf1olem0  48311  paireqne  48320  fmtno4prmfac  48384  dfodd5  48485  sbgoldbo  48612  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  clnbgrcl  48646  clnbgredg  48665  sclnbgrel  48672  isubgredg  48691  uhgrimedgi  48715  isuspgrim0  48719  isuspgrimlem  48720  gricushgr  48742  clnbgrgrimlem  48758  grimedg  48760  usgrgrtrirex  48775  stgrnbgr0  48789  isubgr3stgrlem3  48793  isubgr3stgrlem4  48794  isubgr3stgrlem6  48796  isubgr3stgrlem7  48797  uspgrlimlem2  48814  uspgrlimlem3  48815  grlimedgclnbgr  48820  grlimprclnbgr  48821  grlimprclnbgrvtx  48824  grlimgrtrilem2  48827  usgrexmpl2trifr  48862  gpgvtxel  48872  gpgedgel  48875  gpgusgralem  48881  gpg5order  48885  gpgvtxedg0  48888  gpgvtxedg1  48889  gpgnbgrvtx0  48899  gpgnbgrvtx1  48900  gpg5nbgrvtx03star  48905  gpg5nbgr3star  48906  gpgvtxdg3  48907  gpg5gricstgr3  48915  gpgprismgr4cycllem3  48922  gpgprismgr4cycllem7  48926  gpgprismgr4cycllem8  48927  gpgprismgr4cycllem10  48929  pgnbgreunbgrlem3  48943  pgnbgreunbgrlem6  48949  pgnbgreunbgr  48950  uspgrsprf  48971  uspgrsprf1  48972  uspgrsprfo  48973  dfidom2  49167  ply1sclrmsm  49223  lcoop  49250  lincfsuppcl  49252  linccl  49253  lincvalsng  49255  lincvalpr  49257  lincvalsc0  49260  linc0scn0  49262  lincdifsn  49263  linc1  49264  lincsum  49268  lincscm  49269  lspsslco  49276  snlindsntor  49310  lincresunit3lem2  49319  ldepsnlinclem1  49344  ldepsnlinclem2  49345  prelrrx2  49552  prelrrx2b  49553  rrx2xpref1o  49557  rrx2plord  49559  rrx2linesl  49582  sectrcl  49859  invrcl  49861  initopropdlemlem  50076  initopropd  50080  termopropd  50081  zeroopropd  50082  oppcthin  50275  indthinc  50299  prsthinc  50301  elpglem3  50550