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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  eleq12i  2827  eleqtri  2832  eleq2s  2852  hbxfreq  2864  nfceqi  2893  raleqbii  3312  rexeqbii  3313  rabeqi  3410  rabrabi  3416  reqabi  3420  elab2gw  3631  elab2g  3633  elrabf  3641  elrab3t  3643  elrab2  3647  cbvsbcw  3771  cbvsbcvw  3772  cbvsbc  3773  elin2  4153  elsymdif  4208  noel  4288  eltpg  4641  elunirab  4876  elintrab  4913  disjxiun  5093  exss  5409  otiunsndisj  5466  brabsb  5477  brabga  5480  epelg  5523  pofun  5548  elxp  5645  opeliunxp  5689  opeliun2xp  5690  bropaex12  5713  brab2a  5715  elcnv  5823  dmopabelb  5863  elrnmptg  5908  elres  5977  elimampt  6000  elrid  6003  cnv0  6095  rninxp  6135  elid  6155  elsuci  6384  elsucg  6385  elsuc2g  6386  elfv  6830  0fv  6873  opabiota  6914  dffv2  6927  fvopab3g  6934  fvmptex  6953  fvopab5  6972  fvn0ssdmfun  7017  fveqressseq  7022  f0cli  7041  fmptco  7072  fvrnressn  7104  funfvima  7174  elunirnALT  7196  fliftel  7253  eloprabga  7465  elrnmpo  7492  elimampo  7493  ovid  7497  offval  7629  1st2val  7959  2nd2val  7960  bropopvvv  8030  bropfvvvv  8032  fsplit  8057  xporderlem  8067  frpoins3xpg  8080  frpoins3xp3g  8081  brtpos2  8172  frrlem8  8233  frrlem9  8234  frrlem10  8235  fprresex  8250  issmo  8278  smores3  8283  tfrlem7  8312  tfrlem9  8314  tfrlem9a  8315  tfr2b  8325  tfr2  8327  rdgsuc  8353  frsucmptn  8368  tz7.48-2  8371  el1o  8420  ord2eln012  8422  dif1o  8425  ondif2  8427  oawordeulem  8479  elecg  8677  brecop  8745  erovlem  8748  eceqoveq  8757  mapsncnv  8829  mptelixpg  8871  brsdom  8909  isfi  8910  enssdomOLD  8912  brdom2  8917  xpcomco  8993  brsdom2  9027  en3lplem2  9520  cnfcom2lem  9608  brttrcl2  9621  ttrcltr  9623  rnttrcl  9629  epfrs  9638  r1limg  9681  r1ord  9690  r1ord3  9692  tz9.12lem3  9699  rankvaln  9709  r1elss  9716  rankpwi  9733  ssrankr1  9745  r1val3  9748  r1pw  9755  rankr1b  9774  djur  9829  djuunxp  9831  eldju2ndl  9834  eldju2ndr  9835  isnum2  9855  cardprclem  9889  infxpenlem  9921  alephcard  9978  alephnbtwn  9979  alephnbtwn2  9980  alephord2  9984  alephsdom  9994  dfac3  10029  dfac5lem2  10032  dfac5lem3  10033  dfac5lem5  10035  pwsdompw  10111  cfub  10157  cardcf  10160  cflecard  10161  cfle  10162  cflim2  10171  cofsmo  10177  cfidm  10183  isfin3  10204  isfin5  10207  isfin6  10208  sdom2en01  10210  fin23lem26  10233  fin23lem30  10250  isf32lem5  10265  itunitc1  10328  ituniiun  10330  axdc3lem3  10360  axcclem  10365  axdclem  10427  iunfo  10447  iundom2g  10448  cardidg  10456  konigthlem  10477  alephadd  10486  alephreg  10491  pwcfsdom  10492  cfpwsdom  10493  elgch  10531  fpwwe2lem11  10550  canth4  10556  wunex2  10647  r1tskina  10691  elni  10785  nlt1pi  10815  adderpq  10865  mulerpq  10866  recmulnq  10873  addsrpr  10984  mulsrpr  10985  opelcn  11038  opelreal  11039  elreal  11040  elreal2  11041  0ncn  11042  addcnsr  11044  mulcnsr  11045  xrlenlt  11195  elnn0  12401  elnnne0  12413  un0addcl  12432  un0mulcl  12433  elxnn0  12474  uztrn2  12768  elnnuz  12789  elnn0uz  12790  elq  12861  elxr  13028  elfzm1b  13516  elfz0lmr  13697  uzrdgfni  13879  fzennn  13889  ser0  13975  hash2pwpr  14397  iswrd  14436  pfxccatpfx1  14657  s3iunsndisj  14889  sumz  15643  sumss  15645  fsumcvg3  15650  abscvgcvg  15740  isumshft  15760  prodf1  15812  prodeq1i  15837  zprod  15858  prod1  15865  prodss  15868  prodsn  15883  prodsnf  15885  bpolydiflem  15975  bpoly2  15978  bpoly3  15979  bpoly4  15980  ruclem6  16158  divides  16179  dvdsflip  16242  pwp1fsum  16316  sadc0  16379  eulerthlem2  16707  prm23lt5  16740  4sqlem2  16875  4sqlem12  16882  vdwpc  16906  xpscf  17484  cidpropd  17631  oppcsect  17700  funcpropd  17824  natpropd  17901  dfinito2  17925  dftermo2  17926  initoeu2lem0  17935  arwhoma  17967  eldmcoa  17987  pospo  18264  psss  18501  ex-chn1  18558  ex-chn2  18559  ismgmn0  18565  gsumpropd2lem  18602  elefmndbas  18796  smndex1basss  18828  smndex1mgm  18830  pwmnd  18860  dfgrp2e  18891  mulgfval  18997  eqg0subg  19123  cycsubmel  19127  ghmeqker  19170  elcntr  19257  cntri  19259  cntzsgrpcl  19261  oppgsubg  19290  fvcosymgeq  19356  symgfixels  19361  pmtrfrn  19385  efgsfo  19666  efgrelexlemb  19677  lt6abl  19822  dmdprd  19927  dprdval  19932  dprdw  19939  srgbinomlem4  20162  isnirred  20354  isrhm  20412  issrng  20775  lspexchn2  21084  lspindp2l  21087  lspindp2  21088  lbsextlem2  21112  rnglidl1  21185  df2idl2  21210  2idlss  21215  rngqiprngimfo  21254  cnfldfun  21321  cnfldfunOLD  21334  pzriprnglem3  21436  pzriprnglem4  21437  pzriprnglem7  21440  pzriprnglem8  21441  pzriprnglem9  21442  pzriprnglem12  21445  pzriprnglem14  21447  dsmmelbas  21692  frlmbas3  21729  lindsind2  21772  islindf4  21791  psrbagf  21872  evlslem4  22029  psdmul  22107  ply1bascl2  22143  cply1mul  22238  lply1binom  22252  matsubgcell  22376  matinvgcell  22377  matvscacell  22378  matepmcl  22404  matepm2cl  22405  scmatscm  22455  smatvscl  22466  marrepcl  22506  marepvcl  22511  mulmarep1el  22514  mulmarep1gsum1  22515  mulmarep1gsum2  22516  submabas  22520  m1detdiag  22539  mdetdiag  22541  m2detleib  22573  gsummatr01lem3  22599  gsummatr01  22601  smadiadetlem4  22611  slesolinv  22622  slesolinvbi  22623  slesolex  22624  cramerimplem2  22626  pmatcoe1fsupp  22643  mat2pmatbas  22668  mat2pmatmul  22673  mat2pmatlin  22677  decpmatmul  22714  monmatcollpw  22721  pm2mpf1  22741  pm2mpghm  22758  istps  22876  mretopd  23034  neiptopuni  23072  lpdifsn  23085  restcls  23123  perfopn  23127  pnfnei  23162  mnfnei  23163  lmss  23240  hauscmplem  23348  is2ndc  23388  2ndcdisj  23398  hausnlly  23435  txuni2  23507  ptpjpre1  23513  elpt  23514  dfac14  23560  xkococn  23602  fbasrn  23826  fin1aufil  23874  elfm2  23890  elfm3  23892  fbflim  23918  flffbas  23937  cnpflf2  23942  fclsbas  23963  efmndtmd  24043  tsmssubm  24085  iscusp2  24243  imasdsf1olem  24315  metustel  24492  metuel2  24507  isnghm  24665  opnreen  24774  iccpnfcnv  24896  ehleudisval  25373  ehl1eudis  25374  ehl2eudis  25376  minveclem3b  25382  ovoliunlem1  25457  ioombl1lem4  25516  subopnmbl  25559  vitalilem2  25564  vitalilem3  25565  mbfimaopnlem  25610  mbfimaopn2  25612  itg2l  25684  dvply1  26245  vieta1lem1  26272  vieta1lem2  26273  elaa  26278  taylthlem2  26336  taylthlem2OLD  26337  abelthlem6  26400  abelthlem9  26404  sinq34lt0t  26472  ellogrn  26522  dvrelog  26600  ellogdm  26602  logtayl2  26625  cxpcn3lem  26711  cxpcn3  26712  1cubr  26806  atandm  26840  atanf  26844  reasinsin  26860  atans2  26895  dmarea  26921  xrlimcnp  26932  amgmlem  26954  ppiublem1  27167  lgsdir2lem2  27291  gausslemma2dlem1a  27330  lgsquadlem1  27345  lgsquadlem2  27346  2sqlem1  27382  rpvmasum2  27477  madeval2  27821  newval  27823  leftval  27831  rightval  27832  lltropt  27844  madess  27848  oldssmade  27849  oldss  27850  lrold  27869  addsproplem2  27940  addsproplem4  27942  addsproplem6  27944  negsproplem4  28000  negsproplem6  28002  precsexlem10  28184  precsexlem11  28185  sltonold  28229  elnns  28300  elzs  28342  edgiedgb  29076  isuhgr  29082  isushgr  29083  isupgr  29106  isumgr  29117  umgredg  29160  umgrpredgv  29162  umgredgne  29167  umgredgnlp  29169  isuspgr  29174  isusgr  29175  ausgrusgri  29190  usgredgppr  29218  edgssv2  29220  uspgredg2vlem  29245  uspgredg2v  29246  ushgredgedg  29251  ushgredgedgloop  29253  griedg0ssusgr  29287  uhgrissubgr  29297  subumgredg2  29307  uhgrspansubgrlem  29312  umgrres1lem  29332  upgrres1  29335  nbgrcl  29357  nbuhgr  29365  nbuhgr2vtx1edgblem  29373  nbupgrres  29386  edgnbusgreu  29389  nbusgredgeu0  29390  nbusgrf1o0  29391  hashnbusgrnn0  29398  nbupgruvtxres  29429  cffldtocusgr  29469  cffldtocusgrOLD  29470  cusgrfilem2  29479  vtxdg0v  29496  vtxduhgr0nedg  29515  uhgrvd00  29557  vtxdginducedm1  29566  finsumvtxdg2ssteplem4  29571  wlk1walk  29661  wlkp1lem6  29699  iswwlks  29858  wwlknllvtx  29868  wwlksonvtx  29877  wspthnonp  29881  wlkiswwlksupgr2  29899  wwlksnwwlksnon  29937  2pthon3v  29965  umgr2wlk  29971  elwwlks2s3  29973  wwlks2onv  29975  elwwlks2ons3im  29976  isclwwlk  30008  clwwlkccatlem  30013  clwlkclwwlk  30026  wwlksext2clwwlk  30081  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  clwwlknon1  30121  clwwlknon1nloop  30123  clwwlknon2x  30127  1pthon2v  30177  uhgr3cyclex  30206  isconngr  30213  isconngr1  30214  eucrctshift  30267  frgrnbnb  30317  frgrncvvdeqlem1  30323  frgrncvvdeqlem2  30324  frgrncvvdeqlem3  30325  frgrncvvdeqlem9  30331  fusgreghash2wspv  30359  extwwlkfab  30376  numclwwlk1lem2foa  30378  numclwwlk1lem2fo  30382  clwlknon2num  30392  numclwlk2lem2f1o  30403  numclwwlk5lem  30411  topnfbey  30493  isvclem  30601  isnvlem  30634  vsfval  30657  h2hlm  31004  hhcmpl  31224  hhcms  31227  elch0  31278  omlsilem  31426  h1de2ctlem  31579  elspansni  31582  nonbooli  31675  spansncvi  31676  adjeq  31959  cnlnssadj  32104  cnvbraval  32134  brabgaf  32633  2ndresdju  32676  fmptdF  32683  fmptcof2  32684  acunirnmpt  32686  acunirnmpt2  32687  ofpreima  32692  fcnvgreu  32700  fdifsuppconst  32717  1stpreima  32735  2ndpreima  32736  fz2ssnn0  32814  elxrge02  32962  ccatws1f1o  32982  gsumwrd2dccatlem  33108  psgnfzto1stlem  33131  cycpmgcl  33184  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem4  33276  elrgspnsubrunlem1  33278  domnprodeq0  33307  nsgqusf1olem2  33444  nsgqusf1olem3  33445  prmidl0  33480  crngmxidl  33499  opprnsg  33514  rprmirredb  33562  zringfrac  33584  evl1deg2  33607  evl1deg3  33608  ply1degltel  33624  ply1degleel  33625  evlextv  33656  esplyfval3  33679  esplyindfv  33681  esplyfvn  33682  vietalem  33684  fldextrspunlsplem  33779  isconstr  33842  constrsuc  33844  constrconj  33851  submatres  33912  lmat22lem  33923  crefdf  33954  cmppcmp  33964  rspectopn  33973  prsdm  34020  prsrn  34021  xrge0iifcnv  34039  xrge0iifiso  34041  xrge0iifhom  34043  pnfneige0  34057  qqhre  34126  rrhre  34127  esumnul  34154  esumcvgsum  34194  ldgenpisyslem1  34269  measvuni  34320  cntnevol  34334  dya2iocnrect  34387  sibf0  34440  oddpwdc  34460  eulerpartlemd  34472  eulerpartgbij  34478  eulerpartlemgh  34484  isrrvv  34549  coinfliprv  34589  ballotlem7  34642  signswch  34667  hashreprin  34726  chtvalz  34735  circlemethhgt  34749  hgt750lemb  34762  tgoldbachgt  34769  bnj23  34823  bnj158  34834  bnj168  34835  bnj1138  34893  bnj1143  34895  bnj1454  34947  bnj110  34963  bnj882  35031  bnj893  35033  bnj916  35038  bnj970  35052  bnj983  35056  bnj984  35057  bnj1137  35100  bnj1174  35108  bnj1388  35138  bnj1398  35139  r1wf  35201  onvf1odlem4  35249  loop1cycl  35280  subfacp1lem5  35327  satfv1  35506  satfrnmapom  35513  satf0op  35520  satf0n0  35521  fmlafvel  35528  fmlaomn0  35533  fmlan0  35534  satffunlem2lem2  35549  satfv0fvfmla0  35556  satefvfmla0  35561  mrsub0  35659  mrsubccat  35661  mrsubcn  35662  elmrsubrn  35663  msubco  35674  msubvrs  35703  elmthm  35719  mthmblem  35723  ellcsrspsn  35784  elrn3  35905  dfon2lem7  35930  brsset  36030  eltrans  36032  elfix  36044  ellimits  36051  elfuns  36056  elsingles  36059  fvtransport  36175  brcolinear2  36201  fvray  36284  linedegen  36286  fvline  36287  ellines  36295  fwddifn0  36307  elhf  36317  hfninf  36329  rmoeqi  36330  rmoeqbii  36331  reueqi  36332  reueqbii  36333  rabeqbii  36337  iuneq12i  36338  iineq1i  36339  iineq12i  36340  riotaeqbii  36341  ixpeq1i  36343  itgeq12i  36349  cbvprodvw2  36390  fnessref  36500  bj-ififc  36725  bj-csbsnlem  37047  bj-elgab  37083  currysetlem1  37091  bj-eltag  37121  bj-sngltag  37127  bj-projun  37138  bj-velpwALT  37197  bj-0nelmpt  37260  bj-opelidres  37305  bj-inftyexpitaudisj  37349  bj-elccinfty  37358  f1omptsnlem  37480  icoreelrnab  37498  relowlpssretop  37508  rdgssun  37522  exrecfnlem  37523  finxpnom  37545  uncov  37741  tan2h  37752  ptrecube  37760  poimirlem25  37785  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  cnambfre  37808  ftc1cnnc  37832  sdclem2  37882  sdclem1  37883  fdc  37885  caushft  37901  issmgrpOLD  38003  ismndo  38012  isrngo  38037  isdivrngo  38090  csbcom2fi  38268  elecALTV  38403  brrabga  38473  eldmxrncnvepres  38558  eldmxrncnvepres2  38559  elrels2  38565  blockadjliftmap  38572  dfpre  38589  eupre  38606  eldmcoss  38660  coss0  38681  dath  39935  diclspsn  41393  dvh4dimlem  41642  dvh2dim  41644  dvh3dim3N  41648  lcfrvalsnN  41740  mapdh6eN  41939  mapdh7dN  41949  mapdh8b  41979  hdmap1l6e  42013  lcmfunnnd  42205  3factsumint1  42214  primrootsunit1  42290  primrootscoprmpow  42292  aks6d1c2lem4  42320  sticksstones2  42340  sticksstones3  42341  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  aks6d1c6lem2  42364  aks6d1c6lem3  42365  redvmptabs  42557  readvrec2  42558  readvrec  42559  frlmfielbas  42697  mhpind  42779  pellex  43019  rmspecnonsq  43091  islmodfg  43253  aaitgo  43346  areaquad  43400  ordeldif1o  43444  naddwordnexlem4  43585  fpwfvss  43595  finona1cl  43636  elcnvcnvintab  43765  elnonrel  43768  elcnvcnvlem  43782  cnvcnvintabd  43783  brfvrcld2  43875  grur1cld  44415  dvgrat  44495  cvgdvgrat  44496  radcnvrat  44497  nznngen  44499  uzmptshftfval  44529  binomcxplemcvg  44537  binomcxplemnotnn0  44539  tpid3gVD  45024  en3lplem2VD  45026  orbitclmpt  45141  wfaxrep  45177  wfaxsep  45178  wfaxpow  45180  wfaxpr  45181  wfaxun  45182  wfac8prim  45185  brpermmodelcnv  45187  nregmodellem  45199  iuneq1i  45271  rexanuz3  45282  eliuniin  45285  eliuniin2  45306  disjinfi  45378  fsneq  45392  iuneqfzuzlem  45521  allbutfi  45579  eluzelz2  45589  uz0  45598  uzublem  45616  uzid3  45621  elicores  45721  uzinico  45747  climsuselem1  45795  climsuse  45796  islptre  45807  fnlimfvre  45860  limsupresico  45886  limsupvaluz  45894  limsupubuzlem  45898  limsupequzmptlem  45914  liminfresico  45957  cnrefiisplem  46015  stoweidlem14  46200  stoweidlem39  46225  stoweidlem48  46234  stoweidlem51  46237  stoweidlem59  46245  stoweidlem62  46248  wallispilem3  46253  fourierdlem42  46335  fourierdlem62  46354  fourierdlem80  46372  fourierdlem103  46395  fourierdlem104  46396  etransclem26  46446  rrxsnicc  46486  ioorrnopn  46491  ioorrnopnxr  46493  sge00  46562  sge0fodjrnlem  46602  sge0isum  46613  sge0seq  46632  meadjiunlem  46651  carageneld  46688  volicorescl  46739  hoidmv1lelem1  46777  hoidmv1le  46780  hoidmvlelem1  46781  hoidmvlelem3  46783  ovnhoilem2  46788  hoiqssbllem2  46809  opnvonmbllem2  46819  ovolval4lem1  46835  iinhoiicc  46860  vonioolem1  46866  smflimlem1  46957  smflimlem2  46958  smflim  46963  nsssmfmbf  46965  smfresal  46974  smfrec  46975  smfdiv  46983  smfpimbor1lem2  46985  smflim2  46992  smflimmpt  46996  smfinflem  47003  smflimsuplem1  47006  smflimsuplem2  47007  smflimsuplem3  47008  smflimsuplem5  47010  smflimsuplem6  47011  smflimsup  47014  smflimsupmpt  47015  smfliminfmpt  47018  chnerlem1  47068  chnerlem2  47069  tannpoly  47078  sinnpoly  47079  fcores  47255  ndmaovcl  47391  ndmaovcom  47393  ndmaovass  47394  ndmaovdistr  47395  dfatco  47444  otiunsndisjX  47467  fvmptrabdm  47481  ceilhalfelfzo1  47518  modmknepk  47550  elsetpreimafvb  47572  sprsymrelfolem2  47681  sprsymrelf  47683  sprsymrelf1  47684  prpair  47689  prproropf1olem0  47690  paireqne  47699  fmtno4prmfac  47760  dfodd5  47848  sbgoldbo  47975  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  clnbgrcl  48009  clnbgredg  48028  sclnbgrel  48035  isubgredg  48054  uhgrimedgi  48078  isuspgrim0  48082  isuspgrimlem  48083  gricushgr  48105  clnbgrgrimlem  48121  grimedg  48123  usgrgrtrirex  48138  stgrnbgr0  48152  isubgr3stgrlem3  48156  isubgr3stgrlem4  48157  isubgr3stgrlem6  48159  isubgr3stgrlem7  48160  uspgrlimlem2  48177  uspgrlimlem3  48178  grlimedgclnbgr  48183  grlimprclnbgr  48184  grlimprclnbgrvtx  48187  grlimgrtrilem2  48190  usgrexmpl2trifr  48225  gpgvtxel  48235  gpgedgel  48238  gpgusgralem  48244  gpg5order  48248  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgnbgrvtx0  48262  gpgnbgrvtx1  48263  gpg5nbgrvtx03star  48268  gpg5nbgr3star  48269  gpgvtxdg3  48270  gpg5gricstgr3  48278  gpgprismgr4cycllem3  48285  gpgprismgr4cycllem7  48289  gpgprismgr4cycllem8  48290  gpgprismgr4cycllem10  48292  pgnbgreunbgrlem3  48306  pgnbgreunbgrlem6  48312  pgnbgreunbgr  48313  uspgrsprf  48334  uspgrsprf1  48335  uspgrsprfo  48336  ply1sclrmsm  48572  lcoop  48599  lincfsuppcl  48601  linccl  48602  lincvalsng  48604  lincvalpr  48606  lincvalsc0  48609  linc0scn0  48611  lincdifsn  48612  linc1  48613  lincsum  48617  lincscm  48618  lspsslco  48625  snlindsntor  48659  lincresunit3lem2  48668  ldepsnlinclem1  48693  ldepsnlinclem2  48694  prelrrx2  48901  prelrrx2b  48902  rrx2xpref1o  48906  rrx2plord  48908  rrx2linesl  48931  sectrcl  49209  invrcl  49211  initopropdlemlem  49426  initopropd  49430  termopropd  49431  zeroopropd  49432  oppcthin  49625  indthinc  49649  prsthinc  49651  elpglem3  49900