Theorem eleq2i 2680

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

Syntax hints:   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  eleq12i  2681  eleqtri  2686  eleq2s  2706  hbxfreq  2717  raleqbii  2973  rexeqbii  3036  rabeq2i  3170  elab2g  3322  elrabf  3329  elrab3t  3330  elrab2  3333  cbvsbc  3431  elin2  3763  elsymdif  3811  dfnul2  3876  noel  3878  eltpg  4174  tpid3gOLD  4249  elunirab  4384  elintrab  4423  disjxiun  4579  disjxiunOLD  4580  exss  4858  elopOLD  4863  otiunsndisj  4905  brabsb  4911  brabga  4914  pofun  4975  elxp  5055  brab2a  5091  opeliunxp  5093  bropaex12  5115  brab2ga  5117  elcnv  5221  elrnmptg  5296  opelres  5322  rninxp  5492  elsuci  5708  elsucg  5709  elsuc2g  5710  elfv  6101  0fv  6137  opabiota  6171  dffv2  6181  fvopab3g  6187  fvmptex  6203  fvopab5  6217  fvn0ssdmfun  6258  fveqressseq  6263  f0cli  6278  fmptco  6303  fvrnressn  6333  funfvima  6396  elunirnALT  6414  fliftel  6459  eloprabga  6645  elrnmpt2  6671  ovid  6675  offval  6802  suceloni  6905  1st2val  7085  2nd2val  7086  bropopvvv  7142  bropfvvvv  7144  fsplit  7169  xporderlem  7175  brtpos2  7245  wfrdmcl  7310  wfrfun  7312  wfrlem12  7313  wfrlem17  7318  wfr2  7321  issmo  7332  smores3  7337  tfrlem7  7366  tfrlem9  7368  tfrlem9a  7369  tfr2b  7379  tfr2  7381  rdgsuc  7407  frsucmptn  7421  tz7.48-2  7424  el1o  7466  dif1o  7467  ondif2  7469  oawordeulem  7521  elecg  7672  brecop  7727  erovlem  7730  eceqoveq  7740  mapsncnv  7790  mptelixpg  7831  brsdom  7864  isfi  7865  enssdom  7866  brdom2  7871  map1  7921  xpcomco  7935  brsdom2  7969  en3lplem2  8395  cnfcom2lem  8481  epfrs  8490  r1limg  8517  r1ord  8526  r1ord3  8528  tz9.12lem3  8535  rankvaln  8545  r1elss  8552  rankpwi  8569  ssrankr1  8581  r1val3  8584  r1pw  8591  rankr1b  8610  isnum2  8654  cardprclem  8688  infxpenlem  8719  alephcard  8776  alephnbtwn  8777  alephnbtwn2  8778  alephord2  8782  alephsdom  8792  dfac3  8827  dfac5lem2  8830  dfac5lem3  8831  dfac5lem5  8833  pwsdompw  8909  cfub  8954  cardcf  8957  cflecard  8958  cfle  8959  cflim2  8968  cofsmo  8974  cfidm  8980  isfin3  9001  isfin5  9004  isfin6  9005  sdom2en01  9007  fin23lem26  9030  fin23lem30  9047  isf32lem5  9062  itunitc1  9125  ituniiun  9127  axdc3lem3  9157  axcclem  9162  axdclem  9224  iunfo  9240  iundom2g  9241  cardidg  9249  konigthlem  9269  alephadd  9278  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  elgch  9323  fpwwe2lem12  9342  canth4  9348  wunex2  9439  r1tskina  9483  elni  9577  nlt1pi  9607  adderpq  9657  mulerpq  9658  recmulnq  9665  addsrpr  9775  mulsrpr  9776  opelcn  9829  opelreal  9830  elreal  9831  elreal2  9832  0ncn  9833  addcnsr  9835  mulcnsr  9836  xrlenlt  9982  elnn0  11171  elnnne0  11183  un0addcl  11203  un0mulcl  11204  elxnn0  11242  uztrn2  11581  elnnuz  11600  elnn0uz  11601  elq  11666  elxr  11826  elfzm1b  12287  uzrdgfni  12619  fzennn  12629  fsuppmapnn0fiubOLD  12653  ser0  12715  hash2pwpr  13115  iswrd  13162  s3iunsndisj  13555  sumz  14300  sumss  14302  fsumcvg3  14307  abscvgcvg  14392  isumshft  14410  prodf1  14462  zprod  14506  prod1  14513  prodss  14516  prodsn  14531  prodsnf  14533  bpolydiflem  14624  bpoly2  14627  bpoly3  14628  bpoly4  14629  ruclem6  14803  divides  14823  dvdsflip  14877  pwp1fsum  14952  sadc0  15014  eulerthlem2  15325  prm23lt5  15357  4sqlem2  15491  4sqlem12  15498  vdwpc  15522  xpscf  16049  cidpropd  16193  oppcsect  16261  funcpropd  16383  natpropd  16459  initoeu2lem0  16486  arwhoma  16518  eldmcoa  16538  pospo  16796  psss  17037  ismgmn0  17067  gsumpropd2lem  17096  dfgrp2e  17271  ghmeqker  17510  cntri  17586  oppgsubg  17616  fvcosymgeq  17672  symgfixels  17677  pmtrfrn  17701  efgsfo  17975  efgrelexlemb  17986  lt6abl  18119  dmdprd  18220  dprdval  18225  dprdw  18232  srgbinomlem4  18366  isnirred  18523  isrhm  18544  issrng  18673  lspexchn2  18952  lspindp2l  18955  lspindp2  18956  lbsextlem2  18980  evlslem4  19329  ply1bascl2  19395  cply1mul  19485  lply1binom  19497  dsmmelbas  19902  frlmbas3  19934  lindsind2  19977  islindf4  19996  matsubgcell  20059  matinvgcell  20060  matvscacell  20061  matepmcl  20087  matepm2cl  20088  scmatscm  20138  smatvscl  20149  marrepcl  20189  marepvcl  20194  mulmarep1el  20197  mulmarep1gsum1  20198  mulmarep1gsum2  20199  submabas  20203  m1detdiag  20222  mdetdiag  20224  m2detleib  20256  gsummatr01lem3  20282  gsummatr01  20284  smadiadetlem4  20294  slesolinv  20305  slesolinvbi  20306  slesolex  20307  cramerimplem2  20309  pmatcoe1fsupp  20325  mat2pmatbas  20350  mat2pmatmul  20355  mat2pmatlin  20359  decpmatmul  20396  monmatcollpw  20403  pm2mpf1  20423  pm2mpghm  20440  istps  20551  mretopd  20706  neiptopuni  20744  lpdifsn  20757  restcls  20795  perfopn  20799  pnfnei  20834  mnfnei  20835  lmss  20912  hauscmplem  21019  is2ndc  21059  2ndcdisj  21069  hausnlly  21106  txuni2  21178  ptpjpre1  21184  elpt  21185  dfac14  21231  xkococn  21273  fbasrn  21498  fin1aufil  21546  elfm2  21562  elfm3  21564  fbflim  21590  flffbas  21609  cnpflf2  21614  fclsbas  21635  tsmssubm  21756  iscusp2  21916  imasdsf1olem  21988  metustel  22165  metuel2  22180  isnghm  22337  opnreen  22442  iccpnfcnv  22551  cvsi  22738  minveclem3b  23007  ovoliunlem1  23077  ioombl1lem4  23136  subopnmbl  23178  vitalilem2  23184  vitalilem3  23185  mbfimaopnlem  23228  mbfimaopn2  23230  itg2l  23302  dvply1  23843  vieta1lem1  23869  vieta1lem2  23870  elaa  23875  taylthlem2  23932  abelthlem6  23994  abelthlem9  23998  sinq34lt0t  24065  ellogrn  24110  dvrelog  24183  ellogdm  24185  logtayl2  24208  cxpcn3lem  24288  cxpcn3  24289  1cubr  24369  atandm  24403  atanf  24407  reasinsin  24423  atans2  24458  dmarea  24484  xrlimcnp  24495  amgmlem  24516  ppiublem1  24727  lgsdir2lem2  24851  gausslemma2dlem1a  24890  lgsquadlem1  24905  lgsquadlem2  24906  2sqlem1  24942  rpvmasum2  25001  eleenn  25576  isuhgr  25726  isushgr  25727  isupgr  25751  isumgr  25761  umgredg  25812  umgrpredgav  25813  umgredgne  25816  umgredgnlp  25818  usgraop  25879  nbgra0edg  25961  nbgraf1olem1  25970  nbgraf1olem3  25972  nbgraf1olem5  25974  uvtx01vtx  26020  wlknwwlknsur  26240  clwwlknprop  26300  hashecclwwlkn1  26361  usghashecclwwlk  26362  2wlkonot3v  26402  2spthonot3v  26403  isrgra  26453  isrusgra  26454  frgranbnb  26547  frgrancvvdeqlem2  26558  frgrancvvdeqlem3  26559  frgrancvvdeqlem4  26560  frgrancvvdeqlemC  26566  frgrawopreglem3  26573  frgrawopreglem4  26574  frgrawopreg  26576  2spotiundisj  26589  topnfbey  26717  isvclem  26816  isnvlem  26849  vsfval  26872  h2hlm  27221  hhcmpl  27441  hhcms  27444  elch0  27495  omlsilem  27645  h1de2ctlem  27798  elspansni  27801  nonbooli  27894  spansncvi  27895  adjeq  28178  cnlnssadj  28323  cnvbraval  28353  brabgaf  28800  fmptdF  28836  fmptcof2  28839  acunirnmpt  28841  acunirnmpt2  28842  ofpreima  28848  fcnvgreu  28855  1stpreima  28867  2ndpreima  28868  elxrge02  28971  psgnfzto1stlem  29181  submatres  29200  lmat22lem  29211  crefdf  29243  cmppcmp  29253  prsdm  29288  prsrn  29289  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  pnfneige0  29325  qqhre  29392  rrhre  29393  esumnul  29437  esumcvgsum  29477  ldgenpisyslem1  29553  measvuni  29604  cntnevol  29618  dya2iocnrect  29670  sibf0  29723  oddpwdc  29743  eulerpartlemd  29755  eulerpartgbij  29761  eulerpartlemgh  29767  isrrvv  29832  coinfliprv  29871  ballotlem7  29924  signswch  29964  bnj23  30038  bnj158  30051  bnj168  30052  bnj1138  30113  bnj1143  30115  bnj1454  30166  bnj110  30182  bnj882  30250  bnj893  30252  bnj916  30257  bnj970  30271  bnj983  30275  bnj984  30276  bnj1137  30317  bnj1174  30325  bnj1388  30355  bnj1398  30356  subfacp1lem5  30420  mrsub0  30667  mrsubccat  30669  mrsubcn  30670  elmrsubrn  30671  msubco  30682  msubvrs  30711  elmthm  30727  mthmblem  30731  elrn3  30906  dfon2lem7  30938  eltrpred  30970  frrlem5e  31032  frrlem11  31036  nofulllem5  31105  brsset  31166  eltrans  31168  elfix  31180  ellimits  31187  elfuns  31192  elsingles  31195  fvtransport  31309  brcolinear2  31335  fvray  31418  linedegen  31420  fvline  31421  ellines  31429  fwddifn0  31441  elhf  31451  hfninf  31463  fnessref  31522  bj-csbsnlem  32090  bj-sels  32143  bj-eltag  32158  bj-sngltag  32164  bj-projun  32175  bj-0nelmpt  32250  bj-elid  32262  bj-elccinfty  32278  f1omptsnlem  32359  icoreelrnab  32378  relowlpssretop  32388  finxpnom  32414  uncov  32560  tan2h  32571  ptrecube  32579  poimirlem25  32604  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  cnambfre  32628  ftc1cnnc  32654  sdclem2  32708  sdclem1  32709  fdc  32711  caushft  32727  issmgrpOLD  32832  ismndo  32841  isrngo  32866  isdivrngo  32919  csbcom2fi  33104  dath  34040  diclspsn  35501  dvh4dimlem  35750  dvh2dim  35752  dvh3dim3N  35756  lcfrvalsnN  35848  mapdh6eN  36047  mapdh7dN  36057  mapdh8b  36087  hdmap1l6e  36122  pellex  36417  rmspecnonsq  36490  islmodfg  36657  aaitgo  36751  areaquad  36821  elcnvcnvintab  36907  elnonrel  36910  elcnvcnvlem  36924  cnvcnvintabd  36925  brfvrcld2  37003  dvgrat  37533  cvgdvgrat  37534  radcnvrat  37535  nznngen  37537  uzmptshftfval  37567  binomcxplemcvg  37575  binomcxplemnotnn0  37577  tpid3gVD  38099  en3lplem2VD  38101  rabid3  38285  rexanuz3  38303  eliuniin  38307  eliuniin2  38335  disjinfi  38375  fsneq  38393  iuneqfzuzlem  38491  allbutfi  38557  elicores  38607  climsuselem1  38674  climsuse  38675  islptre  38686  fnlimfvre  38741  stoweidlem14  38907  stoweidlem39  38932  stoweidlem48  38941  stoweidlem51  38944  stoweidlem59  38952  stoweidlem62  38955  wallispilem3  38960  fourierdlem42  39042  fourierdlem62  39061  fourierdlem80  39079  fourierdlem103  39102  fourierdlem104  39103  etransclem26  39153  rrxsnicc  39196  ioorrnopn  39201  ioorrnopnxr  39203  sge00  39269  sge0fodjrnlem  39309  sge0isum  39320  sge0seq  39339  ismea  39344  meadjiunlem  39358  carageneld  39392  volicorescl  39443  hoidmv1lelem1  39481  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem3  39487  ovnhoilem2  39492  hoiqssbllem2  39513  opnvonmbllem2  39523  ovolval4lem1  39539  iinhoiicc  39565  vonioolem1  39571  smflimlem1  39657  smflimlem2  39658  smflim  39663  nsssmfmbf  39665  smfresal  39673  smfrec  39674  smfdiv  39682  smfpimbor1lem2  39684  ndmaovcl  39932  ndmaovcom  39934  ndmaovass  39935  ndmaovdistr  39936  fmtno4prmfac  40022  iseven  40079  isodd  40080  dfodd5  40110  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  pfxccatpfx1  40290  otiunsndisjX  40317  elfz0lmr  40367  isuspgr  40382  isusgr  40383  ausgrusgri  40398  usgredgappr  40423  edgassv2  40425  uspgredg2vlem  40450  uspgredg2v  40451  ushgredgedga  40456  ushgredgedgaloop  40458  griedg0ssusgr  40489  uhgrissubgr  40499  subumgredg2  40509  umgrres1lem  40529  upgrres1  40532  nbgrcl  40559  nbuhgr  40565  nbuhgr2vtx1edgblem  40573  nbupgrres  40592  edgnbusgreu  40595  nbusgredgeu0  40596  nbusgrf1o0  40597  hashnbusgrnn0  40604  nbupgruvtxres  40634  cusgrfilem2  40672  vtxdg0v  40688  vtxduhgr0nedg  40707  uhgrvd00  40750  rgrx0ndm  40793  1wlk1walk  40843  1wlkp1lem6  40887  iswwlks  41039  wspthnonp  41055  wwlksn0  41059  wlknwwlksnsur  41087  wwlksnwwlksnon  41121  umgr2wlk  41156  elwwlks2ons3  41159  2wspiundisj  41166  elwwlks2s3  41169  rusgrnumwlkg  41180  isclwwlks  41188  wwlksext2clwwlk  41231  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  1pthon2v-av  41320  uhgr3cyclex  41349  isconngr  41356  isconngr1  41357  eucrctshift  41411  isfrgr  41430  frgrnbnb  41463  frgrncvvdeqlem2  41470  frgrncvvdeqlem3  41471  frgrncvvdeqlem4  41472  frgrncvvdeqlemC  41478  frgrwopreglem3  41483  frgrwopreglem4  41484  frgrwopreg  41486  fusgreghash2wspv  41499  av-numclwwlkovf2  41515  av-numclwwlk2lem1  41532  av-numclwlk2lem2f1o  41535  opeliun2xp  41904  ply1sclrmsm  41965  lcoop  41994  lincfsuppcl  41996  linccl  41997  lincvalsng  41999  lincvalpr  42001  lincvalsc0  42004  linc0scn0  42006  lincdifsn  42007  linc1  42008  lincsum  42012  lincscm  42013  lspsslco  42020  snlindsntor  42054  lincresunit3lem2  42063  ldepsnlinclem1  42088  ldepsnlinclem2  42089  setrec1lem1  42233  elpglem3  42255