Theorem eleq2i 2823

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111

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 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  eleq12i  2824  eleqtri  2829  eleq2s  2849  hbxfreq  2861  nfceqi  2891  raleqbii  3310  rexeqbii  3311  rabeqi  3408  rabrabi  3414  reqabi  3418  elab2gw  3629  elab2g  3631  elrabf  3639  elrab3t  3641  elrab2  3645  cbvsbcw  3769  cbvsbcvw  3770  cbvsbc  3771  elin2  4150  elsymdif  4205  noel  4285  eltpg  4636  elunirab  4871  elintrab  4908  disjxiun  5086  exss  5401  otiunsndisj  5458  brabsb  5469  brabga  5472  epelg  5515  pofun  5540  elxp  5637  opeliunxp  5681  opeliun2xp  5682  bropaex12  5705  brab2a  5707  elcnv  5815  dmopabelb  5855  elrnmptg  5900  elres  5968  elimampt  5991  elrid  5994  cnv0  6086  rninxp  6126  elid  6146  elsuci  6375  elsucg  6376  elsuc2g  6377  elfv  6820  0fv  6863  opabiota  6904  dffv2  6917  fvopab3g  6924  fvmptex  6943  fvopab5  6962  fvn0ssdmfun  7007  fveqressseq  7012  f0cli  7031  fmptco  7062  fvrnressn  7094  funfvima  7164  elunirnALT  7186  fliftel  7243  eloprabga  7455  elrnmpo  7482  elimampo  7483  ovid  7487  offval  7619  1st2val  7949  2nd2val  7950  bropopvvv  8020  bropfvvvv  8022  fsplit  8047  xporderlem  8057  frpoins3xpg  8070  frpoins3xp3g  8071  brtpos2  8162  frrlem8  8223  frrlem9  8224  frrlem10  8225  fprresex  8240  issmo  8268  smores3  8273  tfrlem7  8302  tfrlem9  8304  tfrlem9a  8305  tfr2b  8315  tfr2  8317  rdgsuc  8343  frsucmptn  8358  tz7.48-2  8361  el1o  8410  ord2eln012  8412  dif1o  8415  ondif2  8417  oawordeulem  8469  elecg  8666  brecop  8734  erovlem  8737  eceqoveq  8746  mapsncnv  8817  mptelixpg  8859  brsdom  8897  isfi  8898  enssdom  8899  brdom2  8904  xpcomco  8980  brsdom2  9014  en3lplem2  9503  cnfcom2lem  9591  brttrcl2  9604  ttrcltr  9606  rnttrcl  9612  epfrs  9621  r1limg  9664  r1ord  9673  r1ord3  9675  tz9.12lem3  9682  rankvaln  9692  r1elss  9699  rankpwi  9716  ssrankr1  9728  r1val3  9731  r1pw  9738  rankr1b  9757  djur  9812  djuunxp  9814  eldju2ndl  9817  eldju2ndr  9818  isnum2  9838  cardprclem  9872  infxpenlem  9904  alephcard  9961  alephnbtwn  9962  alephnbtwn2  9963  alephord2  9967  alephsdom  9977  dfac3  10012  dfac5lem2  10015  dfac5lem3  10016  dfac5lem5  10018  pwsdompw  10094  cfub  10140  cardcf  10143  cflecard  10144  cfle  10145  cflim2  10154  cofsmo  10160  cfidm  10166  isfin3  10187  isfin5  10190  isfin6  10191  sdom2en01  10193  fin23lem26  10216  fin23lem30  10233  isf32lem5  10248  itunitc1  10311  ituniiun  10313  axdc3lem3  10343  axcclem  10348  axdclem  10410  iunfo  10430  iundom2g  10431  cardidg  10439  konigthlem  10459  alephadd  10468  alephreg  10473  pwcfsdom  10474  cfpwsdom  10475  elgch  10513  fpwwe2lem11  10532  canth4  10538  wunex2  10629  r1tskina  10673  elni  10767  nlt1pi  10797  adderpq  10847  mulerpq  10848  recmulnq  10855  addsrpr  10966  mulsrpr  10967  opelcn  11020  opelreal  11021  elreal  11022  elreal2  11023  0ncn  11024  addcnsr  11026  mulcnsr  11027  xrlenlt  11177  elnn0  12383  elnnne0  12395  un0addcl  12414  un0mulcl  12415  elxnn0  12456  uztrn2  12751  elnnuz  12776  elnn0uz  12777  elq  12848  elxr  13015  elfzm1b  13502  elfz0lmr  13683  uzrdgfni  13865  fzennn  13875  ser0  13961  hash2pwpr  14383  iswrd  14422  pfxccatpfx1  14643  s3iunsndisj  14875  sumz  15629  sumss  15631  fsumcvg3  15636  abscvgcvg  15726  isumshft  15746  prodf1  15798  prodeq1i  15823  zprod  15844  prod1  15851  prodss  15854  prodsn  15869  prodsnf  15871  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  bpoly4  15966  ruclem6  16144  divides  16165  dvdsflip  16228  pwp1fsum  16302  sadc0  16365  eulerthlem2  16693  prm23lt5  16726  4sqlem2  16861  4sqlem12  16868  vdwpc  16892  xpscf  17469  cidpropd  17616  oppcsect  17685  funcpropd  17809  natpropd  17886  dfinito2  17910  dftermo2  17911  initoeu2lem0  17920  arwhoma  17952  eldmcoa  17972  pospo  18249  psss  18486  ex-chn1  18543  ex-chn2  18544  ismgmn0  18550  gsumpropd2lem  18587  elefmndbas  18781  smndex1basss  18813  smndex1mgm  18815  pwmnd  18845  dfgrp2e  18876  mulgfval  18982  eqg0subg  19108  cycsubmel  19112  ghmeqker  19155  elcntr  19242  cntri  19244  cntzsgrpcl  19246  oppgsubg  19275  fvcosymgeq  19341  symgfixels  19346  pmtrfrn  19370  efgsfo  19651  efgrelexlemb  19662  lt6abl  19807  dmdprd  19912  dprdval  19917  dprdw  19924  srgbinomlem4  20147  isnirred  20338  isrhm  20396  issrng  20759  lspexchn2  21068  lspindp2l  21071  lspindp2  21072  lbsextlem2  21096  rnglidl1  21169  df2idl2  21194  2idlss  21199  rngqiprngimfo  21238  cnfldfun  21305  cnfldfunOLD  21318  pzriprnglem3  21420  pzriprnglem4  21421  pzriprnglem7  21424  pzriprnglem8  21425  pzriprnglem9  21426  pzriprnglem12  21429  pzriprnglem14  21431  dsmmelbas  21676  frlmbas3  21713  lindsind2  21756  islindf4  21775  psrbagf  21855  evlslem4  22011  psdmul  22081  ply1bascl2  22117  cply1mul  22211  lply1binom  22225  matsubgcell  22349  matinvgcell  22350  matvscacell  22351  matepmcl  22377  matepm2cl  22378  scmatscm  22428  smatvscl  22439  marrepcl  22479  marepvcl  22484  mulmarep1el  22487  mulmarep1gsum1  22488  mulmarep1gsum2  22489  submabas  22493  m1detdiag  22512  mdetdiag  22514  m2detleib  22546  gsummatr01lem3  22572  gsummatr01  22574  smadiadetlem4  22584  slesolinv  22595  slesolinvbi  22596  slesolex  22597  cramerimplem2  22599  pmatcoe1fsupp  22616  mat2pmatbas  22641  mat2pmatmul  22646  mat2pmatlin  22650  decpmatmul  22687  monmatcollpw  22694  pm2mpf1  22714  pm2mpghm  22731  istps  22849  mretopd  23007  neiptopuni  23045  lpdifsn  23058  restcls  23096  perfopn  23100  pnfnei  23135  mnfnei  23136  lmss  23213  hauscmplem  23321  is2ndc  23361  2ndcdisj  23371  hausnlly  23408  txuni2  23480  ptpjpre1  23486  elpt  23487  dfac14  23533  xkococn  23575  fbasrn  23799  fin1aufil  23847  elfm2  23863  elfm3  23865  fbflim  23891  flffbas  23910  cnpflf2  23915  fclsbas  23936  efmndtmd  24016  tsmssubm  24058  iscusp2  24216  imasdsf1olem  24288  metustel  24465  metuel2  24480  isnghm  24638  opnreen  24747  iccpnfcnv  24869  ehleudisval  25346  ehl1eudis  25347  ehl2eudis  25349  minveclem3b  25355  ovoliunlem1  25430  ioombl1lem4  25489  subopnmbl  25532  vitalilem2  25537  vitalilem3  25538  mbfimaopnlem  25583  mbfimaopn2  25585  itg2l  25657  dvply1  26218  vieta1lem1  26245  vieta1lem2  26246  elaa  26251  taylthlem2  26309  taylthlem2OLD  26310  abelthlem6  26373  abelthlem9  26377  sinq34lt0t  26445  ellogrn  26495  dvrelog  26573  ellogdm  26575  logtayl2  26598  cxpcn3lem  26684  cxpcn3  26685  1cubr  26779  atandm  26813  atanf  26817  reasinsin  26833  atans2  26868  dmarea  26894  xrlimcnp  26905  amgmlem  26927  ppiublem1  27140  lgsdir2lem2  27264  gausslemma2dlem1a  27303  lgsquadlem1  27318  lgsquadlem2  27319  2sqlem1  27355  rpvmasum2  27450  madeval2  27794  newval  27796  leftval  27804  rightval  27805  lltropt  27817  madess  27821  oldssmade  27822  oldss  27823  lrold  27842  addsproplem2  27913  addsproplem4  27915  addsproplem6  27917  negsproplem4  27973  negsproplem6  27975  precsexlem10  28154  precsexlem11  28155  sltonold  28198  elnns  28268  elzs  28308  edgiedgb  29032  isuhgr  29038  isushgr  29039  isupgr  29062  isumgr  29073  umgredg  29116  umgrpredgv  29118  umgredgne  29123  umgredgnlp  29125  isuspgr  29130  isusgr  29131  ausgrusgri  29146  usgredgppr  29174  edgssv2  29176  uspgredg2vlem  29201  uspgredg2v  29202  ushgredgedg  29207  ushgredgedgloop  29209  griedg0ssusgr  29243  uhgrissubgr  29253  subumgredg2  29263  uhgrspansubgrlem  29268  umgrres1lem  29288  upgrres1  29291  nbgrcl  29313  nbuhgr  29321  nbuhgr2vtx1edgblem  29329  nbupgrres  29342  edgnbusgreu  29345  nbusgredgeu0  29346  nbusgrf1o0  29347  hashnbusgrnn0  29354  nbupgruvtxres  29385  cffldtocusgr  29425  cffldtocusgrOLD  29426  cusgrfilem2  29435  vtxdg0v  29452  vtxduhgr0nedg  29471  uhgrvd00  29513  vtxdginducedm1  29522  finsumvtxdg2ssteplem4  29527  wlk1walk  29617  wlkp1lem6  29655  iswwlks  29814  wwlknllvtx  29824  wwlksonvtx  29833  wspthnonp  29837  wlkiswwlksupgr2  29855  wwlksnwwlksnon  29893  2pthon3v  29921  umgr2wlk  29927  elwwlks2s3  29929  wwlks2onv  29931  elwwlks2ons3im  29932  isclwwlk  29964  clwwlkccatlem  29969  clwlkclwwlk  29982  wwlksext2clwwlk  30037  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  clwwlknon1  30077  clwwlknon1nloop  30079  clwwlknon2x  30083  1pthon2v  30133  uhgr3cyclex  30162  isconngr  30169  isconngr1  30170  eucrctshift  30223  frgrnbnb  30273  frgrncvvdeqlem1  30279  frgrncvvdeqlem2  30280  frgrncvvdeqlem3  30281  frgrncvvdeqlem9  30287  fusgreghash2wspv  30315  extwwlkfab  30332  numclwwlk1lem2foa  30334  numclwwlk1lem2fo  30338  clwlknon2num  30348  numclwlk2lem2f1o  30359  numclwwlk5lem  30367  topnfbey  30449  isvclem  30557  isnvlem  30590  vsfval  30613  h2hlm  30960  hhcmpl  31180  hhcms  31183  elch0  31234  omlsilem  31382  h1de2ctlem  31535  elspansni  31538  nonbooli  31631  spansncvi  31632  adjeq  31915  cnlnssadj  32060  cnvbraval  32090  brabgaf  32589  2ndresdju  32631  fmptdF  32638  fmptcof2  32639  acunirnmpt  32641  acunirnmpt2  32642  ofpreima  32647  fcnvgreu  32655  fdifsuppconst  32670  1stpreima  32688  2ndpreima  32689  fz2ssnn0  32768  elxrge02  32912  ccatws1f1o  32932  gsumwrd2dccatlem  33046  psgnfzto1stlem  33069  cycpmgcl  33122  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem1  33214  nsgqusf1olem2  33379  nsgqusf1olem3  33380  prmidl0  33415  crngmxidl  33434  opprnsg  33449  rprmirredb  33497  zringfrac  33519  evl1deg2  33540  evl1deg3  33541  ply1degltel  33555  ply1degleel  33556  fldextrspunlsplem  33686  isconstr  33749  constrsuc  33751  constrconj  33758  submatres  33819  lmat22lem  33830  crefdf  33861  cmppcmp  33871  rspectopn  33880  prsdm  33927  prsrn  33928  xrge0iifcnv  33946  xrge0iifiso  33948  xrge0iifhom  33950  pnfneige0  33964  qqhre  34033  rrhre  34034  esumnul  34061  esumcvgsum  34101  ldgenpisyslem1  34176  measvuni  34227  cntnevol  34241  dya2iocnrect  34294  sibf0  34347  oddpwdc  34367  eulerpartlemd  34379  eulerpartgbij  34385  eulerpartlemgh  34391  isrrvv  34456  coinfliprv  34496  ballotlem7  34549  signswch  34574  hashreprin  34633  chtvalz  34642  circlemethhgt  34656  hgt750lemb  34669  tgoldbachgt  34676  bnj23  34730  bnj158  34741  bnj168  34742  bnj1138  34800  bnj1143  34802  bnj1454  34854  bnj110  34870  bnj882  34938  bnj893  34940  bnj916  34945  bnj970  34959  bnj983  34963  bnj984  34964  bnj1137  35007  bnj1174  35015  bnj1388  35045  bnj1398  35046  r1wf  35107  onvf1odlem4  35150  loop1cycl  35181  subfacp1lem5  35228  satfv1  35407  satfrnmapom  35414  satf0op  35421  satf0n0  35422  fmlafvel  35429  fmlaomn0  35434  fmlan0  35435  satffunlem2lem2  35450  satfv0fvfmla0  35457  satefvfmla0  35462  mrsub0  35560  mrsubccat  35562  mrsubcn  35563  elmrsubrn  35564  msubco  35575  msubvrs  35604  elmthm  35620  mthmblem  35624  ellcsrspsn  35685  elrn3  35806  dfon2lem7  35831  brsset  35931  eltrans  35933  elfix  35945  ellimits  35952  elfuns  35957  elsingles  35960  fvtransport  36076  brcolinear2  36102  fvray  36185  linedegen  36187  fvline  36188  ellines  36196  fwddifn0  36208  elhf  36218  hfninf  36230  rmoeqi  36231  rmoeqbii  36232  reueqi  36233  reueqbii  36234  rabeqbii  36238  iuneq12i  36239  iineq1i  36240  iineq12i  36241  riotaeqbii  36242  ixpeq1i  36244  itgeq12i  36250  cbvprodvw2  36291  fnessref  36401  bj-ififc  36626  bj-csbsnlem  36947  bj-elgab  36983  currysetlem1  36991  bj-eltag  37021  bj-sngltag  37027  bj-projun  37038  bj-velpwALT  37097  bj-0nelmpt  37160  bj-opelidres  37205  bj-inftyexpitaudisj  37249  bj-elccinfty  37258  f1omptsnlem  37380  icoreelrnab  37398  relowlpssretop  37408  rdgssun  37422  exrecfnlem  37423  finxpnom  37445  uncov  37651  tan2h  37662  ptrecube  37670  poimirlem25  37695  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimirlem32  37702  cnambfre  37718  ftc1cnnc  37742  sdclem2  37792  sdclem1  37793  fdc  37795  caushft  37811  issmgrpOLD  37913  ismndo  37922  isrngo  37947  isdivrngo  38000  csbcom2fi  38178  elecALTV  38313  brrabga  38383  eldmxrncnvepres  38468  eldmxrncnvepres2  38469  elrels2  38475  blockadjliftmap  38482  dfpre  38499  eupre  38516  eldmcoss  38570  coss0  38591  dath  39845  diclspsn  41303  dvh4dimlem  41552  dvh2dim  41554  dvh3dim3N  41558  lcfrvalsnN  41650  mapdh6eN  41849  mapdh7dN  41859  mapdh8b  41889  hdmap1l6e  41923  lcmfunnnd  42115  3factsumint1  42124  primrootsunit1  42200  primrootscoprmpow  42202  aks6d1c2lem4  42230  sticksstones2  42250  sticksstones3  42251  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  aks6d1c6lem2  42274  aks6d1c6lem3  42275  redvmptabs  42463  readvrec2  42464  readvrec  42465  frlmfielbas  42603  mhpind  42697  pellex  42938  rmspecnonsq  43010  islmodfg  43172  aaitgo  43265  areaquad  43319  ordeldif1o  43363  naddwordnexlem4  43504  fpwfvss  43515  finona1cl  43556  elcnvcnvintab  43685  elnonrel  43688  elcnvcnvlem  43702  cnvcnvintabd  43703  brfvrcld2  43795  grur1cld  44335  dvgrat  44415  cvgdvgrat  44416  radcnvrat  44417  nznngen  44419  uzmptshftfval  44449  binomcxplemcvg  44457  binomcxplemnotnn0  44459  tpid3gVD  44944  en3lplem2VD  44946  orbitclmpt  45061  wfaxrep  45097  wfaxsep  45098  wfaxpow  45100  wfaxpr  45101  wfaxun  45102  wfac8prim  45105  brpermmodelcnv  45107  nregmodellem  45119  iuneq1i  45192  rexanuz3  45203  eliuniin  45206  eliuniin2  45227  disjinfi  45299  fsneq  45313  iuneqfzuzlem  45443  allbutfi  45501  eluzelz2  45511  uz0  45520  uzublem  45538  uzid3  45543  elicores  45643  uzinico  45669  climsuselem1  45717  climsuse  45718  islptre  45729  fnlimfvre  45782  limsupresico  45808  limsupvaluz  45816  limsupubuzlem  45820  limsupequzmptlem  45836  liminfresico  45879  cnrefiisplem  45937  stoweidlem14  46122  stoweidlem39  46147  stoweidlem48  46156  stoweidlem51  46159  stoweidlem59  46167  stoweidlem62  46170  wallispilem3  46175  fourierdlem42  46257  fourierdlem62  46276  fourierdlem80  46294  fourierdlem103  46317  fourierdlem104  46318  etransclem26  46368  rrxsnicc  46408  ioorrnopn  46413  ioorrnopnxr  46415  sge00  46484  sge0fodjrnlem  46524  sge0isum  46535  sge0seq  46554  meadjiunlem  46573  carageneld  46610  volicorescl  46661  hoidmv1lelem1  46699  hoidmv1le  46702  hoidmvlelem1  46703  hoidmvlelem3  46705  ovnhoilem2  46710  hoiqssbllem2  46731  opnvonmbllem2  46741  ovolval4lem1  46757  iinhoiicc  46782  vonioolem1  46788  smflimlem1  46879  smflimlem2  46880  smflim  46885  nsssmfmbf  46887  smfresal  46896  smfrec  46897  smfdiv  46905  smfpimbor1lem2  46907  smflim2  46914  smflimmpt  46918  smfinflem  46925  smflimsuplem1  46928  smflimsuplem2  46929  smflimsuplem3  46930  smflimsuplem5  46932  smflimsuplem6  46933  smflimsup  46936  smflimsupmpt  46937  smfliminfmpt  46940  chnerlem1  46990  chnerlem2  46991  tannpoly  47000  sinnpoly  47001  fcores  47177  ndmaovcl  47313  ndmaovcom  47315  ndmaovass  47316  ndmaovdistr  47317  dfatco  47366  otiunsndisjX  47389  fvmptrabdm  47403  ceilhalfelfzo1  47440  modmknepk  47472  elsetpreimafvb  47494  sprsymrelfolem2  47603  sprsymrelf  47605  sprsymrelf1  47606  prpair  47611  prproropf1olem0  47612  paireqne  47621  fmtno4prmfac  47682  dfodd5  47770  sbgoldbo  47897  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  clnbgrcl  47931  clnbgredg  47950  sclnbgrel  47957  isubgredg  47976  uhgrimedgi  48000  isuspgrim0  48004  isuspgrimlem  48005  gricushgr  48027  clnbgrgrimlem  48043  grimedg  48045  usgrgrtrirex  48060  stgrnbgr0  48074  isubgr3stgrlem3  48078  isubgr3stgrlem4  48079  isubgr3stgrlem6  48081  isubgr3stgrlem7  48082  uspgrlimlem2  48099  uspgrlimlem3  48100  grlimedgclnbgr  48105  grlimprclnbgr  48106  grlimprclnbgrvtx  48109  grlimgrtrilem2  48112  usgrexmpl2trifr  48147  gpgvtxel  48157  gpgedgel  48160  gpgusgralem  48166  gpg5order  48170  gpgvtxedg0  48173  gpgvtxedg1  48174  gpgnbgrvtx0  48184  gpgnbgrvtx1  48185  gpg5nbgrvtx03star  48190  gpg5nbgr3star  48191  gpgvtxdg3  48192  gpg5gricstgr3  48200  gpgprismgr4cycllem3  48207  gpgprismgr4cycllem7  48211  gpgprismgr4cycllem8  48212  gpgprismgr4cycllem10  48214  pgnbgreunbgrlem3  48228  pgnbgreunbgrlem6  48234  pgnbgreunbgr  48235  uspgrsprf  48256  uspgrsprf1  48257  uspgrsprfo  48258  ply1sclrmsm  48494  lcoop  48522  lincfsuppcl  48524  linccl  48525  lincvalsng  48527  lincvalpr  48529  lincvalsc0  48532  linc0scn0  48534  lincdifsn  48535  linc1  48536  lincsum  48540  lincscm  48541  lspsslco  48548  snlindsntor  48582  lincresunit3lem2  48591  ldepsnlinclem1  48616  ldepsnlinclem2  48617  prelrrx2  48824  prelrrx2b  48825  rrx2xpref1o  48829  rrx2plord  48831  rrx2linesl  48854  sectrcl  49133  invrcl  49135  initopropdlemlem  49350  initopropd  49354  termopropd  49355  zeroopropd  49356  oppcthin  49549  indthinc  49573  prsthinc  49575  elpglem3  49824