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 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eleq12i  2827  eleqtri  2832  eleq2s  2852  hbxfreq  2865  nfceqi  2901  raleqbii  3339  rexeqbii  3340  rabeqi  3446  rabrabi  3451  reqabi  3455  elab2g  3671  elrabf  3680  elrab3t  3683  elrab2  3687  cbvsbcw  3812  cbvsbcvw  3813  cbvsbc  3814  elin2  4198  elsymdif  4248  noel  4331  noelOLD  4332  eltpg  4690  elunirab  4925  elintrab  4965  disjxiun  5146  exss  5464  otiunsndisj  5521  brabsb  5532  brabga  5535  epelg  5582  pofun  5607  elxp  5700  opeliunxp  5744  bropaex12  5768  brab2a  5770  elcnv  5877  dmopabelb  5917  elrnmptg  5959  elres  6021  elrid  6046  rninxp  6179  elid  6199  elsuci  6432  elsucg  6433  elsuc2g  6434  elfv  6890  0fv  6936  opabiota  6975  dffv2  6987  fvopab3g  6994  fvmptex  7013  fvopab5  7031  fvn0ssdmfun  7077  fveqressseq  7082  f0cli  7100  fmptco  7127  fvrnressn  7159  funfvima  7232  elunirnALT  7251  fliftel  7306  eloprabga  7516  eloprabgaOLD  7517  elrnmpo  7545  ovid  7549  offval  7679  sucexeloniOLD  7798  suceloniOLD  7800  1st2val  8003  2nd2val  8004  bropopvvv  8076  bropfvvvv  8078  fsplit  8103  xporderlem  8113  frpoins3xpg  8126  frpoins3xp3g  8127  brtpos2  8217  frrlem8  8278  frrlem9  8279  frrlem10  8280  fprresex  8295  wfrdmclOLD  8317  wfrfunOLD  8319  wfrlem12OLD  8320  wfrlem17OLD  8325  wfr2OLD  8328  issmo  8348  smores3  8353  tfrlem7  8383  tfrlem9  8385  tfrlem9a  8386  tfr2b  8396  tfr2  8398  rdgsuc  8424  frsucmptn  8439  tz7.48-2  8442  el1o  8495  ord2eln012  8497  dif1o  8500  ondif2  8502  oawordeulem  8554  elecg  8746  brecop  8804  erovlem  8807  eceqoveq  8816  mapsncnv  8887  mptelixpg  8929  brsdom  8971  isfi  8972  enssdom  8973  brdom2  8978  xpcomco  9062  brsdom2  9097  en3lplem2  9608  cnfcom2lem  9696  brttrcl2  9709  ttrcltr  9711  rnttrcl  9717  epfrs  9726  r1limg  9766  r1ord  9775  r1ord3  9777  tz9.12lem3  9784  rankvaln  9794  r1elss  9801  rankpwi  9818  ssrankr1  9830  r1val3  9833  r1pw  9840  rankr1b  9859  djur  9914  djuunxp  9916  eldju2ndl  9919  eldju2ndr  9920  isnum2  9940  cardprclem  9974  infxpenlem  10008  alephcard  10065  alephnbtwn  10066  alephnbtwn2  10067  alephord2  10071  alephsdom  10081  dfac3  10116  dfac5lem2  10119  dfac5lem3  10120  dfac5lem5  10122  pwsdompw  10199  cfub  10244  cardcf  10247  cflecard  10248  cfle  10249  cflim2  10258  cofsmo  10264  cfidm  10270  isfin3  10291  isfin5  10294  isfin6  10295  sdom2en01  10297  fin23lem26  10320  fin23lem30  10337  isf32lem5  10352  itunitc1  10415  ituniiun  10417  axdc3lem3  10447  axcclem  10452  axdclem  10514  iunfo  10534  iundom2g  10535  cardidg  10543  konigthlem  10563  alephadd  10572  alephreg  10577  pwcfsdom  10578  cfpwsdom  10579  elgch  10617  fpwwe2lem11  10636  canth4  10642  wunex2  10733  r1tskina  10777  elni  10871  nlt1pi  10901  adderpq  10951  mulerpq  10952  recmulnq  10959  addsrpr  11070  mulsrpr  11071  opelcn  11124  opelreal  11125  elreal  11126  elreal2  11127  0ncn  11128  addcnsr  11130  mulcnsr  11131  xrlenlt  11279  elnn0  12474  elnnne0  12486  un0addcl  12505  un0mulcl  12506  elxnn0  12546  uztrn2  12841  elnnuz  12866  elnn0uz  12867  elq  12934  elxr  13096  elfzm1b  13579  elfz0lmr  13747  uzrdgfni  13923  fzennn  13933  ser0  14020  hash2pwpr  14437  iswrd  14466  pfxccatpfx1  14686  s3iunsndisj  14915  sumz  15668  sumss  15670  fsumcvg3  15675  abscvgcvg  15765  isumshft  15785  prodf1  15837  zprod  15881  prod1  15888  prodss  15891  prodsn  15906  prodsnf  15908  bpolydiflem  15998  bpoly2  16001  bpoly3  16002  bpoly4  16003  ruclem6  16178  divides  16199  dvdsflip  16260  pwp1fsum  16334  sadc0  16395  eulerthlem2  16715  prm23lt5  16747  4sqlem2  16882  4sqlem12  16889  vdwpc  16913  xpscf  17511  cidpropd  17654  oppcsect  17725  funcpropd  17851  natpropd  17929  dfinito2  17953  dftermo2  17954  initoeu2lem0  17963  arwhoma  17995  eldmcoa  18015  pospo  18298  psss  18533  ismgmn0  18563  gsumpropd2lem  18598  elefmndbas  18754  smndex1basss  18786  smndex1mgm  18788  pwmnd  18818  dfgrp2e  18848  mulgfval  18952  eqg0subg  19073  cycsubmel  19077  ghmeqker  19119  elcntr  19194  cntri  19196  cntzsgrpcl  19198  oppgsubg  19230  fvcosymgeq  19297  symgfixels  19302  pmtrfrn  19326  efgsfo  19607  efgrelexlemb  19618  lt6abl  19763  dmdprd  19868  dprdval  19873  dprdw  19880  srgbinomlem4  20052  isnirred  20234  isrhm  20257  issrng  20458  lspexchn2  20744  lspindp2l  20747  lspindp2  20748  lbsextlem2  20772  2idlss  20868  cnfldfun  20956  dsmmelbas  21294  frlmbas3  21331  lindsind2  21374  islindf4  21393  psrbagf  21471  evlslem4  21637  ply1bascl2  21728  cply1mul  21818  lply1binom  21830  matsubgcell  21936  matinvgcell  21937  matvscacell  21938  matepmcl  21964  matepm2cl  21965  scmatscm  22015  smatvscl  22026  marrepcl  22066  marepvcl  22071  mulmarep1el  22074  mulmarep1gsum1  22075  mulmarep1gsum2  22076  submabas  22080  m1detdiag  22099  mdetdiag  22101  m2detleib  22133  gsummatr01lem3  22159  gsummatr01  22161  smadiadetlem4  22171  slesolinv  22182  slesolinvbi  22183  slesolex  22184  cramerimplem2  22186  pmatcoe1fsupp  22203  mat2pmatbas  22228  mat2pmatmul  22233  mat2pmatlin  22237  decpmatmul  22274  monmatcollpw  22281  pm2mpf1  22301  pm2mpghm  22318  istps  22436  mretopd  22596  neiptopuni  22634  lpdifsn  22647  restcls  22685  perfopn  22689  pnfnei  22724  mnfnei  22725  lmss  22802  hauscmplem  22910  is2ndc  22950  2ndcdisj  22960  hausnlly  22997  txuni2  23069  ptpjpre1  23075  elpt  23076  dfac14  23122  xkococn  23164  fbasrn  23388  fin1aufil  23436  elfm2  23452  elfm3  23454  fbflim  23480  flffbas  23499  cnpflf2  23504  fclsbas  23525  efmndtmd  23605  tsmssubm  23647  iscusp2  23807  imasdsf1olem  23879  metustel  24059  metuel2  24074  isnghm  24240  opnreen  24347  iccpnfcnv  24460  ehleudisval  24936  ehl1eudis  24937  ehl2eudis  24939  minveclem3b  24945  ovoliunlem1  25019  ioombl1lem4  25078  subopnmbl  25121  vitalilem2  25126  vitalilem3  25127  mbfimaopnlem  25172  mbfimaopn2  25174  itg2l  25247  dvply1  25797  vieta1lem1  25823  vieta1lem2  25824  elaa  25829  taylthlem2  25886  abelthlem6  25948  abelthlem9  25952  sinq34lt0t  26019  ellogrn  26068  dvrelog  26145  ellogdm  26147  logtayl2  26170  cxpcn3lem  26255  cxpcn3  26256  1cubr  26347  atandm  26381  atanf  26385  reasinsin  26401  atans2  26436  dmarea  26462  xrlimcnp  26473  amgmlem  26494  ppiublem1  26705  lgsdir2lem2  26829  gausslemma2dlem1a  26868  lgsquadlem1  26883  lgsquadlem2  26884  2sqlem1  26920  rpvmasum2  27015  madeval2  27348  newval  27350  leftval  27358  rightval  27359  lltropt  27367  madess  27371  oldssmade  27372  lrold  27391  addsproplem2  27454  addsproplem4  27456  addsproplem6  27458  negsproplem4  27505  negsproplem6  27507  precsexlem10  27662  precsexlem11  27663  edgiedgb  28314  isuhgr  28320  isushgr  28321  isupgr  28344  isumgr  28355  umgredg  28398  umgrpredgv  28400  umgredgne  28405  umgredgnlp  28407  isuspgr  28412  isusgr  28413  ausgrusgri  28428  usgredgppr  28453  edgssv2  28455  uspgredg2vlem  28480  uspgredg2v  28481  ushgredgedg  28486  ushgredgedgloop  28488  griedg0ssusgr  28522  uhgrissubgr  28532  subumgredg2  28542  uhgrspansubgrlem  28547  umgrres1lem  28567  upgrres1  28570  nbgrcl  28592  nbuhgr  28600  nbuhgr2vtx1edgblem  28608  nbupgrres  28621  edgnbusgreu  28624  nbusgredgeu0  28625  nbusgrf1o0  28626  hashnbusgrnn0  28633  nbupgruvtxres  28664  cffldtocusgr  28704  cusgrfilem2  28713  vtxdg0v  28730  vtxduhgr0nedg  28749  uhgrvd00  28791  vtxdginducedm1  28800  finsumvtxdg2ssteplem4  28805  wlk1walk  28896  wlkp1lem6  28935  iswwlks  29090  wwlknllvtx  29100  wwlksonvtx  29109  wspthnonp  29113  wlkiswwlksupgr2  29131  wwlksnwwlksnon  29169  2pthon3v  29197  umgr2wlk  29203  elwwlks2s3  29205  wwlks2onv  29207  elwwlks2ons3im  29208  isclwwlk  29237  clwwlkccatlem  29242  clwlkclwwlk  29255  wwlksext2clwwlk  29310  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  clwwlknon1  29350  clwwlknon1nloop  29352  clwwlknon2x  29356  1pthon2v  29406  uhgr3cyclex  29435  isconngr  29442  isconngr1  29443  eucrctshift  29496  frgrnbnb  29546  frgrncvvdeqlem1  29552  frgrncvvdeqlem2  29553  frgrncvvdeqlem3  29554  frgrncvvdeqlem9  29560  fusgreghash2wspv  29588  extwwlkfab  29605  numclwwlk1lem2foa  29607  numclwwlk1lem2fo  29611  clwlknon2num  29621  numclwlk2lem2f1o  29632  numclwwlk5lem  29640  topnfbey  29722  isvclem  29830  isnvlem  29863  vsfval  29886  h2hlm  30233  hhcmpl  30453  hhcms  30456  elch0  30507  omlsilem  30655  h1de2ctlem  30808  elspansni  30811  nonbooli  30904  spansncvi  30905  adjeq  31188  cnlnssadj  31333  cnvbraval  31363  brabgaf  31837  elimampt  31862  2ndresdju  31874  fmptdF  31881  fmptcof2  31882  acunirnmpt  31884  acunirnmpt2  31885  ofpreima  31890  fcnvgreu  31898  fdifsuppconst  31911  1stpreima  31928  2ndpreima  31929  fz2ssnn0  31996  elxrge02  32098  psgnfzto1stlem  32259  cycpmgcl  32312  nsgqusf1olem2  32525  nsgqusf1olem3  32526  prmidl0  32569  crngmxidl  32585  opprnsg  32598  ply1degltel  32666  submatres  32786  lmat22lem  32797  crefdf  32828  cmppcmp  32838  rspectopn  32847  prsdm  32894  prsrn  32895  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  pnfneige0  32931  qqhre  33000  rrhre  33001  esumnul  33046  esumcvgsum  33086  ldgenpisyslem1  33161  measvuni  33212  cntnevol  33226  dya2iocnrect  33280  sibf0  33333  oddpwdc  33353  eulerpartlemd  33365  eulerpartgbij  33371  eulerpartlemgh  33377  isrrvv  33442  coinfliprv  33481  ballotlem7  33534  signswch  33572  hashreprin  33632  chtvalz  33641  circlemethhgt  33655  hgt750lemb  33668  tgoldbachgt  33675  bnj23  33729  bnj158  33740  bnj168  33741  bnj1138  33799  bnj1143  33801  bnj1454  33853  bnj110  33869  bnj882  33937  bnj893  33939  bnj916  33944  bnj970  33958  bnj983  33962  bnj984  33963  bnj1137  34006  bnj1174  34014  bnj1388  34044  bnj1398  34045  loop1cycl  34128  subfacp1lem5  34175  satfv1  34354  satfrnmapom  34361  satf0op  34368  satf0n0  34369  fmlafvel  34376  fmlaomn0  34381  fmlan0  34382  satffunlem2lem2  34397  satfv0fvfmla0  34404  satefvfmla0  34409  mrsub0  34507  mrsubccat  34509  mrsubcn  34510  elmrsubrn  34511  msubco  34522  msubvrs  34551  elmthm  34567  mthmblem  34571  elrn3  34732  dfon2lem7  34761  brsset  34861  eltrans  34863  elfix  34875  ellimits  34882  elfuns  34887  elsingles  34890  fvtransport  35004  brcolinear2  35030  fvray  35113  linedegen  35115  fvline  35116  ellines  35124  fwddifn0  35136  elhf  35146  hfninf  35158  fnessref  35242  bj-ififc  35459  bj-csbsnlem  35783  bj-elgab  35819  currysetlem1  35828  bj-eltag  35858  bj-sngltag  35864  bj-projun  35875  bj-velpwALT  35934  bj-0nelmpt  35997  bj-opelidres  36042  bj-inftyexpitaudisj  36086  bj-elccinfty  36095  f1omptsnlem  36217  icoreelrnab  36235  relowlpssretop  36245  rdgssun  36259  exrecfnlem  36260  finxpnom  36282  uncov  36469  tan2h  36480  ptrecube  36488  poimirlem25  36513  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  cnambfre  36536  ftc1cnnc  36560  sdclem2  36610  sdclem1  36611  fdc  36613  caushft  36629  issmgrpOLD  36731  ismndo  36740  isrngo  36765  isdivrngo  36818  csbcom2fi  36996  elecALTV  37134  brrabga  37210  eldmcoss  37328  coss0  37349  elrels2  37356  dath  38607  diclspsn  40065  dvh4dimlem  40314  dvh2dim  40316  dvh3dim3N  40320  lcfrvalsnN  40412  mapdh6eN  40611  mapdh7dN  40621  mapdh8b  40651  hdmap1l6e  40685  lcmfunnnd  40877  3factsumint1  40886  sticksstones2  40963  sticksstones3  40964  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  frlmfielbas  41074  mhpind  41166  elab2gw  41409  pellex  41573  rmspecnonsq  41645  islmodfg  41811  aaitgo  41904  areaquad  41965  ordeldif1o  42010  naddwordnexlem4  42152  fpwfvss  42163  finona1cl  42204  elcnvcnvintab  42333  elnonrel  42336  elcnvcnvlem  42350  cnvcnvintabd  42351  brfvrcld2  42443  grur1cld  42991  dvgrat  43071  cvgdvgrat  43072  radcnvrat  43073  nznngen  43075  uzmptshftfval  43105  binomcxplemcvg  43113  binomcxplemnotnn0  43115  tpid3gVD  43603  en3lplem2VD  43605  rexanuz3  43785  eliuniin  43788  eliuniin2  43809  disjinfi  43891  fsneq  43905  iuneqfzuzlem  44044  allbutfi  44103  eluzelz2  44113  uz0  44122  uzublem  44140  uzid3  44145  elicores  44246  uzinico  44273  climsuselem1  44323  climsuse  44324  islptre  44335  fnlimfvre  44390  limsupresico  44416  limsupvaluz  44424  limsupubuzlem  44428  limsupequzmptlem  44444  liminfresico  44487  cnrefiisplem  44545  stoweidlem14  44730  stoweidlem39  44755  stoweidlem48  44764  stoweidlem51  44767  stoweidlem59  44775  stoweidlem62  44778  wallispilem3  44783  fourierdlem42  44865  fourierdlem62  44884  fourierdlem80  44902  fourierdlem103  44925  fourierdlem104  44926  etransclem26  44976  rrxsnicc  45016  ioorrnopn  45021  ioorrnopnxr  45023  sge00  45092  sge0fodjrnlem  45132  sge0isum  45143  sge0seq  45162  meadjiunlem  45181  carageneld  45218  volicorescl  45269  hoidmv1lelem1  45307  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem3  45313  ovnhoilem2  45318  hoiqssbllem2  45339  opnvonmbllem2  45349  ovolval4lem1  45365  iinhoiicc  45390  vonioolem1  45396  smflimlem1  45487  smflimlem2  45488  smflim  45493  nsssmfmbf  45495  smfresal  45504  smfrec  45505  smfdiv  45513  smfpimbor1lem2  45515  smflim2  45522  smflimmpt  45526  smfinflem  45533  smfinfmpt  45535  smflimsuplem1  45536  smflimsuplem2  45537  smflimsuplem3  45538  smflimsuplem5  45540  smflimsuplem6  45541  smflimsup  45544  smflimsupmpt  45545  smfliminfmpt  45548  fcores  45777  ndmaovcl  45911  ndmaovcom  45913  ndmaovass  45914  ndmaovdistr  45915  dfatco  45964  otiunsndisjX  45987  fvmptrabdm  46001  elsetpreimafvb  46052  sprsymrelfolem2  46161  sprsymrelf  46163  sprsymrelf1  46164  prpair  46169  prproropf1olem0  46170  paireqne  46179  fmtno4prmfac  46240  dfodd5  46328  sbgoldbo  46455  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  isomushgr  46494  isomuspgrlem2c  46498  uspgrsprf  46524  uspgrsprf1  46525  uspgrsprfo  46526  rnglidl1  46753  rngqiprngimfo  46786  pzriprnglem3  46807  pzriprnglem4  46808  pzriprnglem7  46811  pzriprnglem8  46812  pzriprnglem9  46813  pzriprnglem12  46816  pzriprnglem14  46818  opeliun2xp  47008  ply1sclrmsm  47064  lcoop  47092  lincfsuppcl  47094  linccl  47095  lincvalsng  47097  lincvalpr  47099  lincvalsc0  47102  linc0scn0  47104  lincdifsn  47105  linc1  47106  lincsum  47110  lincscm  47111  lspsslco  47118  snlindsntor  47152  lincresunit3lem2  47161  ldepsnlinclem1  47186  ldepsnlinclem2  47187  prelrrx2  47399  prelrrx2b  47400  rrx2xpref1o  47404  rrx2plord  47406  rrx2linesl  47429  oppcthin  47659  indthinc  47672  prsthinc  47674  elpglem3  47758