Theorem eleq2i 2855

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eleq12i  2856  eleqtri  2861  eleq2s  2881  hbxfreq  2893  nfceqi  2922  raleqbii  3336  rexeqbii  3337  rabeqi  3429  rabrabi  3435  reqabi  3439  elab2gw  3637  elab2g  3639  elrabf  3647  elrab3t  3649  elrab2  3654  cbvsbcw  3777  cbvsbcvw  3778  cbvsbc  3779  elin2  4156  elsymdif  4211  noel  4291  eltpg  4652  elunirab  4887  elintrab  4925  disjxiun  5106  exss  5444  otiunsndisj  5503  brabsb  5515  brabga  5518  epelg  5562  pofun  5587  elxp  5684  opeliunxp  5728  opeliun2xp  5729  bropaex12  5752  brab2a  5754  elcnv  5862  cnv0  5869  dmopabelb  5906  elrnmptg  5951  elres  6019  elimampt  6045  elrid  6048  rninxp  6177  elid  6198  elsuci  6430  elsucg  6431  elsuc2g  6432  elfv  6879  0fv  6922  opabiota  6963  dffv2  6976  fvopab3g  6984  fvmptex  7004  fvopab5  7023  fsneq  7030  fvn0ssdmfun  7069  fveqressseq  7074  f0cli  7093  fmptco  7125  fvrnressn  7158  funfvima  7228  elunirnALT  7250  fliftel  7307  eloprabga  7519  elrnmpo  7546  elimampo  7547  ovid  7551  offval  7683  1st2val  8010  2nd2val  8011  bropopvvv  8081  bropfvvvv  8083  fsplit  8108  xporderlem  8119  frpoins3xpg  8132  frpoins3xp3g  8133  brtpos2  8224  frrlem8  8286  frrlem9  8287  frrlem10  8288  fprresex  8303  issmo  8331  smores3  8336  tfrlem7  8366  tfrlem9  8368  tfrlem9a  8369  tfr2b  8379  tfr2  8381  rdgsuc  8407  frsucmptn  8422  tz7.48-2  8425  el1o  8476  ord2eln012  8478  dif1o  8481  ondif2  8483  oawordeulem  8535  elecg  8735  brecop  8804  erovlem  8807  eceqoveq  8816  mapsncnv  8887  mptelixpg  8929  brsdom  8967  isfi  8968  enssdomOLD  8970  brdom2  8975  xpcomco  9051  brsdom2  9085  en3lplem2  9578  cnfcom2lem  9666  brttrcl2  9679  ttrcltr  9681  rnttrcl  9687  epfrs  9696  r1limg  9739  r1ord  9748  r1ord3  9750  tz9.12lem3  9757  rankvaln  9767  r1elss  9774  rankpwi  9791  ssrankr1  9803  r1val3  9806  r1pw  9813  rankr1b  9832  djur  9901  djuunxp  9903  eldju2ndl  9906  eldju2ndr  9907  isnum2  9927  cardprclem  9961  infxpenlem  9993  alephcard  10050  alephnbtwn  10051  alephnbtwn2  10052  alephord2  10056  alephsdom  10066  dfac3  10101  dfac5lem2  10104  dfac5lem3  10105  dfac5lem5  10107  pwsdompw  10182  cfub  10227  cardcf  10230  cflecard  10231  cfle  10232  cflim2  10242  cofsmo  10248  cfidm  10254  isfin3  10275  isfin5  10278  isfin6  10279  sdom2en01  10281  fin23lem26  10304  fin23lem30  10321  isf32lem5  10336  itunitc1  10399  ituniiun  10401  axdc3lem3  10431  axcclem  10436  axdclem  10498  iunfo  10518  iundom2g  10519  cardidg  10527  konigthlem  10548  alephadd  10557  alephreg  10562  pwcfsdom  10563  cfpwsdom  10564  elgch  10602  fpwwe2lem11  10621  canth4  10627  wunex2  10718  r1tskina  10762  elni  10856  nlt1pi  10886  adderpq  10936  mulerpq  10937  recmulnq  10944  addsrpr  11055  mulsrpr  11056  opelcn  11109  opelreal  11110  elreal  11111  elreal2  11112  0ncn  11113  addcnsr  11115  mulcnsr  11116  xrlenlt  11269  elnn0  12501  elnnne0  12513  un0addcl  12532  un0mulcl  12533  elxnn0  12574  uztrn2  12876  elnnuz  12897  elnn0uz  12898  elq  12969  elxr  13136  elfzm1b  13626  elfz0lmr  13808  uzrdgfni  13990  fzennn  14000  ser0  14086  hash2pwpr  14509  iswrd  14548  pfxccatpfx1  14769  s3iunsndisj  15001  sumz  15769  sumss  15771  fsumcvg3  15776  abscvgcvg  15867  isumshft  15889  prodf1  15941  prodeq1i  15966  zprod  15987  prod1  15994  prodss  15997  prodsn  16012  prodsnf  16014  bpolydiflem  16103  bpoly2  16106  bpoly3  16107  bpoly4  16108  ruclem6  16286  divides  16307  dvdsflip  16370  pwp1fsum  16444  sadc0  16507  eulerthlem2  16836  prm23lt5  16869  4sqlem2  17004  4sqlem12  17011  vdwpc  17035  xpscf  17614  cidpropd  17761  oppcsect  17830  funcpropd  17954  natpropd  18031  dfinito2  18055  dftermo2  18056  initoeu2lem0  18065  arwhoma  18097  eldmcoa  18117  pospo  18394  psss  18631  ex-chn1  18688  ex-chn2  18689  ismgmn0  18695  gsumpropd2lem  18732  elefmndbas  18927  smndex1basss  18962  smndex1mgm  18964  pwmnd  18994  dfgrp2e  19025  mulgfval  19130  eqg0subg  19262  cycsubmel  19266  ghmeqker  19308  elcntr  19395  cntri  19397  cntzsgrpcl  19399  oppgsubg  19428  fvcosymgeq  19494  symgfixels  19499  pmtrfrn  19523  efgsfo  19804  efgrelexlemb  19815  lt6abl  19960  dmdprd  20065  dprdval  20070  dprdw  20077  srgbinomlem4  20306  isnirred  20498  isrhm  20557  isdrng3lem1  20851  issrng  20947  lspexchn2  21255  lspindp2l  21258  lspindp2  21259  lbsextlem2  21283  rnglidl1  21358  df2idl2  21396  2idlss  21401  rngqiprngimfo  21441  prmidl0  21478  cnfldfun  21536  pzriprnglem3  21633  pzriprnglem4  21634  pzriprnglem7  21637  pzriprnglem8  21638  pzriprnglem9  21639  pzriprnglem12  21642  pzriprnglem14  21644  dsmmelbas  21889  frlmbas3  21926  lindsind2  21969  islindf4  21988  psrbagf  22068  evlslem4  22227  psdmul  22329  ply1bascl2  22364  cply1mul  22456  lply1binom  22470  matsubgcell  22591  matinvgcell  22592  matvscacell  22593  matepmcl  22619  matepm2cl  22620  scmatscm  22670  smatvscl  22681  marrepcl  22721  marepvcl  22726  mulmarep1el  22729  mulmarep1gsum1  22730  mulmarep1gsum2  22731  submabas  22735  m1detdiag  22754  mdetdiag  22756  m2detleib  22788  gsummatr01lem3  22814  gsummatr01  22816  smadiadetlem4  22826  slesolinv  22837  slesolinvbi  22838  slesolex  22839  cramerimplem2  22841  pmatcoe1fsupp  22858  mat2pmatbas  22883  mat2pmatmul  22888  mat2pmatlin  22892  decpmatmul  22929  monmatcollpw  22936  pm2mpf1  22956  pm2mpghm  22973  istps  23091  mretopd  23249  neiptopuni  23287  lpdifsn  23300  restcls  23338  perfopn  23342  pnfnei  23377  mnfnei  23378  lmss  23455  hauscmplem  23563  is2ndc  23603  2ndcdisj  23613  hausnlly  23650  txuni2  23722  ptpjpre1  23728  elpt  23729  dfac14  23775  xkococn  23817  fbasrn  24041  fin1aufil  24089  elfm2  24105  elfm3  24107  fbflim  24133  flffbas  24152  cnpflf2  24157  fclsbas  24178  efmndtmd  24258  tsmssubm  24300  iscusp2  24458  imasdsf1olem  24530  metustel  24707  metuel2  24722  isnghm  24880  opnreen  24989  iccpnfcnv  25103  ehleudisval  25578  ehl1eudis  25579  ehl2eudis  25581  minveclem3b  25587  ovoliunlem1  25661  ioombl1lem4  25720  subopnmbl  25763  vitalilem2  25768  vitalilem3  25769  mbfimaopnlem  25814  mbfimaopn2  25816  itg2l  25888  dvply1  26445  vieta1lem1  26471  vieta1lem2  26472  elaa  26477  taylthlem2  26537  abelthlem6  26599  abelthlem9  26603  sinq34lt0t  26674  ellogrn  26724  dvrelog  26802  ellogdm  26804  logtayl2  26827  cxpcn3lem  26912  cxpcn3  26913  1cubr  27007  atandm  27041  atanf  27045  reasinsin  27061  atans2  27096  dmarea  27122  xrlimcnp  27133  amgmlem  27154  ppiublem1  27366  lgsdir2lem2  27490  gausslemma2dlem1a  27529  lgsquadlem1  27544  lgsquadlem2  27545  2sqlem1  27581  rpvmasum2  27676  madeval2  28026  newval  28028  leftval  28042  rightval  28043  lltr  28055  madess  28059  oldssmade  28060  oldss  28063  lrold  28090  addsproplem2  28163  addsproplem4  28165  addsproplem6  28167  negsproplem4  28224  negsproplem6  28226  precsexlem10  28409  precsexlem11  28410  ltonold  28454  elnns  28533  elzs  28577  edgiedgb  29404  isuhgr  29410  isushgr  29411  isupgr  29434  isumgr  29445  umgredg  29488  umgrpredgv  29490  umgredgne  29495  umgredgnlp  29497  isuspgr  29502  isusgr  29503  ausgrusgri  29518  usgredgppr  29546  edgssv2  29548  uspgredg2vlem  29573  uspgredg2v  29574  ushgredgedg  29579  ushgredgedgloop  29581  griedg0ssusgr  29615  uhgrissubgr  29625  subumgredg2  29635  uhgrspansubgrlem  29640  umgrres1lem  29660  upgrres1  29663  nbgrcl  29685  nbuhgr  29693  nbuhgr2vtx1edgblem  29701  nbupgrres  29714  edgnbusgreu  29717  nbusgredgeu0  29718  nbusgrf1o0  29719  hashnbusgrnn0  29726  nbupgruvtxres  29757  cffldtocusgr  29797  cusgrfilem2  29806  vtxdg0v  29823  vtxduhgr0nedg  29842  uhgrvd00  29884  vtxdginducedm1  29893  finsumvtxdg2ssteplem4  29898  wlk1walk  29988  wlkp1lem6  30026  iswwlks  30185  wwlknllvtx  30195  wwlksonvtx  30204  wspthnonp  30208  wlkiswwlksupgr2  30226  wwlksnwwlksnon  30264  2pthon3v  30292  umgr2wlk  30298  elwwlks2s3  30300  wwlks2onv  30302  elwwlks2ons3im  30303  isclwwlk  30335  clwwlkccatlem  30340  clwlkclwwlk  30353  wwlksext2clwwlk  30408  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwwlknon1  30448  clwwlknon1nloop  30450  clwwlknon2x  30454  1pthon2v  30504  uhgr3cyclex  30533  isconngr  30540  isconngr1  30541  eucrctshift  30594  frgrnbnb  30644  frgrncvvdeqlem1  30650  frgrncvvdeqlem2  30651  frgrncvvdeqlem3  30652  frgrncvvdeqlem9  30658  fusgreghash2wspv  30686  extwwlkfab  30703  numclwwlk1lem2foa  30705  numclwwlk1lem2fo  30709  clwlknon2num  30719  numclwlk2lem2f1o  30730  numclwwlk5lem  30738  topnfbey  30820  isvclem  30929  isnvlem  30962  vsfval  30985  h2hlm  31332  hhcmpl  31552  hhcms  31555  elch0  31606  omlsilem  31754  h1de2ctlem  31907  elspansni  31910  nonbooli  32003  spansncvi  32004  adjeq  32287  cnlnssadj  32432  cnvbraval  32462  brabgaf  32951  2ndresdju  32994  fmptdF  33001  fmptcof2  33002  acunirnmpt  33004  acunirnmpt2  33005  ofpreima  33010  fcnvgreu  33017  fdifsuppconst  33034  1stpreima  33052  2ndpreima  33053  fz2ssnn0  33130  elxrge02  33251  ccatws1f1o  33271  gsumwrd2dccatlem  33397  psgnfzto1stlem  33420  cycpmgcl  33473  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem4  33565  elrgspnsubrunlem1  33567  rlocisunit  33596  domnprodeq0  33599  nsgqusf1olem2  33723  nsgqusf1olem3  33724  crngmxidl  33752  opprnsg  33766  rprmirredb  33822  zringfrac  33844  evl1deg2  33867  evl1deg3  33868  ply1degltel  33884  ply1degleel  33885  evlextv  33932  esplyfval3  33962  esplyindfv  33966  esplyfvn  33967  vietalem  33969  fldextrspunlsplem  34063  isconstr  34126  constrsuc  34128  constrconj  34135  submatres  34196  lmat22lem  34207  crefdf  34238  cmppcmp  34248  rspectopn  34257  prsdm  34304  prsrn  34305  xrge0iifcnv  34323  xrge0iifiso  34325  xrge0iifhom  34327  pnfneige0  34341  qqhre  34410  rrhre  34411  esumnul  34438  esumcvgsum  34478  ldgenpisyslem1  34553  measvuni  34604  cntnevol  34618  dya2iocnrect  34671  sibf0  34724  oddpwdc  34744  eulerpartlemd  34756  eulerpartgbij  34762  eulerpartlemgh  34768  isrrvv  34833  coinfliprv  34873  ballotlem7  34926  signswch  34948  hashreprin  35007  chtvalz  35016  circlemethhgt  35030  hgt750lemb  35043  tgoldbachgt  35050  bnj23  35107  bnj158  35118  bnj168  35119  bnj1138  35177  bnj1143  35178  bnj1454  35230  bnj110  35246  bnj882  35314  bnj893  35316  bnj916  35321  bnj970  35335  bnj983  35339  bnj984  35340  bnj1137  35383  bnj1174  35391  bnj1388  35421  bnj1398  35422  r1wf  35489  onrankid  35494  onvf1odlem4  35590  loop1cycl  35629  subfacp1lem5  35676  satfv1  35855  satfrnmapom  35862  satf0op  35869  satf0n0  35870  fmlafvel  35877  fmlaomn0  35882  fmlan0  35883  satffunlem2lem2  35898  satfv0fvfmla0  35905  satefvfmla0  35910  mrsub0  36008  mrsubccat  36010  mrsubcn  36011  elmrsubrn  36012  msubco  36023  msubvrs  36052  elmthm  36068  mthmblem  36072  ellcsrspsn  36133  elrn3  36254  dfon2lem7  36279  brsset  36379  eltrans  36381  elfix  36393  ellimits  36400  elfuns  36405  elsingles  36408  fvtransport  36524  brcolinear2  36550  fvray  36633  linedegen  36635  fvline  36636  ellines  36644  fwddifn0  36656  elhf  36666  hfninf  36678  rmoeqi  36719  rmoeqbii  36720  reueqi  36721  reueqbii  36722  rabeqbii  36726  iuneq12i  36727  iineq1i  36728  iineq12i  36729  riotaeqbii  36730  ixpeq1i  36732  itgeq12i  36738  cbvprodvw2  36779  fnessref  36888  ttctr  37024  bj-ififc  37195  bj-csbsnlem  37558  bj-elgab  37595  currysetlem1  37603  bj-eltag  37633  bj-sngltag  37639  bj-projun  37650  bj-velpwALT  37709  bj-0nelmpt  37778  bj-opelidres  37825  bj-inftyexpitaudisj  37869  bj-elccinfty  37878  f1omptsnlem  38002  icoreelrnab  38020  relowlpssretop  38030  rdgssun  38044  exrecfnlem  38045  finxpnom  38067  uncov  38272  tan2h  38283  ptrecube  38291  poimirlem25  38316  poimirlem29  38320  poimirlem30  38321  poimirlem31  38322  poimirlem32  38323  cnambfre  38339  ftc1cnnc  38363  sdclem2  38413  sdclem1  38414  fdc  38416  caushft  38432  issmgrpOLD  38534  ismndo  38543  isrngo  38568  isdivrngo  38621  csbcom2fi  38797  elecALTV  38940  brrabga  39010  eldmxrncnvepres  39103  eldmxrncnvepres2  39104  elrels2  39110  blockadjliftmap  39127  dfpre  39145  eupre  39163  eldmcoss  39217  coss0  39238  petseq  39645  dath  40530  diclspsn  41988  dvh4dimlem  42237  dvh2dim  42239  dvh3dim3N  42243  lcfrvalsnN  42335  mapdh6eN  42534  mapdh7dN  42544  mapdh8b  42574  hdmap1l6e  42608  lcmfunnnd  42799  3factsumint1  42808  primrootsunit1  42884  primrootscoprmpow  42886  aks6d1c2lem4  42914  sticksstones2  42934  sticksstones3  42935  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  aks6d1c6lem2  42958  aks6d1c6lem3  42959  redvmptabs  43141  readvrec2  43142  readvrec  43143  frlmfielbas  43294  mhpind  43346  pellex  43582  rmspecnonsq  43654  islmodfg  43816  aaitgo  43909  areaquad  43963  ordeldif1o  44007  naddwordnexlem4  44148  fpwfvss  44158  finona1cl  44199  elcnvcnvintab  44328  elnonrel  44331  elcnvcnvlem  44345  cnvcnvintabd  44346  brfvrcld2  44438  grur1cld  44976  dvgrat  45042  cvgdvgrat  45043  radcnvrat  45044  nznngen  45046  uzmptshftfval  45076  binomcxplemcvg  45084  binomcxplemnotnn0  45086  tpid3gVD  45570  en3lplem2VD  45572  orbitclmpt  45687  wfaxrep  45723  wfaxsep  45724  wfaxpow  45726  wfaxpr  45727  wfaxun  45728  wfac8prim  45731  brpermmodelcnv  45733  nregmodellem  45745  iuneq1i  45824  rexanuz3  45834  eliuniin  45837  eliuniin2  45858  disjinfi  45930  iuneqfzuzlem  46070  allbutfi  46128  eluzelz2  46137  uz0  46146  uzublem  46164  uzid3  46169  elicores  46269  uzinico  46295  climsuselem1  46343  climsuse  46344  islptre  46355  fnlimfvre  46408  limsupresico  46434  limsupvaluz  46442  limsupubuzlem  46446  limsupequzmptlem  46462  liminfresico  46505  cnrefiisplem  46563  stoweidlem14  46748  stoweidlem39  46773  stoweidlem48  46782  stoweidlem51  46785  stoweidlem59  46793  stoweidlem62  46796  wallispilem3  46801  fourierdlem42  46883  fourierdlem62  46902  fourierdlem80  46920  fourierdlem103  46943  fourierdlem104  46944  etransclem26  46994  rrxsnicc  47034  ioorrnopn  47039  ioorrnopnxr  47041  sge00  47110  sge0fodjrnlem  47150  sge0isum  47161  sge0seq  47180  meadjiunlem  47199  carageneld  47236  volicorescl  47287  hoidmv1lelem1  47325  hoidmv1le  47328  hoidmvlelem1  47329  hoidmvlelem3  47331  ovnhoilem2  47336  hoiqssbllem2  47357  opnvonmbllem2  47367  ovolval4lem1  47383  iinhoiicc  47408  vonioolem1  47414  smflimlem1  47505  smflimlem2  47506  smflim  47511  nsssmfmbf  47513  smfresal  47522  smfrec  47523  smfdiv  47531  smfpimbor1lem2  47533  smflim2  47540  smflimmpt  47544  smfinflem  47551  smflimsuplem1  47554  smflimsuplem2  47555  smflimsuplem3  47556  smflimsuplem5  47558  smflimsuplem6  47559  smflimsup  47562  smflimsupmpt  47563  smfliminfmpt  47566  chnerlem1  47618  chnerlem2  47619  tannpoly  47647  sinnpoly  47648  fcores  47824  ndmaovcl  47960  ndmaovcom  47962  ndmaovass  47963  ndmaovdistr  47964  dfatco  48013  otiunsndisjX  48036  fvmptrabdm  48050  ceilhalfelfzo1  48091  modmknepk  48125  elsetpreimafvb  48153  sprsymrelfolem2  48262  sprsymrelf  48264  sprsymrelf1  48265  prpair  48270  prproropf1olem0  48271  paireqne  48280  fmtno4prmfac  48344  dfodd5  48445  sbgoldbo  48572  nnsum4primeseven  48585  nnsum4primesevenALTV  48586  clnbgrcl  48606  clnbgredg  48625  sclnbgrel  48632  isubgredg  48651  uhgrimedgi  48675  isuspgrim0  48679  isuspgrimlem  48680  gricushgr  48702  clnbgrgrimlem  48718  grimedg  48720  usgrgrtrirex  48735  stgrnbgr0  48749  isubgr3stgrlem3  48753  isubgr3stgrlem4  48754  isubgr3stgrlem6  48756  isubgr3stgrlem7  48757  uspgrlimlem2  48774  uspgrlimlem3  48775  grlimedgclnbgr  48780  grlimprclnbgr  48781  grlimprclnbgrvtx  48784  grlimgrtrilem2  48787  usgrexmpl2trifr  48822  gpgvtxel  48832  gpgedgel  48835  gpgusgralem  48841  gpg5order  48845  gpgvtxedg0  48848  gpgvtxedg1  48849  gpgnbgrvtx0  48859  gpgnbgrvtx1  48860  gpg5nbgrvtx03star  48865  gpg5nbgr3star  48866  gpgvtxdg3  48867  gpg5gricstgr3  48875  gpgprismgr4cycllem3  48882  gpgprismgr4cycllem7  48886  gpgprismgr4cycllem8  48887  gpgprismgr4cycllem10  48889  pgnbgreunbgrlem3  48903  pgnbgreunbgrlem6  48909  pgnbgreunbgr  48910  uspgrsprf  48931  uspgrsprf1  48932  uspgrsprfo  48933  dfidom2  49128  ply1sclrmsm  49184  lcoop  49211  lincfsuppcl  49213  linccl  49214  lincvalsng  49216  lincvalpr  49218  lincvalsc0  49221  linc0scn0  49223  lincdifsn  49224  linc1  49225  lincsum  49229  lincscm  49230  lspsslco  49237  snlindsntor  49271  lincresunit3lem2  49280  ldepsnlinclem1  49305  ldepsnlinclem2  49306  prelrrx2  49513  prelrrx2b  49514  rrx2xpref1o  49518  rrx2plord  49520  rrx2linesl  49543  sectrcl  49820  invrcl  49822  initopropdlemlem  50037  initopropd  50041  termopropd  50042  zeroopropd  50043  oppcthin  50236  indthinc  50260  prsthinc  50262  elpglem3  50511